Hi, After sending out my question, I noticed that hugs and ghc understood my code differently: from the error messages, we can see that hugs view (\a -> super a) as having type Sub b _1 -> Super b _2, while ghc thinks it is Sub c a -> Super c Int. To verify it, I changed my code s.t. y is defined as y = f (\(a :: Sub c Int) -> super a) x instead of y = f (\a -> super a) x Guess what happened: ghc *accepted* the code, and hugs *rejected* it with message: ERROR "R2Test.hs" (line 19): Cannot justify constraints in application *** Expression : \a -> super a *** Type : Sub b Int -> Super b _2 *** Given context : () *** Constraints : SubType (Sub b Int) (Super b _2) Aha, this is something interesting! Either there is no standard for the Haskell rank-2 type inference algorithm (which is a sad thing), or one of hugs and ghc is wrong here. Now the hugs/ghc guys on the list can no longer remain silent -- you got to defend yourselves! :-) Could anyone explain to me what the right behavior is supposed to be here? Thanks. -- Zhanyong Zhanyong Wan wrote:

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!