On Fri, Dec 22, 2006 at 06:44:54PM +0100, Pepe Iborra wrote:
Rank-2 types seem to interact badly with (.) and ($), but my type theory educated neuron doesn't know why. I think this is folklore knowledge?
You say:
runErrSt = (.) runST runErrorT
runErrorT has type ErrorT e m a -> m (Either e a) runST has type (forall s. ST s a) -> a (.) has type (b -> c) -> (a -> b) -> (a -> c) since runST is the first argument to (.), we must unify (forall s. ST s a) with b Quoting the GHC Manual:
There is one place you cannot put a forall: you cannot instantiate a type variable with a forall-type. So you cannot make a forall-type the argument of a type constructor. So these types are illegal:
I am not aware of why this restriction exists, but it is a consequence of a documented restriction. (I hear rumors about limited support for "left-to-right impredicative instantiation" in GHC HEAD, but it's way over my head :( )