[Haskell] Re: indirectly recursive dictionaries

[oleg at okmij.org]

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)