Injective type families

For details see #6018, Phab:D202 and the wiki page:

https://ghc.haskell.org/trac/ghc/wiki/InjectiveTypeFamilies

This patch also wires-in Maybe data type and updates haddock submodule.

Test Plan: ./validate

Reviewers: simonpj, goldfire, austin, bgamari

Subscribers: mpickering, bgamari, alanz, thomie, goldfire, simonmar,
             carter

Differential Revision: https://phabricator.haskell.org/D202

GHC Trac Issues: #6018

11 files changed, 157 insertions, 28 deletions

diff --git a/testsuite/tests/th/ClosedFam2TH.hs b/testsuite/tests/th/ClosedFam2TH.hs
index cd2dc2de60..bb355a2790 100644
--- a/testsuite/tests/th/ClosedFam2TH.hs
+++ b/testsuite/tests/th/ClosedFam2TH.hs
@@ -4,16 +4,18 @@ module ClosedFam2 where
 
 import Language.Haskell.TH
 
-$( return [ ClosedTypeFamilyD (mkName "Equals")
-                              [ KindedTV (mkName "a") (VarT (mkName "k"))
-                              , KindedTV (mkName "b") (VarT (mkName "k")) ]
-                              Nothing
-                              [ TySynEqn [ (VarT (mkName "a"))
-                                         , (VarT (mkName "a")) ]
-                                         (ConT (mkName "Int"))
-                              , TySynEqn [ (VarT (mkName "a"))
-                                         , (VarT (mkName "b")) ]
-                                         (ConT (mkName "Bool")) ] ])
+$( return [ ClosedTypeFamilyD
+              (mkName "Equals")
+              [ KindedTV (mkName "a") (VarT (mkName "k"))
+              , KindedTV (mkName "b") (VarT (mkName "k")) ]
+              ( TyVarSig (KindedTV (mkName "r") (VarT (mkName "k"))))
+              Nothing
+              [ TySynEqn [ (VarT (mkName "a"))
+                         , (VarT (mkName "a")) ]
+                         (ConT (mkName "Int"))
+              , TySynEqn [ (VarT (mkName "a"))
+                         , (VarT (mkName "b")) ]
+                         (ConT (mkName "Bool")) ] ])
 
 a :: Equals b b
 a = (5 :: Int)
diff --git a/testsuite/tests/th/T10306.hs b/testsuite/tests/th/T10306.hs
index b93114b61c..b74eb591e9 100644
--- a/testsuite/tests/th/T10306.hs
+++ b/testsuite/tests/th/T10306.hs
@@ -9,6 +9,6 @@ import GHC.TypeLits
 -- caused a crash, because it has no equations
 $(do x <- reify ''(+)
      case x of
-       FamilyI (ClosedTypeFamilyD _ _ _ []) _ -> return []
-       _                                      -> error $ show x
+       FamilyI (ClosedTypeFamilyD _ _ _ _ []) _ -> return []
+       _                                        -> error $ show x
  )
