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