Sat Jan 26 15:36:11 CET 2013


The general idea above works, but there's a slight problem.  Type
inference seems to work "backwards", meaning that going down the code
actually affects type bindings that where made earlier.

Trouble came with typing
in :: L a -> a

for a binding (e (in l)) and types e : e and l : l, the unification
step is

               l = List e

However, it is possible that l is not a type variable, but something
like List e2.  In which case the unification would be:

    List e = List e2
 => e = e2

Ok, this works.