Fix T6018th test failure
[ghc.git] / testsuite / tests / th / T6018th.hs
1 {-# LANGUAGE TypeFamilies, DataKinds, UndecidableInstances, PolyKinds #-}
2
3 module T6018th where
4
5 import Language.Haskell.TH
6
7 -- Test that injectivity works correct with TH. This test is not as exhaustive
8 -- as the original T6018 test.
9
10 -- type family F a b c = (result :: k) | result -> a b c
11 -- type instance F Int Char Bool = Bool
12 -- type instance F Char Bool Int = Int
13 -- type instance F Bool Int Char = Char
14 $( return
15 [ OpenTypeFamilyD
16 (mkName "F")
17 [ PlainTV (mkName "a"), PlainTV (mkName "b"), PlainTV (mkName "c") ]
18 (TyVarSig (KindedTV (mkName "result") (VarT (mkName "k"))))
19 (Just $ InjectivityAnn (mkName "result")
20 [(mkName "a"), (mkName "b"), (mkName "c") ])
21 , TySynInstD
22 (mkName "F")
23 (TySynEqn [ ConT (mkName "Int"), ConT (mkName "Char")
24 , ConT (mkName "Bool")]
25 ( ConT (mkName "Bool")))
26 , TySynInstD
27 (mkName "F")
28 (TySynEqn [ ConT (mkName "Char"), ConT (mkName "Bool")
29 , ConT (mkName "Int")]
30 ( ConT (mkName "Int")))
31 , TySynInstD
32 (mkName "F")
33 (TySynEqn [ ConT (mkName "Bool"), ConT (mkName "Int")
34 , ConT (mkName "Char")]
35 ( ConT (mkName "Char")))
36 ] )
37
38 -- this is injective - a type variables mentioned on LHS is not mentioned on RHS
39 -- but we don't claim injectivity in that argument.
40 --
41 -- type family J a (b :: k) = r | r -> a
42 ---type instance J Int b = Char
43 $( return
44 [ OpenTypeFamilyD
45 (mkName "J")
46 [ PlainTV (mkName "a"), KindedTV (mkName "b") (VarT (mkName "k")) ]
47 (TyVarSig (PlainTV (mkName "r")))
48 (Just $ InjectivityAnn (mkName "r") [mkName "a"])
49 , TySynInstD
50 (mkName "J")
51 (TySynEqn [ ConT (mkName "Int"), VarT (mkName "b") ]
52 ( ConT (mkName "Int")))
53 ] )
54
55 -- Closed type families
56
57 -- type family IClosed (a :: *) (b :: *) (c :: *) = r | r -> a b where
58 -- IClosed Int Char Bool = Bool
59 -- IClosed Int Char Int = Bool
60 -- IClosed Bool Int Int = Int
61
62 $( return
63 [ ClosedTypeFamilyD
64 (mkName "I")
65 [ KindedTV (mkName "a") StarT, KindedTV (mkName "b") StarT
66 , KindedTV (mkName "c") StarT ]
67 (TyVarSig (PlainTV (mkName "r")))
68 (Just $ InjectivityAnn (mkName "r") [(mkName "a"), (mkName "b")])
69 [ TySynEqn [ ConT (mkName "Int"), ConT (mkName "Char")
70 , ConT (mkName "Bool")]
71 ( ConT (mkName "Bool"))
72 , TySynEqn [ ConT (mkName "Int"), ConT (mkName "Char")
73 , ConT (mkName "Int")]
74 ( ConT (mkName "Bool"))
75 , TySynEqn [ ConT (mkName "Bool"), ConT (mkName "Int")
76 , ConT (mkName "Int")]
77 ( ConT (mkName "Int"))
78 ]
79 ] )
80
81 -- reification test
82 $( do { decl@([ClosedTypeFamilyD _ _ _ (Just inj) _]) <-
83 [d| type family Bak a = r | r -> a where
84 Bak Int = Char
85 Bak Char = Int
86 Bak a = a |]
87 ; return decl
88 }
89 )
90
91 -- Check whether incorrect injectivity declarations are caught
92
93 -- type family I a b c = r | r -> a b
94 -- type instance I Int Char Bool = Bool
95 -- type instance I Int Int Int = Bool
96 -- type instance I Bool Int Int = Int
97 $( return
98 [ OpenTypeFamilyD
99 (mkName "H")
100 [ PlainTV (mkName "a"), PlainTV (mkName "b"), PlainTV (mkName "c") ]
101 (TyVarSig (PlainTV (mkName "r")))
102 (Just $ InjectivityAnn (mkName "r")
103 [(mkName "a"), (mkName "b") ])
104 , TySynInstD
105 (mkName "H")
106 (TySynEqn [ ConT (mkName "Int"), ConT (mkName "Char")
107 , ConT (mkName "Bool")]
108 ( ConT (mkName "Bool")))
109 , TySynInstD
110 (mkName "H")
111 (TySynEqn [ ConT (mkName "Int"), ConT (mkName "Int")
112 , ConT (mkName "Int")]
113 ( ConT (mkName "Bool")))
114 , TySynInstD
115 (mkName "H")
116 (TySynEqn [ ConT (mkName "Bool"), ConT (mkName "Int")
117 , ConT (mkName "Int")]
118 ( ConT (mkName "Int")))
119 ] )