summaryrefslogtreecommitdiff
path: root/tests/examples/ghc86/T6018th.hs
diff options
context:
space:
mode:
Diffstat (limited to 'tests/examples/ghc86/T6018th.hs')
-rw-r--r--tests/examples/ghc86/T6018th.hs121
1 files changed, 121 insertions, 0 deletions
diff --git a/tests/examples/ghc86/T6018th.hs b/tests/examples/ghc86/T6018th.hs
new file mode 100644
index 0000000..91c61a1
--- /dev/null
+++ b/tests/examples/ghc86/T6018th.hs
@@ -0,0 +1,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")))
+ ] )
+