diff --git a/testsuite/tests/th/T6018th.hs b/testsuite/tests/th/T6018th.hs
new file mode 100644
index 0000000000..32053636e2
--- /dev/null
+++ b/testsuite/tests/th/T6018th.hs
@@ -0,0 +1,120 @@
+{-# LANGUAGE TypeFamilies, 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
+       (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
+       (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
+       (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 _ _ _ (Just inj) _]) <-
+               [d| type family Bak a = r | r -> a where
+                        Bak Int  = Char
+                        Bak Char = Int
+                        Bak a    = a |]
+      ; runIO $ putStrLn (pprint inj)
+      ; 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
+       (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")))
+   ] )
diff --git a/testsuite/tests/th/T6018th.stderr b/testsuite/tests/th/T6018th.stderr
new file mode 100644
index 0000000000..98c318b63d
--- /dev/null
+++ b/testsuite/tests/th/T6018th.stderr
@@ -0,0 +1,6 @@
+| r_0 -> a_1
+
+T6018th.hs:98:4:
+    Type family equations violate injectivity annotation:
+      H Int Int Int = Bool
+      H Int Char Bool = Bool
diff --git a/testsuite/tests/th/T8028.hs b/testsuite/tests/th/T8028.hs
index 6145428aaf..c54f0e3dcf 100644
--- a/testsuite/tests/th/T8028.hs
+++ b/testsuite/tests/th/T8028.hs
@@ -12,6 +12,6 @@ $(x)
 -- subsequently be reified
 $(do f <- reify ''F
      case f of
-       FamilyI (ClosedTypeFamilyD _ _ _ []) _ -> return []
-       _                                      -> error $ show f
+       FamilyI (ClosedTypeFamilyD _ _ _ _ []) _ -> return []
+       _                                        -> error $ show f
  )
diff --git a/testsuite/tests/th/T8028a.hs b/testsuite/tests/th/T8028a.hs
index 928a96e52c..7845c13b71 100644
--- a/testsuite/tests/th/T8028a.hs
+++ b/testsuite/tests/th/T8028a.hs
@@ -3,4 +3,4 @@ module T8028a where
 import Language.Haskell.TH
 
 x = do n <- newName "F"
-       return [ClosedTypeFamilyD n [] Nothing []]
+       return [ClosedTypeFamilyD n [] NoSig Nothing []]
diff --git a/testsuite/tests/th/T8884.hs b/testsuite/tests/th/T8884.hs
index ca6ed9c4b1..acbd6208df 100644
--- a/testsuite/tests/th/T8884.hs
+++ b/testsuite/tests/th/T8884.hs
@@ -5,19 +5,20 @@ module T8884 where
 import Language.Haskell.TH
 import System.IO
 
-type family Foo a where
+type family Foo a = r | r -> a where
   Foo x = x
 
-type family Baz (a :: k)
+type family Baz (a :: k) = (r :: k) | r -> a
 type instance Baz x = x
 
-$( do FamilyI foo@(ClosedTypeFamilyD _ tvbs1 m_kind1 eqns1) [] <- reify ''Foo
-      FamilyI baz@(FamilyD TypeFam _ tvbs2 m_kind2)
+$( do FamilyI foo@(ClosedTypeFamilyD _ tvbs1 res1 m_kind1 eqns1)
+              [] <- reify ''Foo
+      FamilyI baz@(OpenTypeFamilyD _ tvbs2 res2 m_kind2)
               [inst@(TySynInstD _ eqn2)] <- reify ''Baz
       runIO $ putStrLn $ pprint foo
       runIO $ putStrLn $ pprint baz
       runIO $ putStrLn $ pprint inst
       runIO $ hFlush stdout
-      return [ ClosedTypeFamilyD (mkName "Foo'") tvbs1 m_kind1 eqns1
-             , FamilyD TypeFam (mkName "Baz'") tvbs2 m_kind2
+      return [ ClosedTypeFamilyD (mkName "Foo'") tvbs1 res1 m_kind1 eqns1
+             , OpenTypeFamilyD   (mkName "Baz'") tvbs2 res2 m_kind2
              , TySynInstD (mkName "Baz'") eqn2 ] )
diff --git a/testsuite/tests/th/T8884.stderr b/testsuite/tests/th/T8884.stderr
index 24fc15a81f..28be29951d 100644
--- a/testsuite/tests/th/T8884.stderr
+++ b/testsuite/tests/th/T8884.stderr
@@ -1,3 +1,4 @@
-type family T8884.Foo (a_0 :: k_1) :: k_1 where T8884.Foo x_2 = x_2
-type family T8884.Baz (a_0 :: k_1) :: *
-type instance T8884.Baz (x_0 :: *) = x_0
+type family T8884.Foo (a_0 :: k_1) = (r_2 :: k_1) | r_2 -> k_1 a_0 where
+    T8884.Foo x_3 = x_3
+type family T8884.Baz (a_0 :: k_1) = (r_2 :: k_1) | r_2 -> k_1 a_0
+type instance T8884.Baz (x_0 :: k_1) = x_0
diff --git a/testsuite/tests/th/TH_RichKinds2.hs b/testsuite/tests/th/TH_RichKinds2.hs
index b804688b6a..c77988c3bc 100644
--- a/testsuite/tests/th/TH_RichKinds2.hs
+++ b/testsuite/tests/th/TH_RichKinds2.hs
@@ -12,13 +12,13 @@ import Data.Char
 import Data.List
 import Language.Haskell.TH
 
-$(return [FamilyD TypeFam (mkName "Map") [KindedTV (mkName "f")
+$(return [OpenTypeFamilyD (mkName "Map") [KindedTV (mkName "f")
                                                    (AppT (AppT ArrowT (VarT (mkName "k1")))
                                                            (VarT (mkName "k2"))),
                                           KindedTV (mkName "l")
                                                    (AppT ListT
                                                          (VarT (mkName "k1")))]
-                                          (Just (AppT ListT (VarT (mkName "k2"))))])
+                                          (KindSig (AppT ListT (VarT (mkName "k2")))) Nothing])
 
 $( let fixKs :: String -> String -- need to remove TH renaming index from k variables
        fixKs s =
diff --git a/testsuite/tests/th/TH_reifyDecl1.hs b/testsuite/tests/th/TH_reifyDecl1.hs
index 7e7c9f40b9..c4ae3c065d 100644
--- a/testsuite/tests/th/TH_reifyDecl1.hs
+++ b/testsuite/tests/th/TH_reifyDecl1.hs
@@ -84,5 +84,3 @@ test = $(let
           ; display ''DF1
           ; display ''DF2
           ; [| () |] })
-
-
diff --git a/testsuite/tests/th/all.T b/testsuite/tests/th/all.T
index a43cf57f3d..dada44a325 100644
--- a/testsuite/tests/th/all.T
+++ b/testsuite/tests/th/all.T
@@ -351,3 +351,4 @@ test('T10704',
      extra_clean(['T10704a.o','T10704a.hi']),
      multimod_compile_and_run,
      ['T10704', '-v0'])
+test('T6018th', normal, compile_fail, ['-v0'])