[project @ 2003-09-11 14:20:40 by simonpj]

[project @ 2003-09-11 14:20:40 by simonpj]
--------------------------
	    Allow recursive dictionaries
	   --------------------------

In response to various bleatings, here's a lovely fix that involved simply
inverting two lines of code, to allow recursive dictionaries.  Here's
the comment.  (typecheck/should_run/tc030 tests it)

Note [RECURSIVE DICTIONARIES]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider
    data D r = ZeroD | SuccD (r (D r));

    instance (Eq (r (D r))) => Eq (D r) where
        ZeroD     == ZeroD     = True
        (SuccD a) == (SuccD b) = a == b
        _         == _         = False;

    equalDC :: D [] -> D [] -> Bool;
    equalDC = (==);

We need to prove (Eq (D [])).  Here's how we go:

	d1 : Eq (D [])

by instance decl, holds if
	d2 : Eq [D []]
	where 	d1 = dfEqD d2

by instance decl of Eq, holds if
	d3 : D []
	where	d2 = dfEqList d2
		d1 = dfEqD d2

But now we can "tie the knot" to give

	d3 = d1
	d2 = dfEqList d2
	d1 = dfEqD d2

and it'll even run!  The trick is to put the thing we are trying to prove
(in this case Eq (D []) into the database before trying to prove its
contributing clauses.