[Haskell] indirectly recursive dictionaries

[Tom Schrijvers]

> {-
>
> Recursive instance heads as in ...
> Â instance C0 (x,Bool) => C0 x
> ... are Ok if we allow for typechecking scheme as described in "SYB with class".
> The main idea is to assume C0 x in proving the preconditions of the
> body of the clause.
> This is also works for mutual recursion among type classes and
> instances to the extent exercised in ditto paper.
>
> What about the below example though?
> Here recursion detours through an extra class in a way that leads to
> nonterminating typechecking with GHC 6.10.1.
> Does anyone agree that a constraint resolution scheme like the one
> mentioned could be reasonably expected to cover this case?
>
> Regards,
> Ralf
>
> -}
>
> {-# OPTIONS -fglasgow-exts #-}
> {-# OPTIONS -fallow-overlapping-instances #-}
> {-# OPTIONS -fallow-undecidable-instances #-}
>
> -- Direct recursion terminates (typechecking-wise)
>
> class C0 x
> Â where
> Â m0 :: x -> ()
> Â m0 = const undefined
>
> instance (C0 x, C0 y) => C0 (x,y)
> instance C0 Bool
> instance C0 (x,Bool) => C0 x
>
> foo :: ()
> foo = m0 (1::Int)
>
>
> -- Indirect recursion does not terminate (typechecking-wise)
>
> class C1 x
> Â where
> Â m1 :: x -> ()
> Â m1 = const undefined
>
> instance (C1 x, C1 y) => C1 (x,y)
> instance C1 Bool
> instance (C2 x y, C1 (y,Bool)) => C1 x
>
> class C2 x y | x -> y
> instance C2 Int Int

The cyclic dictionaries approach is a bit fragile. The problem appears to 
be here that GHC alternates exhaustive phases of constraint reduction and 
functional dependency improvement. The problem is that in your example you 
need both for detecting a cycle.

This can happen:

 	C1 Int
 	==> 3rd C1 inst
 	C2 Int y, C1 (y,Bool)
 	==> 1st C1 inst
 	C2 Int y, C1 y, C1 Bool
 	==> 2nd C1 inst
 	C2 Int y, C1 y
 	==> 3rd C1 inst
 	C2 Int y, C2 y z, C1 (z,Bool)
 	==>
 	...

where all the constraint are different because fresh variables are 
introduced.

What you want to happen is:

 	C1 Int
 	==> 3rd C1 inst
 	C2 Int y, C1 (y,Bool)
 	==> 1st C1 inst
 	C2 Int y, C1 y, C1 Bool
 	==> 2nd C1 inst
 	C2 Int y, C1 y
 	==> C2 FD improvement {Int/y}  <<<<
  	C2 Int Int, C1 Int
 	==> C1 Int cycle detected
 	C2 Int Int
 	==> C2 1st instance
 	{}

It seems that you want improvement to happen at a higher priority than GHC 
does now.

Tom

--
Tom Schrijvers

Department of Computer Science
K.U. Leuven
Celestijnenlaan 200A
B-3001 Heverlee
Belgium

tel: +32 16 327544
e-mail: tom.schrijvers at cs.kuleuven.be
url: http://www.cs.kuleuven.be/~toms/