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)
_______________________________________________
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell
