Deriving excitement

[Simon Peyton-Jones]

Folks

Here is a nice corner I have just tripped over, triggered by recent
email from Olaf Chitil and David Feuer.  Is this legal Haskell 98?

	data Min h a =3D E | M a (h a)   deriving( Eq )

[This exact decl occurs in Chris Okasaki's Edison library.]

According to the report it is not legal, because the derived instance
declaration presumably has form

	instance (Eq a, Eq (h a)) =3D> Eq (Min h a) where ...

but that is not legal Haskell 98, and the report says that the derived
instance declaration only has an instance context of the form (Eq
tyvar).


OK, so is this a bug in the report?   No, we can't allow instance
declarations like those above in general, because that can lead to
undecidable instances.   So I conclude that the report is OK, but
the above 'deriving' clause is not ok.


Suppose we allow undecidable instances (a GHC extension, which
can make the type checker diverge).  Then 'deriving' gives a second
way to make the compiler diverge.  David Feuer=20
produced an example similar to this:

	data Sq h a =3D E (Sq (Pair h) a)  | M a (h a) deriving( Eq )

	newtype Pair h a =3D P (h (h a)) deriving( Eq )

Clearly, to derive Eq for Sq, one needs (Eq a, Eq (h a)).
But we also need (Eq (Sq (Pair h) a)).  Hence we need=20
(Eq a, Eq (h (h a))).  But then we need....
If you work it out, you'll see that the derived instance declaration,
straightforwardly computed, would be

	instance (Eq a, Eq (h a), Eq (h (h a)), Eq (h (h (h a))), ...)=20
		=3D> Eq (Sq h a) where ...

Obviously this can't be done.   So the bit of the compiler that does
a fixpoint calculation to figure out the context of a derived instance
will diverge.

ASIDE: One needs an extension to Haskell to write the=20
instance decl at all.  What one needs to write is:

	instance (Eq a, forall b. Eq b =3D> Eq (h b)) =3D> Eq (Sq h a)
where..
END OF ASIDE


Simon