Tom Schrijvers wrote:
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.
It seems we can convince GHC to do constraint reduction and improvement in the order we desire. The key is to use the continuation-passing style -- which forces things to happen in the right order, both at the run-time and at the compile time. I took the liberty to flesh out the example a bit more, to verify that recursive dictionaries are indeed constructed and used. The trace statement shows it. {-# OPTIONS -fglasgow-exts #-} {-# OPTIONS -fallow-overlapping-instances #-} {-# OPTIONS -fallow-undecidable-instances #-} import Debug.Trace class C1 x where m1 :: x -> Int instance (C1 x, C1 y) => C1 (x,y) where m1 (x,y) = m1 x + m1 y instance C1 Bool where m1 = fromEnum -- Was: instance (C2 x y, C1 (y,Bool)) => C1 x instance C2CPS x (C1K Bool) => C1 x where m1 x = trace "recursive C1" $ c2invoke (C1K True) x newtype C1K a = C1K a -- The class C2CPS below is a CPS version of the class C2 below -- class C2 x y | x -> y where c2 :: x -> y -- instance C2 Int Int where c2 = id -- The functional dependency becomes implicit class C2CPS x k where c2invoke :: k -> x -> Int instance Apply k Int Int => C2CPS Int k where c2invoke k x = apply k x class Apply f x y | f x -> y where apply:: f -> x -> y instance C1 (b,a) => Apply (C1K a) b Int where apply (C1K a) x = m1 (x,a) -- It is this declaration that was causing nontermination of typechecking. -- Not any more bar :: Int bar = m1 (1::Int)