Rank2 polymorphism & type inference
Simon PeytonJones
simonpj@microsoft.com
Tue, 5 Dec 2000 05:12:20 0800
 > My question is: how does the type inference algorithm work in the
 > presence of rank2 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 rank2 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, 20000915) 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 overkillish. But it's unsettling that the inference algorithm is
incomplete.
Simon