diff options
Diffstat (limited to 'testsuite/tests/typecheck/should_compile/tc177.hs')
-rw-r--r-- | testsuite/tests/typecheck/should_compile/tc177.hs | 108 |
1 files changed, 108 insertions, 0 deletions
diff --git a/testsuite/tests/typecheck/should_compile/tc177.hs b/testsuite/tests/typecheck/should_compile/tc177.hs new file mode 100644 index 0000000000..613528fef3 --- /dev/null +++ b/testsuite/tests/typecheck/should_compile/tc177.hs @@ -0,0 +1,108 @@ +{-# LANGUAGE FlexibleInstances, UndecidableInstances, + MultiParamTypeClasses, FunctionalDependencies #-} + +-- This is a rather complicated program that uses functional +-- dependencies to do Peano arithmetic. +-- +-- GHC 6.2 dies because tcSimplifyRestricted was trying to +-- be too clever. See 'Plan B' in tcSimplifyRestricted + +module ShouldCompile where + + + +-- This is the offending definition. It falls under +-- the monomorphism restriction, so tcSimplifyRestricted applies +bug = ins b (ins b Nil) + + +------------------------------------ +data LAB l r = LAB l r deriving Show + +data OR a b = OR a b deriving Show + + +data Cons x y = Cons x y deriving Show + +data Nil = Nil deriving Show + +data T = T + +data F = F + +data A = A deriving Show + +data B = B deriving Show + +data Zero = Zero + +data Succ n = Succ n + +b = ((LAB B []),[]) + +-- insertion function +-- insert label pairs in the a list of list, each list contains a collection of +-- label pair that sharing the common label. + + +class Ins r l l' | r l -> l' where + ins :: r -> l -> l' + + +instance Ins ((LAB l1 r1),r1') Nil (Cons (Cons ((LAB l1 r1),r1') Nil) Nil) where + ins l Nil = (Cons (Cons l Nil) Nil) + + +instance ( L2N l1 n1 + , L2N l2 n2 + , EqR n1 n2 b + , Ins1 ((LAB l1 r1),r1') (Cons (Cons ((LAB l2 r2),r2') rs) rs') b l + ) => Ins ((LAB l1 r1),r1') (Cons (Cons ((LAB l2 r2),r2') rs) rs') l + where + ins ((LAB l1 r1),r1') (Cons (Cons ((LAB l2 r2),r2') rs) rs') + = ins1 ((LAB l1 r1),r1') (Cons (Cons ((LAB l2 r2),r2') rs) rs') + (eqR (l2n l1) (l2n l2)) +-- Note that n1 and n2 are functionally defined by l1 and l2, respectively, +-- and b is functionally defined by n1 and n2. + + +class Ins1 r l b l' | r l b -> l' where + ins1 :: r -> l -> b -> l' + +instance Ins1 ((LAB l1 r1),r1') (Cons r rs) T + (Cons (Cons ((LAB l1 r1),r1') r) rs) where + ins1 l (Cons r rs) _ = (Cons (Cons l r) rs) + +instance ( Ins ((LAB l1 r1),r1') rs rs') + => Ins1 ((LAB l1 r1),r1') (Cons r rs) F (Cons r rs') where + ins1 l (Cons r rs) _ = (Cons r (ins l rs)) + +-- class for mapping label to number + +class L2N l n | l -> n where + l2n :: l -> n + +instance L2N A Zero where + l2n A = Zero + +instance L2N B (Succ Zero) where + l2n B = Succ Zero + + +-- class for comparing number type + +class EqR n1 n2 b | n1 n2 -> b where + eqR :: n1 -> n2 -> b + +instance EqR Zero Zero T where + eqR _ _ = T + +instance EqR Zero (Succ n) F where + eqR _ _ = F + +instance EqR (Succ n) Zero F where + eqR _ _ = F + +instance (EqR n1 n2 b) => EqR (Succ n1) (Succ n2) b where + eqR (Succ n1) (Succ n2) = eqR n1 n2 + |