solitary patterns involving type functions do not work

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.

Original issue reported on code.google.com by ggr...@gmail.com on 25 Nov 2012 at 2:18

ggreif / omega

solitary patterns involving type functions do not work #109