https://code.google.com/p/omega/source/browse/trunk/tests/move.prg?spec=svn1375&r=1375

Results in this error:

**** Near File: ../tests/move.prg line: 13 column: 1

While inferring the type of the pattern: Nil we expected it to have type: Thrist (At Char) _b {plus _a _b} but we computed type: Thrist _d _e _e where types have kinds: _b:Nat _a:Nat _c:*1 _d:_c ~> _c ~> *0 _e:_c but, the current refinement fails because _b != {plus _a _b}. Sometimes reordering the patterns can fix this.

The last sentence seems bogus since there is only one pattern involved.

But I wonder how these types of functions can be written. the diagnostic _b != {plus _a _b} is wrong, as it fails for _a = 0t. This could be a hint to the type checker.

Alternatively the provided RHS could provide a clue, as it fixes _a to 0t. Feeding this back into the pattern's equation should also make it solvable.

The next revision provides a theorem, but, alas, it is ignored.