Rank-2 polymorphism & type inference

[Simon Peyton-Jones]

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