# Deriving excitement

Simon Peyton-Jones simonpj@microsoft.com
Fri, 1 Feb 2002 03:17:07 -0800

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