Hi! I'm observing very strange error messages from Hugs involving rank-2 types. The whole thing could just be an error in the pretty printer but it is never the less rather disturbing. I'm running the December 2001 release. OK, here's how to reproduce the behaviour. Consider the following (*not* type correct) program: \begin{code} data Plus m1 m2 a = T1 (m1 (Plus m1 m2 a)) | T2 (m2 (Plus m1 m2 a)) | Var a run :: (Functor m1, Functor m2) => (forall a. m1 a -> a) -> (forall a. m2 a -> a) -> Plus m1 m2 a -> a run r1 r2 (T1 m) = run r1 r2 (fmap (run r1 r2) r1 m) run r1 r2 (T2 m) = run r1 r2 (fmap (run r1 r2) r2 m) run r1 r2 (Var a) = a \end{code} Hugs should give a type error for the definition of "run" and does so. But the error message looks really strange. Here's what it looks like: Prelude> :r Reading file "HugsBug.hs": Type checking ERROR "HugsBug.hs":6 - Type error in explicitly typed binding *** Term : run *** Type : (forall a. a d -> d) -> (forall a. b d -> d) -> Plus a b (Plus a b c) -> c *** Does not match : (forall a. a d -> d) -> (forall a. b d -> d) -> Plus a b (Plus a b c) -> Plus a b c *** Because : unification would give infinite type Prelude> Look at the quantification. It quantifies over the wrong type variable. Cheers, /Josef