Rank-2 polymorphism & type inference

[Zhanyong Wan]

Hello,

I'm playing with Haskell's rank-2 polymorphism extension and am puzzled
by the following example:

-----------------------------------------------------------
module R2Test where

class SubType a b where
  super :: a -> b

data Sub c a = Sub
data Super c a = Super

instance SubType (Sub c a) (Super c a)

f :: (forall c. Sub c a -> Super c b) -> Sub c a -> Super c b
f g x = undefined

x :: Sub c Int
x = undefined

y :: Super c Int
y = f (\a -> super a) x
----------------------------------------------------------

I though the definition of y should type-check because (roughly):

1. We know x :: Sub c Int, y :: Super c Int
2. Hence in f :: (forall c. Sub c a -> Super c b) -> Sub c a -> Super c
b, we know a is Int and b is Int.
3. Hence (\a -> super a) :: (forall c. Sub c Int -> Super c Int), and we
are all set.

However, Hugs 98 Feb 2000 (with the -98 switch) gives me:

ERROR "R2Test.hs" (line 19): Cannot justify constraints in application
*** Expression    : \a -> super a
*** Type          : Sub b _1 -> Super b _2
*** Given context : ()
*** Constraints   : SubType (Sub b _1) (Super b _2)

and GHC 4.08.1 (with the -fglasgow-exts switch) gives:

R2Test.hs:19:
    Could not deduce `SubType (Sub c a) (Super c Int)'
        from the context: ()
    Probable cause: missing `SubType (Sub c a) (Super c Int)'
                    in the type signature of an expression
                    or missing instance declaration for `SubType (Sub c
a) (Super
 c Int)'
    arising from use of `super' at R2Test.hs:16
    In the right-hand side of a lambda abstraction: super a

If I remove the "forall c." from the type signature for f, then both
compilers accept my code.

My question is: how does the type inference algorithm work in the
presence of rank-2 types?  Does anyone know of any documentation on
this?  Thanks!

-- Zhanyong

# Zhanyong Wan     http://pantheon.yale.edu/~zw23/ ____
# Yale University, Dept of Computer Science       /\___\
# P.O.Box 208285, New Haven, CT 06520-8285        ||___|