| > 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! I had a look at this. Actually it turns out to be only loosely related to rank-2 polymorphism. I've been able to reproduce your problem using only Haskell 98. It looks like a problem with incomplete type inference Consider this: module MP where class C t where op :: t -> Bool instance C [t] where op x = True test :: [Int] -> Bool -- REQUIRED! test y = let f :: c -> Bool f x = op (y >> return x) in f (y::[Int]) Both GHC and Hugs reject this module if the type signature for test is omitted. NHC (v1.00, 2000-09-15) falls over completely, with Fail: Prelude.chr: bad argument All three succeed if the signature is in, or if the signature for f is omitted. This was unexpected, to me at least. You may need to add a type signature if polymorphic recursion is being used, but here it isn't! The problem is this: the compiler learns that y::[Int] "too late" to make use of it when solving the constraints arising from the RHS of f. In more detail, here's what happens. First we typecheck the RHS of f, deducing the types x :: a where a is fresh y :: k a where k is fresh y >> return x :: k a op (y >> return x) :: Bool with constraint C (k a) \x -> op (y >> return x) :: a -> Bool with constraint C (k a) Now we try to generalise over a. We need to discharge the contraint C (k a). Later we will find that y::[Int], so k=[], but we don't know that yet. So we can't solve the constraint. Adding the type signature to 'f' lets both GHC and Hugs figure out that y::[Int] in advance, so we need to solve the constraint C ([] a), which is fine. So I think you have uncovered a genuine problem, and one I don't know how to solve. It can always be "solved" by adding more type information, such as the type sig for 'test'. In you case you said: | 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 This is exactly right, and GHC is happy now. I can't account for Hugs' behaviour. The "right" solution is presumably to defer all constraint checking until we know what 'k' is. But that's a bit tricky because the constraint checking generates bindings that must appear in f's RHS. A full solution looks a bit over-kill-ish. But it's unsettling that the inference algorithm is incomplete. Simon