big lambda in class declarations

[Hal Daume III]

So the word on the street is that allowing big lambda makes type inference
undecidable.  This makes sense to me since allowing big lambda essentially
allows you to program at the type level and thus of course you'll get
undecidability.

However, I'm having difficulty understanding where the undecidability
sneaks in if you allow big lambda in class declarations.  I suppose the
cannonical example is when you want to write something like:

> class Set s where { ... }
> instance Set (/\ a. FiniteMap a ()) where { ... }

but now you have to write:

> data FMSet a = FMSet (FiniteMap a ())
> instance Set FMSet where { ... }

The big lambda is of course equivalent to not applying type synonyms
completely, somethign like:

> type FM a = FiniteMap a ()
> instance Set FM where { ... }

will of course also be rejected (since this would give us a way to do big
lambda).

Could some one help my intuition a bit here and explain to me how you
could use big lambdas in class declarations to write programs?

Thanks!

 - Hal

--
 Hal Daume III                                   | hdaume@isi.edu
 "Arrest this man, he talks in maths."           | www.isi.edu/~hdaume