Rank-2 polymorphism & type inference

[Mark P Jones]

Johan Nordlander and I have been looking at these interesting examples,
and would like to offer another entertaining variation to the =
collection:

  class C t where op :: t -> Bool
  instance C [t] where op x =3D True

  p y =3D (let f :: c -> Bool; f x =3D op (y >> return x) in f, y ++ [])
  q y =3D (y ++ [], let f :: c -> Bool; f x =3D op (y >> return x) in f)

The definitions of p and q differ only in the order of the components in
the pair on their right-hand sides.  And yet:

  ghc and "Typing Haskell in Haskell" reject p, but accept q;
  Hugs rejects q, but accepts p;
  hbc rejects both p and q;
  nhc98 ... (Malcolm, can you fill in the blank for us!).

The type signature for f forces context reduction to take place, and
the results of this depend on whether or not the type of y is known,
which in turn depends on which component of the pair the type checker
analyzes first.  I'm sure we will all continue to ponder this for some
time to come ...

All the best,
Mark & Johan