"The signature contexts in a mutually recursive group should all be identical"; why?

Simon Peyton-Jones simonpj@microsoft.com
Fri, 21 Dec 2001 01:35:37 -0800


[Note to the Haskell list.  The question this thread is discussing
is whether the H98 rule that all the functions in a mutually=20
recursive group must have the same context, is a show stopper.]

| Oeer.  Come to think of it, if f is getting the dictionary=20
| (in the real world
| example) from the context, rather than from the existential=20
| type, I fear it may be getting the wrong dictionary, and will=20
| crash badly when I try to run the code. =20

No I don't think that can happen. But I have thought of a test
case

data T =3D forall a. Eq a =3D> MkT a a T
	 | Nil

f :: T -> Bool
f Nil =3D True
f (MkT x y t) =3D g x y t

g  :: Eq b =3D> b -> b -> T -> Bool
g x y t =3D (x=3D=3Dy) && f t


Notice that
  (a) f and g are mutually recursive
  (b) They have different contexts in their type sig
  (c)  If they were made the same, f would get an
	ambiguous type  f :: Eq a =3D> T -> Bool
  (d) Haskell's polymorphic recursion is essential here;
	each call to g may be at a different type

So it looks to me that, in the presence of existentials, the H98
rule goes from being moot to being throughly awkward.=20

Mark's THIH paper shows that there's no real need for the rule,
because one can type-check the bindings without type sigs as
a group, and then the ones with type sigs one by one. =20

But what happens for pattern-bindings that bind more than
one variable.  Must all those variables have the same context?
(I hope so.)

Needless to say, I'm not proposing any changes in H98!  But
I thought the example would be of interest.  Maybe it's well known,
but it wasn't to me.

Simon