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 ||___|