Skip to content
  • Simon Peyton Jones's avatar
    [project @ 2003-09-11 14:20:40 by simonpj] · 25aeb246
    Simon Peyton Jones authored
    --------------------------
    	    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.
    25aeb246