613528fef37903f170d5c0edc544271da49cbcc0
[ghc.git] / testsuite / tests / typecheck / should_compile / tc177.hs
1 {-# LANGUAGE FlexibleInstances, UndecidableInstances,
2 MultiParamTypeClasses, FunctionalDependencies #-}
3
4 -- This is a rather complicated program that uses functional
5 -- dependencies to do Peano arithmetic.
6 --
7 -- GHC 6.2 dies because tcSimplifyRestricted was trying to
8 -- be too clever. See 'Plan B' in tcSimplifyRestricted
9
10 module ShouldCompile where
11
12
13
14 -- This is the offending definition. It falls under
15 -- the monomorphism restriction, so tcSimplifyRestricted applies
16 bug = ins b (ins b Nil)
17
18
19 ------------------------------------
20 data LAB l r = LAB l r deriving Show
21
22 data OR a b = OR a b deriving Show
23
24
25 data Cons x y = Cons x y deriving Show
26
27 data Nil = Nil deriving Show
28
29 data T = T
30
31 data F = F
32
33 data A = A deriving Show
34
35 data B = B deriving Show
36
37 data Zero = Zero
38
39 data Succ n = Succ n
40
41 b = ((LAB B []),[])
42
43 -- insertion function
44 -- insert label pairs in the a list of list, each list contains a collection of
45 -- label pair that sharing the common label.
46
47
48 class Ins r l l' | r l -> l' where
49 ins :: r -> l -> l'
50
51
52 instance Ins ((LAB l1 r1),r1') Nil (Cons (Cons ((LAB l1 r1),r1') Nil) Nil) where
53 ins l Nil = (Cons (Cons l Nil) Nil)
54
55
56 instance ( L2N l1 n1
57 , L2N l2 n2
58 , EqR n1 n2 b
59 , Ins1 ((LAB l1 r1),r1') (Cons (Cons ((LAB l2 r2),r2') rs) rs') b l
60 ) => Ins ((LAB l1 r1),r1') (Cons (Cons ((LAB l2 r2),r2') rs) rs') l
61 where
62 ins ((LAB l1 r1),r1') (Cons (Cons ((LAB l2 r2),r2') rs) rs')
63 = ins1 ((LAB l1 r1),r1') (Cons (Cons ((LAB l2 r2),r2') rs) rs')
64 (eqR (l2n l1) (l2n l2))
65 -- Note that n1 and n2 are functionally defined by l1 and l2, respectively,
66 -- and b is functionally defined by n1 and n2.
67
68
69 class Ins1 r l b l' | r l b -> l' where
70 ins1 :: r -> l -> b -> l'
71
72 instance Ins1 ((LAB l1 r1),r1') (Cons r rs) T
73 (Cons (Cons ((LAB l1 r1),r1') r) rs) where
74 ins1 l (Cons r rs) _ = (Cons (Cons l r) rs)
75
76 instance ( Ins ((LAB l1 r1),r1') rs rs')
77 => Ins1 ((LAB l1 r1),r1') (Cons r rs) F (Cons r rs') where
78 ins1 l (Cons r rs) _ = (Cons r (ins l rs))
79
80 -- class for mapping label to number
81
82 class L2N l n | l -> n where
83 l2n :: l -> n
84
85 instance L2N A Zero where
86 l2n A = Zero
87
88 instance L2N B (Succ Zero) where
89 l2n B = Succ Zero
90
91
92 -- class for comparing number type
93
94 class EqR n1 n2 b | n1 n2 -> b where
95 eqR :: n1 -> n2 -> b
96
97 instance EqR Zero Zero T where
98 eqR _ _ = T
99
100 instance EqR Zero (Succ n) F where
101 eqR _ _ = F
102
103 instance EqR (Succ n) Zero F where
104 eqR _ _ = F
105
106 instance (EqR n1 n2 b) => EqR (Succ n1) (Succ n2) b where
107 eqR (Succ n1) (Succ n2) = eqR n1 n2
108