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

4 files changed, 135 insertions, 47 deletions

diff --git a/libraries/template-haskell/Language/Haskell/TH/Lib.hs b/libraries/template-haskell/Language/Haskell/TH/Lib.hs
index 5d2b08c671..fd5dd70802 100644
--- a/libraries/template-haskell/Language/Haskell/TH/Lib.hs
+++ b/libraries/template-haskell/Language/Haskell/TH/Lib.hs
@@ -2,12 +2,14 @@
 -- TH.Lib contains lots of useful helper functions for
 -- generating and manipulating Template Haskell terms
 
+{-# LANGUAGE CPP #-}
+
 module Language.Haskell.TH.Lib where
     -- All of the exports from this module should
     -- be "public" functions.  The main module TH
     -- re-exports them all.
 
-import Language.Haskell.TH.Syntax hiding (Role)
+import Language.Haskell.TH.Syntax hiding (Role, InjectivityAnn)
 import qualified Language.Haskell.TH.Syntax as TH
 import Control.Monad( liftM, liftM2 )
 import Data.Word( Word8 )
@@ -40,6 +42,7 @@ type FieldExpQ      = Q FieldExp
 type RuleBndrQ      = Q RuleBndr
 type TySynEqnQ      = Q TySynEqn
 type Role           = TH.Role       -- must be defined here for DsMeta to find it
+type InjectivityAnn = TH.InjectivityAnn
 
 ----------------------------------------------------------
 -- * Lowercase pattern syntax functions
@@ -201,11 +204,6 @@ clause ps r ds = do { ps' <- sequence ps;
 dyn :: String -> ExpQ
 dyn s = return (VarE (mkName s))
 
-global :: Name -> ExpQ
-{-# DEPRECATED global "Use varE instead" #-}
--- Trac #8656; I have no idea why this function is duplicated
-global s = return (VarE s)
-
 varE :: Name -> ExpQ
 varE s = return (VarE s)
 
@@ -422,12 +420,6 @@ pragAnnD target expr
 pragLineD :: Int -> String -> DecQ
 pragLineD line file = return $ PragmaD $ LineP line file
 
-familyNoKindD :: FamFlavour -> Name -> [TyVarBndr] -> DecQ
-familyNoKindD flav tc tvs = return $ FamilyD flav tc tvs Nothing
-
-familyKindD :: FamFlavour -> Name -> [TyVarBndr] -> Kind -> DecQ
-familyKindD flav tc tvs k = return $ FamilyD flav tc tvs (Just k)
-
 dataInstD :: CxtQ -> Name -> [TypeQ] -> [ConQ] -> [Name] -> DecQ
 dataInstD ctxt tc tys cons derivs =
   do
@@ -450,17 +442,57 @@ tySynInstD tc eqn =
     eqn1 <- eqn
     return (TySynInstD tc eqn1)
 
+dataFamilyD :: Name -> [TyVarBndr] -> Maybe Kind -> DecQ
+dataFamilyD tc tvs kind
+    = return $ DataFamilyD tc tvs kind
+
+openTypeFamilyD :: Name -> [TyVarBndr] -> FamilyResultSig
+                -> Maybe InjectivityAnn -> DecQ
+openTypeFamilyD tc tvs res inj
+    = return $ OpenTypeFamilyD tc tvs res inj
+
+closedTypeFamilyD :: Name -> [TyVarBndr] -> FamilyResultSig
+                  -> Maybe InjectivityAnn -> [TySynEqnQ] -> DecQ
+closedTypeFamilyD tc tvs result injectivity eqns =
+  do eqns1 <- sequence eqns
+     return (ClosedTypeFamilyD tc tvs result injectivity eqns1)
+
+-- These were deprecated in GHC 7.12 with a plan to remove them in 7.14. If you
+-- remove this check please also:
+--   1. remove deprecated functions
+--   2. remove CPP language extension from top of this module
+--   3. remove the FamFlavour data type from Syntax module
+--   4. make sure that all references to FamFlavour are gone from DsMeta,
+--      Convert, TcSplice (follows from 3)
+#if __GLASGOW_HASKELL__ > 712
+#error Remove deprecated familyNoKindD, familyKindD, closedTypeFamilyNoKindD and closedTypeFamilyKindD
+#endif
+
+{-# DEPRECATED familyNoKindD, familyKindD
+               "This function will be removed in the next stable release. Use openTypeFamilyD/dataFamilyD instead." #-}
+familyNoKindD :: FamFlavour -> Name -> [TyVarBndr] -> DecQ
+familyNoKindD flav tc tvs =
+    case flav of
+      TypeFam -> return $ OpenTypeFamilyD tc tvs NoSig Nothing
+      DataFam -> return $ DataFamilyD tc tvs Nothing
+
+familyKindD :: FamFlavour -> Name -> [TyVarBndr] -> Kind -> DecQ
+familyKindD flav tc tvs k =
+    case flav of
+      TypeFam -> return $ OpenTypeFamilyD tc tvs (KindSig k) Nothing
+      DataFam -> return $ DataFamilyD tc tvs (Just k)
+
+{-# DEPRECATED closedTypeFamilyNoKindD, closedTypeFamilyKindD
+               "This function will be removed in the next stable release. Use closedTypeFamilyD instead." #-}
 closedTypeFamilyNoKindD :: Name -> [TyVarBndr] -> [TySynEqnQ] -> DecQ
 closedTypeFamilyNoKindD tc tvs eqns =
-  do
-    eqns1 <- sequence eqns
-    return (ClosedTypeFamilyD tc tvs Nothing eqns1)
+ do eqns1 <- sequence eqns
+    return (ClosedTypeFamilyD tc tvs NoSig Nothing eqns1)
 
 closedTypeFamilyKindD :: Name -> [TyVarBndr] -> Kind -> [TySynEqnQ] -> DecQ
 closedTypeFamilyKindD tc tvs kind eqns =
-  do
-    eqns1 <- sequence eqns
-    return (ClosedTypeFamilyD tc tvs (Just kind) eqns1)
+ do eqns1 <- sequence eqns
+    return (ClosedTypeFamilyD tc tvs (KindSig kind) Nothing eqns1)
 
 roleAnnotD :: Name -> [Role] -> DecQ
 roleAnnotD name roles = return $ RoleAnnotD name roles
@@ -653,6 +685,24 @@ constraintK :: Kind
 constraintK = ConstraintT
 
 -------------------------------------------------------------------------------
+-- *   Type family result
+
+noSig :: FamilyResultSig
+noSig = NoSig
+
+kindSig :: Kind -> FamilyResultSig
+kindSig = KindSig
+
+tyVarSig :: TyVarBndr -> FamilyResultSig
+tyVarSig = TyVarSig
+
+-------------------------------------------------------------------------------
+-- *   Injectivity annotation
+
+injectivityAnn :: Name -> [Name] -> InjectivityAnn
+injectivityAnn = TH.InjectivityAnn
+
+-------------------------------------------------------------------------------
 -- *   Role
 
 nominalR, representationalR, phantomR, inferR :: Role
diff --git a/libraries/template-haskell/Language/Haskell/TH/Ppr.hs b/libraries/template-haskell/Language/Haskell/TH/Ppr.hs
index 5fb7197bc7..589382aac3 100644
--- a/libraries/template-haskell/Language/Haskell/TH/Ppr.hs
+++ b/libraries/template-haskell/Language/Haskell/TH/Ppr.hs
@@ -66,7 +66,7 @@ instance Ppr Info where
               case mb_d of { Nothing -> empty; Just d -> ppr d }]
 
 ppr_sig :: Name -> Type -> Doc
-ppr_sig v ty = ppr v <+> text "::" <+> ppr ty
+ppr_sig v ty = ppr v <+> dcolon <+> ppr ty
 
 pprFixity :: Name -> Fixity -> Doc
 pprFixity _ f | f == defaultFixity = empty
@@ -167,7 +167,7 @@ pprExp _ (CompE ss) = text "[" <> ppr s
           ss' = init ss
 pprExp _ (ArithSeqE d) = ppr d
 pprExp _ (ListE es) = brackets $ sep $ punctuate comma $ map ppr es
-pprExp i (SigE e t) = parensIf (i > noPrec) $ ppr e <+> text "::" <+> ppr t
+pprExp i (SigE e t) = parensIf (i > noPrec) $ ppr e <+> dcolon <+> ppr t
 pprExp _ (RecConE nm fs) = ppr nm <> braces (pprFields fs)
 pprExp _ (RecUpdE e fs) = pprExp appPrec e <> braces (pprFields fs)
 pprExp i (StaticE e) = parensIf (i >= appPrec) $
@@ -267,7 +267,7 @@ pprPat _ (RecP nm fs)
             <+> braces (sep $ punctuate comma $
                         map (\(s,p) -> ppr s <+> equals <+> ppr p) fs)
 pprPat _ (ListP ps) = brackets $ sep $ punctuate comma $ map ppr ps
-pprPat i (SigP p t) = parensIf (i > noPrec) $ ppr p <+> text "::" <+> ppr t
+pprPat i (SigP p t) = parensIf (i > noPrec) $ ppr p <+> dcolon <+> ppr t
 pprPat _ (ViewP e p) = parens $ pprExp noPrec e <+> text "->" <+> pprPat noPrec p
 
 ------------------------------
@@ -291,18 +291,17 @@ ppr_dec _  (ClassD ctxt c xs fds ds)
     $$ where_clause ds
 ppr_dec _ (InstanceD ctxt i ds) = text "instance" <+> pprCxt ctxt <+> ppr i
                                   $$ where_clause ds
-ppr_dec _ (SigD f t)    = pprPrefixOcc f <+> text "::" <+> ppr t
+ppr_dec _ (SigD f t)    = pprPrefixOcc f <+> dcolon <+> ppr t
 ppr_dec _ (ForeignD f)  = ppr f
 ppr_dec _ (InfixD fx n) = pprFixity n fx
 ppr_dec _ (PragmaD p)   = ppr p
-ppr_dec isTop (FamilyD flav tc tvs k)
-  = ppr flav <+> maybeFamily <+> ppr tc <+> hsep (map ppr tvs) <+> maybeKind
+ppr_dec isTop (DataFamilyD tc tvs kind)
+  = text "data" <+> maybeFamily <+> ppr tc <+> hsep (map ppr tvs) <+> maybeKind
   where
     maybeFamily | isTop     = text "family"
                 | otherwise = empty
-
-    maybeKind | (Just k') <- k = text "::" <+> ppr k'
-              | otherwise      = empty
+    maybeKind | (Just k') <- kind = dcolon <+> ppr k'
+              | otherwise = empty
 ppr_dec isTop (DataInstD ctxt tc tys cs decs)
   = ppr_data maybeInst ctxt tc (sep (map pprParendType tys)) cs decs
   where
@@ -318,13 +317,21 @@ ppr_dec isTop (TySynInstD tc (TySynEqn tys rhs))
   where
     maybeInst | isTop     = text "instance"
               | otherwise = empty
-ppr_dec _ (ClosedTypeFamilyD tc tvs mkind eqns)
-  = hang (hsep [ text "type family", ppr tc, hsep (map ppr tvs), maybeKind
-               , text "where" ])
+ppr_dec isTop (OpenTypeFamilyD tc tvs res inj)
+  = text "type" <+> maybeFamily <+> ppr tc <+> hsep (map ppr tvs) <+>
+    ppr res <+> maybeInj
+  where
+    maybeFamily | isTop     = text "family"
+                | otherwise = empty
+    maybeInj | (Just inj') <- inj = ppr inj'
+             | otherwise          = empty
+ppr_dec _ (ClosedTypeFamilyD tc tvs res inj eqns)
+  = hang (hsep [ text "type family", ppr tc, hsep (map ppr tvs), ppr res
+               , maybeInj, text "where" ])
       nestDepth (vcat (map ppr_eqn eqns))
   where
-    maybeKind | (Just k') <- mkind = text "::" <+> ppr k'
-              | otherwise          = empty
+    maybeInj | (Just inj') <- inj = ppr inj'
+             | otherwise          = empty
     ppr_eqn (TySynEqn lhs rhs)
       = ppr tc <+> sep (map pprParendType lhs) <+> text "=" <+> ppr rhs
 
@@ -335,7 +342,7 @@ ppr_dec _ (StandaloneDerivD cxt ty)
   = hsep [ text "deriving instance", pprCxt cxt, ppr ty ]
 
 ppr_dec _ (DefaultSigD n ty)
-  = hsep [ text "default", pprPrefixOcc n, text "::", ppr ty ]
+  = hsep [ text "default", pprPrefixOcc n, dcolon, ppr ty ]
 
 ppr_data :: Doc -> Cxt -> Name -> Doc -> [Con] -> [Name] -> Doc
 ppr_data maybeInst ctxt t argsDoc cs decs
@@ -381,6 +388,17 @@ instance Ppr FamFlavour where
     ppr TypeFam = text "type"
 
 ------------------------------
+instance Ppr FamilyResultSig where
+    ppr NoSig           = empty
+    ppr (KindSig k)     = dcolon <+> ppr k
+    ppr (TyVarSig bndr) = text "=" <+> ppr bndr
+
+------------------------------
+instance Ppr InjectivityAnn where
+    ppr (InjectivityAnn lhs rhs) =
+        char '|' <+> ppr lhs <+> text "->" <+> hsep (map ppr rhs)
+
+------------------------------
 instance Ppr Foreign where
     ppr (ImportF callconv safety impent as typ)
        = text "foreign import"
@@ -388,13 +406,13 @@ instance Ppr Foreign where
      <+> showtextl safety
      <+> text (show impent)
      <+> ppr as
-     <+> text "::" <+> ppr typ
+     <+> dcolon <+> ppr typ
     ppr (ExportF callconv expent as typ)
         = text "foreign export"
       <+> showtextl callconv
       <+> text (show expent)
       <+> ppr as
-      <+> text "::" <+> ppr typ
+      <+> dcolon <+> ppr typ
 
 ------------------------------
 instance Ppr Pragma where
@@ -409,7 +427,7 @@ instance Ppr Pragma where
        =   text "{-# SPECIALISE"
        <+> maybe empty ppr inline
        <+> ppr phases
-       <+> sep [ ppr n <+> text "::"
+       <+> sep [ ppr n <+> dcolon
                , nest 2 $ ppr ty ]
        <+> text "#-}"
     ppr (SpecialiseInstP inst)
@@ -450,7 +468,7 @@ instance Ppr Phases where
 ------------------------------
 instance Ppr RuleBndr where
     ppr (RuleVar n)         = ppr n
-    ppr (TypedRuleVar n ty) = parens $ ppr n <+> text "::" <+> ppr ty
+    ppr (TypedRuleVar n ty) = parens $ ppr n <+> dcolon <+> ppr ty
 
 ------------------------------
 instance Ppr Clause where
@@ -471,7 +489,7 @@ instance Ppr Con where
 ------------------------------
 pprVarStrictType :: (Name, Strict, Type) -> Doc
 -- Slight infelicity: with print non-atomic type with parens
-pprVarStrictType (v, str, t) = ppr v <+> text "::" <+> pprStrictType (str, t)
+pprVarStrictType (v, str, t) = ppr v <+> dcolon <+> pprStrictType (str, t)
 
 ------------------------------
 pprStrictType :: (Strict, Type) -> Doc
@@ -524,7 +542,6 @@ parens around it.  E.g. the parens are required here:
    type instance F Int = (Bool :: *)
 So we always print a SigT with parens (see Trac #10050). -}
 
-
 pprTyApp :: (Type, [Type]) -> Doc
 pprTyApp (ArrowT, [arg1,arg2]) = sep [pprFunArgType arg1 <+> text "->", ppr arg2]
 pprTyApp (EqualityT, [arg1, arg2]) =
@@ -558,7 +575,7 @@ instance Ppr TyLit where
 ------------------------------
 instance Ppr TyVarBndr where
     ppr (PlainTV nm)    = ppr nm
-    ppr (KindedTV nm k) = parens (ppr nm <+> text "::" <+> ppr k)
+    ppr (KindedTV nm k) = parens (ppr nm <+> dcolon <+> ppr k)
 
 instance Ppr Role where
     ppr NominalR          = text "nominal"
diff --git a/libraries/template-haskell/Language/Haskell/TH/PprLib.hs b/libraries/template-haskell/Language/Haskell/TH/PprLib.hs
index 68134965a5..8019e48205 100644
--- a/libraries/template-haskell/Language/Haskell/TH/PprLib.hs
+++ b/libraries/template-haskell/Language/Haskell/TH/PprLib.hs
@@ -10,7 +10,7 @@ module Language.Haskell.TH.PprLib (
 
         -- * Primitive Documents
         empty,
-        semi, comma, colon, space, equals, arrow,
+        semi, comma, colon, dcolon, space, equals, arrow,
         lparen, rparen, lbrack, rbrack, lbrace, rbrace,
 
         -- * Converting values into documents
@@ -27,7 +27,7 @@ module Language.Haskell.TH.PprLib (
         fsep, fcat, 
         nest,
         hang, punctuate,
-        
+
         -- * Predicates on documents
         isEmpty,
 
@@ -63,6 +63,7 @@ empty   :: Doc;                 -- ^ An empty document
 semi    :: Doc;                 -- ^ A ';' character
 comma   :: Doc;                 -- ^ A ',' character
 colon   :: Doc;                 -- ^ A ':' character
+dcolon  :: Doc;                 -- ^ A "::" string
 space   :: Doc;                 -- ^ A space character
 equals  :: Doc;                 -- ^ A '=' character
 arrow   :: Doc;                 -- ^ A "->" string
@@ -171,6 +172,7 @@ empty = return HPJ.empty
 semi = return HPJ.semi
 comma = return HPJ.comma
 colon = return HPJ.colon
+dcolon = return $ HPJ.text "::"
 space = return HPJ.space
 equals = return HPJ.equals
 arrow = return $ HPJ.text "->"
diff --git a/libraries/template-haskell/Language/Haskell/TH/Syntax.hs b/libraries/template-haskell/Language/Haskell/TH/Syntax.hs
index 9f7b5107f0..82e22dd212 100644
--- a/libraries/template-haskell/Language/Haskell/TH/Syntax.hs
+++ b/libraries/template-haskell/Language/Haskell/TH/Syntax.hs
@@ -1367,9 +1367,10 @@ data Dec
   -- | pragmas
   | PragmaD Pragma                -- ^ @{ {\-# INLINE [1] foo #-\} }@
 
-  -- | type families (may also appear in [Dec] of 'ClassD' and 'InstanceD')
-  | FamilyD FamFlavour Name
-         [TyVarBndr] (Maybe Kind) -- ^ @{ type family T a b c :: * }@
+  -- | data families (may also appear in [Dec] of 'ClassD' and 'InstanceD')
+  | DataFamilyD Name [TyVarBndr]
+               (Maybe Kind)
+         -- ^ @{ data family T a b c :: * }@
 
   | DataInstD Cxt Name [Type]
          [Con] [Name]             -- ^ @{ data instance Cxt x => T [x] = A x
@@ -1380,9 +1381,17 @@ data Dec
                                   --       deriving (Z,W)}@
   | TySynInstD Name TySynEqn      -- ^ @{ type instance ... }@
 
+  -- | open type families (may also appear in [Dec] of 'ClassD' and 'InstanceD')
+  | OpenTypeFamilyD Name
+         [TyVarBndr] FamilyResultSig
+         (Maybe InjectivityAnn)
+         -- ^ @{ type family T a b c = (r :: *) | r -> a b }@
+
   | ClosedTypeFamilyD Name
-      [TyVarBndr] (Maybe Kind)
-      [TySynEqn]                  -- ^ @{ type family F a b :: * where ... }@
+      [TyVarBndr] FamilyResultSig
+      (Maybe InjectivityAnn)
+      [TySynEqn]
+       -- ^ @{ type family F a b = (r :: *) | r -> a where ... }@
 
   | RoleAnnotD Name [Role]        -- ^ @{ type role T nominal representational }@
   | StandaloneDerivD Cxt Type     -- ^ @{ deriving instance Ord a => Ord (Foo a) }@
@@ -1493,6 +1502,16 @@ data TyVarBndr = PlainTV  Name            -- ^ @a@
                | KindedTV Name Kind       -- ^ @(a :: k)@
       deriving( Show, Eq, Ord, Data, Typeable, Generic )
 
+-- | Type family result signature
+data FamilyResultSig = NoSig              -- ^ no signature
+                     | KindSig  Kind      -- ^ @k@
+                     | TyVarSig TyVarBndr -- ^ @= r, = (r :: k)@
+      deriving( Show, Eq, Ord, Data, Typeable, Generic )
+
+-- | Injectivity annotation
+data InjectivityAnn = InjectivityAnn Name [Name]
+  deriving ( Show, Eq, Ord, Data, Typeable, Generic )
+
 data TyLit = NumTyLit Integer             -- ^ @2@
            | StrTyLit String              -- ^ @"Hello"@
   deriving ( Show, Eq, Ord, Data, Typeable, Generic )