[Haskell] indirectly recursive dictionaries
Ralf Laemmel
rlaemmel at gmail.com
Mon Mar 16 21:52:41 EDT 2009
{-
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
-- It is this declaration that causes nontermination of typechecking.
bar :: ()
bar = m1 (1::Int)
More information about the Haskell
mailing list