Unification of (var,term) failed

compile this program:

<http://svn.berlios.de/viewcvs/al4nin/trunk/found-bugs/bug11-Thrist.omg?
rev=361&view=markup>

I would expect it to compile, but I get:

**** Near line: 203 column: 1

While type checking in the scope of:
   te1a
We need to prove:
   Equal {blowLike {countArr (Int -> Bool)} (Int -> Bool) {blow #1 b}} {Int; c}, Equal {range 
{countArr (Int -> Bool)} (Int -> Bool)} Bool, Equal {blow #1 b} {Int; b}
From the truths:
And the rules:S,Z,
But, Unification of (var,term) failed, this is impossible
[(bgw,{rh0; sh0})]

If I comment this line out, it compiles. The only difference between te1 and 
te1a is the usage of 
{{{Greater}}} vs. {{{ge}}}.

Typing them in the listener gives the same types:

prompt> Greater
Greater : forall (a:Row *0).Cat {Int,Int; a} {Bool; a}
prompt> gt
(Prim (ArrTractable IntTractable BoolTractable) Pgt <fn>) : forall (a:Row 
*0).Cat {Int,Int; a} {Bool; 
a}

So I really do not understand why this does not compile. My first guess is that 
unification takes 
place before normalization of type expressions. Maybe lazy evaluation of types 
is somehow 
connected to the problem.

Original issue reported on code.google.com by ggr...@gmail.com on 15 May 2007 at 8:04

google-code-export / omega

Unification of (var,term) failed #7