diff options
Diffstat (limited to 'tests/examples/ghc86/T6018th.hs')
-rw-r--r-- | tests/examples/ghc86/T6018th.hs | 121 |
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"))) + ] ) + |