Weird quantification in error message

[Josef Svenningsson]

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