summaryrefslogtreecommitdiff
path: root/tests/examples/ghc86/T6018th.hs
blob: 91c61a18b392030d4a019719ba8bad493cb67022 (plain)
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
{-# LANGUAGE TypeFamilyDependencies, DataKinds, UndecidableInstances,
             PolyKinds #-}
{-# LANGUAGE TemplateHaskell #-}
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 [ ConT (mkName "Int"), ConT (mkName "Char")
                 , ConT (mkName "Bool")]
                 ( ConT (mkName "Bool")))
   , TySynInstD
       (mkName "F")
       (TySynEqn [ ConT (mkName "Char"), ConT (mkName "Bool")
                 , ConT (mkName "Int")]
                 ( ConT (mkName "Int")))
   , TySynInstD
       (mkName "F")
       (TySynEqn [ 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 [ 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 [ ConT (mkName "Int"), ConT (mkName "Char")
                  , ConT (mkName "Bool")]
                  ( ConT (mkName "Bool"))
       , TySynEqn [ ConT (mkName "Int"), ConT (mkName "Char")
                  , ConT (mkName "Int")]
                  ( ConT (mkName "Bool"))
       , TySynEqn [ 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 [ ConT (mkName "Int"), ConT (mkName "Char")
                 , ConT (mkName "Bool")]
                 ( ConT (mkName "Bool")))
   , TySynInstD
       (mkName "H")
       (TySynEqn [ ConT (mkName "Int"), ConT (mkName "Int")
                 , ConT (mkName "Int")]
                 ( ConT (mkName "Bool")))
   , TySynInstD
       (mkName "H")
       (TySynEqn [ ConT (mkName "Bool"), ConT (mkName "Int")
                 , ConT (mkName "Int")]
                 ( ConT (mkName "Int")))
   ] )