Permit empty closed type families

Fixes #9840 and #10306, and includes an alternative resolution to #8028.
This permits empty closed type families, and documents them in the user
guide. It updates the Haddock submodule to support the API change.

Test Plan: Added `indexed-types/should_compile/T9840` and updated
`indexed-types/should_fail/ClosedFam4` and `th/T8028`.

Reviewers: austin, simonpj, goldfire

Reviewed By: goldfire

Subscribers: bgamari, jstolarek, thomie, goldfire

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

GHC Trac Issues: #9840, #10306

compiler/deSugar/DsMeta.hs

@@ -316,18 +316,20 @@ repSynDecl tc bndrs ty
        ; repTySyn tc bndrs ty1 }
 
 repFamilyDecl :: LFamilyDecl Name -> DsM (SrcSpan, Core TH.DecQ)
-repFamilyDecl (L loc (FamilyDecl { fdInfo    = info,
-                                   fdLName   = tc,
-                                   fdTyVars  = tvs,
-                                   fdKindSig = opt_kind }))
+repFamilyDecl decl@(L loc (FamilyDecl { fdInfo  = info,
+                                        fdLName   = tc,
+                                        fdTyVars  = tvs,
+                                        fdKindSig = opt_kind }))
   = do { tc1 <- lookupLOcc tc           -- See note [Binders and occurrences]
        ; dec <- addTyClTyVarBinds tvs $ \bndrs ->
            case (opt_kind, info) of
-                  (Nothing, ClosedTypeFamily eqns) ->
+                  (_      , ClosedTypeFamily Nothing) ->
+                    notHandled "abstract closed type family" (ppr decl)
+                  (Nothing, ClosedTypeFamily (Just eqns)) ->
                     do { eqns1 <- mapM repTyFamEqn eqns
                        ; eqns2 <- coreList tySynEqnQTyConName eqns1
                        ; repClosedFamilyNoKind tc1 bndrs eqns2 }
-                  (Just ki, ClosedTypeFamily eqns) ->
+                  (Just ki, ClosedTypeFamily (Just eqns)) ->
                     do { eqns1 <- mapM repTyFamEqn eqns
                        ; eqns2 <- coreList tySynEqnQTyConName eqns1
                        ; ki1 <- repLKind ki

compiler/hsSyn/Convert.hs

@@ -296,14 +296,11 @@ cvtDec (TySynInstD tc eqn)
                                         , tfid_fvs = placeHolderNames } } }
 
 cvtDec (ClosedTypeFamilyD tc tyvars mkind eqns)
-  | not $ null eqns
   = do { (_, tc', tvs') <- cvt_tycl_hdr [] tc tyvars
        ; mkind' <- cvtMaybeKind mkind
        ; eqns' <- mapM (cvtTySynEqn tc') eqns
        ; returnJustL $ TyClD $ FamDecl $
-         FamilyDecl (ClosedTypeFamily eqns') tc' tvs' mkind' }
-  | otherwise
-  = failWith (ptext (sLit "Illegal empty closed type family"))
+         FamilyDecl (ClosedTypeFamily (Just eqns')) tc' tvs' mkind' }
 
 cvtDec (TH.RoleAnnotD tc roles)
   = do { tc' <- tconNameL tc

compiler/hsSyn/HsDecls.hs

@@ -557,9 +557,9 @@ deriving instance (DataId id) => Data (FamilyDecl id)
 data FamilyInfo name
   = DataFamily
   | OpenTypeFamily
-     -- this list might be empty, if we're in an hs-boot file and the user
+     -- | 'Nothing' if we're in an hs-boot file and the user
      -- said "type family Foo x where .."
-  | ClosedTypeFamily [LTyFamInstEqn name]
+  | ClosedTypeFamily (Maybe [LTyFamInstEqn name])
   deriving( Typeable )
 deriving instance (DataId name) => Data (FamilyInfo name)
 
@@ -739,11 +739,12 @@ instance (OutputableBndr name) => Outputable (FamilyDecl name) where
                       Nothing   -> empty
                       Just kind -> dcolon <+> ppr kind
           (pp_where, pp_eqns) = case info of
-            ClosedTypeFamily eqns -> ( ptext (sLit "where")
-                                     , if null eqns
-                                       then ptext (sLit "..")
-                                       else vcat $ map ppr_fam_inst_eqn eqns )
-            _                     -> (empty, empty)
+            ClosedTypeFamily mb_eqns ->
+              ( ptext (sLit "where")
+              , case mb_eqns of
+                  Nothing   -> ptext (sLit "..")
+                  Just eqns -> vcat $ map ppr_fam_inst_eqn eqns )
+            _ -> (empty, empty)
 
 pprFlavour :: FamilyInfo name -> SDoc
 pprFlavour DataFamily            = ptext (sLit "data family")

compiler/iface/IfaceSyn.hs

@@ -154,8 +154,9 @@ data IfaceTyConParent
 
 data IfaceFamTyConFlav
   = IfaceOpenSynFamilyTyCon
-  | IfaceClosedSynFamilyTyCon IfExtName       -- name of associated axiom
-                              [IfaceAxBranch] -- for pretty printing purposes only
+  | IfaceClosedSynFamilyTyCon (Maybe (IfExtName, [IfaceAxBranch]))
+    -- ^ Name of associated axiom and branches for pretty printing purposes,
+    -- or 'Nothing' for an empty closed family without an axiom
   | IfaceAbstractClosedSynFamilyTyCon
   | IfaceBuiltInSynFamTyCon -- for pretty printing purposes only
 
@@ -682,13 +683,16 @@ pprIfaceDecl ss (IfaceFamily { ifName = tycon, ifTyVars = tyvars
               2 (ppr kind <+> ppShowRhs ss (pp_rhs rhs))
          , ppShowRhs ss (nest 2 (pp_branches rhs)) ]
   where
-    pp_rhs IfaceOpenSynFamilyTyCon             = ppShowIface ss (ptext (sLit "open"))
-    pp_rhs IfaceAbstractClosedSynFamilyTyCon   = ppShowIface ss (ptext (sLit "closed, abstract"))
-    pp_rhs (IfaceClosedSynFamilyTyCon _ (_:_)) = ptext (sLit "where")
-    pp_rhs IfaceBuiltInSynFamTyCon = ppShowIface ss (ptext (sLit "built-in"))
-    pp_rhs _ = panic "pprIfaceDecl syn"
-
-    pp_branches (IfaceClosedSynFamilyTyCon ax brs)
+    pp_rhs IfaceOpenSynFamilyTyCon
+      = ppShowIface ss (ptext (sLit "open"))
+    pp_rhs IfaceAbstractClosedSynFamilyTyCon
+      = ppShowIface ss (ptext (sLit "closed, abstract"))
+    pp_rhs (IfaceClosedSynFamilyTyCon _)
+      = ptext (sLit "where")
+    pp_rhs IfaceBuiltInSynFamTyCon
+      = ppShowIface ss (ptext (sLit "built-in"))
+
+    pp_branches (IfaceClosedSynFamilyTyCon (Just (ax, brs)))
       = vcat (map (pprAxBranch (pprPrefixIfDeclBndr ss tycon)) brs)
         $$ ppShowIface ss (ptext (sLit "axiom") <+> ppr ax)
     pp_branches _ = Outputable.empty
@@ -1090,8 +1094,9 @@ freeNamesIfIdDetails _                 = emptyNameSet
 -- All other changes are handled via the version info on the tycon
 freeNamesIfFamFlav :: IfaceFamTyConFlav -> NameSet
 freeNamesIfFamFlav IfaceOpenSynFamilyTyCon           = emptyNameSet
-freeNamesIfFamFlav (IfaceClosedSynFamilyTyCon ax br)
+freeNamesIfFamFlav (IfaceClosedSynFamilyTyCon (Just (ax, br)))
   = unitNameSet ax &&& fnList freeNamesIfAxBranch br
+freeNamesIfFamFlav (IfaceClosedSynFamilyTyCon Nothing) = emptyNameSet
 freeNamesIfFamFlav IfaceAbstractClosedSynFamilyTyCon = emptyNameSet
 freeNamesIfFamFlav IfaceBuiltInSynFamTyCon = emptyNameSet
 
@@ -1440,8 +1445,7 @@ instance Binary IfaceDecl where
 
 instance Binary IfaceFamTyConFlav where
     put_ bh IfaceOpenSynFamilyTyCon           = putByte bh 0
-    put_ bh (IfaceClosedSynFamilyTyCon ax br) = putByte bh 1 >> put_ bh ax
-                                                             >> put_ bh br
+    put_ bh (IfaceClosedSynFamilyTyCon mb)    = putByte bh 1 >> put_ bh mb
     put_ bh IfaceAbstractClosedSynFamilyTyCon = putByte bh 2
     put_ _ IfaceBuiltInSynFamTyCon
         = pprPanic "Cannot serialize IfaceBuiltInSynFamTyCon, used for pretty-printing only" Outputable.empty
@@ -1449,9 +1453,8 @@ instance Binary IfaceFamTyConFlav where
     get bh = do { h <- getByte bh
                 ; case h of
                     0 -> return IfaceOpenSynFamilyTyCon
-                    1 -> do { ax <- get bh
-                            ; br <- get bh
-                            ; return (IfaceClosedSynFamilyTyCon ax br) }
+                    1 -> do { mb <- get bh
+                            ; return (IfaceClosedSynFamilyTyCon mb) }
                     _ -> return IfaceAbstractClosedSynFamilyTyCon }
 
 instance Binary IfaceClassOp where

compiler/iface/MkIface.hs

@@ -1675,10 +1675,13 @@ tyConToIfaceDecl env tycon
                Nothing           -> IfNoParent
 
     to_if_fam_flav OpenSynFamilyTyCon        = IfaceOpenSynFamilyTyCon
-    to_if_fam_flav (ClosedSynFamilyTyCon ax) = IfaceClosedSynFamilyTyCon axn ibr
+    to_if_fam_flav (ClosedSynFamilyTyCon (Just ax))
+      = IfaceClosedSynFamilyTyCon (Just (axn, ibr))
       where defs = fromBranchList $ coAxiomBranches ax
             ibr  = map (coAxBranchToIfaceBranch' tycon) defs
             axn  = coAxiomName ax
+    to_if_fam_flav (ClosedSynFamilyTyCon Nothing)
+      = IfaceClosedSynFamilyTyCon Nothing
     to_if_fam_flav AbstractClosedSynFamilyTyCon
       = IfaceAbstractClosedSynFamilyTyCon
 

compiler/iface/TcIface.hs

@@ -358,8 +358,8 @@ tc_iface_decl parent _ (IfaceFamily {ifName = occ_name, ifTyVars = tv_bndrs,
    where
      mk_doc n = ptext (sLit "Type synonym") <+> ppr n
      tc_fam_flav IfaceOpenSynFamilyTyCon   = return OpenSynFamilyTyCon
-     tc_fam_flav (IfaceClosedSynFamilyTyCon ax_name _)
-       = do { ax <- tcIfaceCoAxiom ax_name
+     tc_fam_flav (IfaceClosedSynFamilyTyCon mb_ax_name_branches)
+       = do { ax <- traverse (tcIfaceCoAxiom . fst) mb_ax_name_branches
             ; return (ClosedSynFamilyTyCon ax) }
      tc_fam_flav IfaceAbstractClosedSynFamilyTyCon
          = return AbstractClosedSynFamilyTyCon

compiler/main/HscTypes.hs

@@ -1722,7 +1722,7 @@ extras_plus thing = thing : implicitTyThings thing
 implicitCoTyCon :: TyCon -> [TyThing]
 implicitCoTyCon tc
   | Just co <- newTyConCo_maybe tc = [ACoAxiom $ toBranchedAxiom co]
-  | Just co <- isClosedSynFamilyTyCon_maybe tc
+  | Just co <- isClosedSynFamilyTyConWithAxiom_maybe tc
                                    = [ACoAxiom co]
   | otherwise                      = []
 

compiler/parser/Parser.y

@@ -1009,17 +1009,17 @@ where_type_family :: { Located ([AddAnn],FamilyInfo RdrName) }
         : {- empty -}                      { noLoc ([],OpenTypeFamily) }
         | 'where' ty_fam_inst_eqn_list
                { sLL $1 $> (mj AnnWhere $1:(fst $ unLoc $2)
-                    ,ClosedTypeFamily (reverse (snd $ unLoc $2))) }
+                    ,ClosedTypeFamily (fmap reverse $ snd $ unLoc $2)) }
 
-ty_fam_inst_eqn_list :: { Located ([AddAnn],[LTyFamInstEqn RdrName]) }
+ty_fam_inst_eqn_list :: { Located ([AddAnn],Maybe [LTyFamInstEqn RdrName]) }
         :     '{' ty_fam_inst_eqns '}'     { sLL $1 $> ([moc $1,mcc $3]
-                                                ,unLoc $2) }
+                                                ,Just (unLoc $2)) }
         | vocurly ty_fam_inst_eqns close   { let L loc _ = $2 in
-                                             L loc ([],unLoc $2) }
+                                             L loc ([],Just (unLoc $2)) }
         |     '{' '..' '}'                 { sLL $1 $> ([moc $1,mj AnnDotdot $2
-                                                 ,mcc $3],[]) }
+                                                 ,mcc $3],Nothing) }
         | vocurly '..' close               { let L loc _ = $2 in
-                                             L loc ([mj AnnDotdot $2],[]) }
+                                             L loc ([mj AnnDotdot $2],Nothing) }
 
 ty_fam_inst_eqns :: { Located [LTyFamInstEqn RdrName] }
         : ty_fam_inst_eqns ';' ty_fam_inst_eqn
@@ -1028,6 +1028,7 @@ ty_fam_inst_eqns :: { Located [LTyFamInstEqn RdrName] }
         | ty_fam_inst_eqns ';'        {% addAnnotation (gl $1) AnnSemi (gl $2)
                                          >> return (sLL $1 $>  (unLoc $1)) }
         | ty_fam_inst_eqn             { sLL $1 $> [$1] }
+        | {- empty -}                 { noLoc [] }
 
 ty_fam_inst_eqn :: { LTyFamInstEqn RdrName }
         : type '=' ctype

compiler/prelude/TysPrim.hs

@@ -772,7 +772,7 @@ anyTy = mkTyConTy anyTyCon
 
 anyTyCon :: TyCon
 anyTyCon = mkFamilyTyCon anyTyConName kind [kKiVar]
-                         AbstractClosedSynFamilyTyCon
+                         (ClosedSynFamilyTyCon Nothing)
                          NoParentTyCon
   where
     kind = ForAllTy kKiVar (mkTyVarTy kKiVar)

compiler/rename/RnSource.hs

@@ -1214,10 +1214,12 @@ rnFamDecl mb_cls (FamilyDecl { fdLName = tycon, fdTyVars = tyvars
      fmly_doc = TyFamilyCtx tycon
      kvs = extractRdrKindSigVars kind
 
-     rn_info (ClosedTypeFamily eqns)
+     rn_info (ClosedTypeFamily (Just eqns))
        = do { (eqns', fvs) <- rnList (rnTyFamInstEqn Nothing) eqns
                                                     -- no class context,
-            ; return (ClosedTypeFamily eqns', fvs) }
+            ; return (ClosedTypeFamily (Just eqns'), fvs) }
+     rn_info (ClosedTypeFamily Nothing)
+       = return (ClosedTypeFamily Nothing, emptyFVs)
      rn_info OpenTypeFamily = return (OpenTypeFamily, emptyFVs)
      rn_info DataFamily     = return (DataFamily, emptyFVs)
 

compiler/typecheck/TcRnDriver.hs

@@ -1036,8 +1036,11 @@ checkBootTyCon tc1 tc2
         pname1 = quotes (ppr name1)
         pname2 = quotes (ppr name2)
 
-    eqClosedFamilyAx (CoAxiom { co_ax_branches = branches1 })
-                     (CoAxiom { co_ax_branches = branches2 })
+    eqClosedFamilyAx Nothing Nothing  = True
+    eqClosedFamilyAx Nothing (Just _) = False
+    eqClosedFamilyAx (Just _) Nothing = False
+    eqClosedFamilyAx (Just (CoAxiom { co_ax_branches = branches1 }))
+                     (Just (CoAxiom { co_ax_branches = branches2 }))
       =  brListLength branches1 == brListLength branches2
       && (and $ brListZipWith eqClosedFamilyBranch branches1 branches2)
 

compiler/typecheck/TcSplice.hs

@@ -1336,14 +1336,15 @@ reifyFunDep (xs, ys) = TH.FunDep (map reifyName xs) (map reifyName ys)
 reifyFamFlavour :: TyCon -> TcM (Either TH.FamFlavour [TH.TySynEqn])
 reifyFamFlavour tc
   | isOpenTypeFamilyTyCon tc = return $ Left TH.TypeFam
-  | isDataFamilyTyCon    tc = return $ Left TH.DataFam
-
-    -- this doesn't really handle abstract closed families, but let's not worry
-    -- about that now
-  | Just ax <- isClosedSynFamilyTyCon_maybe tc
-  = do { eqns <- brListMapM reifyAxBranch $ coAxiomBranches ax
-       ; return $ Right eqns }
-
+  | isDataFamilyTyCon     tc = return $ Left TH.DataFam
+  | Just flav <- famTyConFlav_maybe tc = case flav of
+      OpenSynFamilyTyCon           -> return $ Left TH.TypeFam
+      AbstractClosedSynFamilyTyCon -> return $ Right []
+      BuiltInSynFamTyCon _         -> return $ Right []
+      ClosedSynFamilyTyCon Nothing -> return $ Right []
+      ClosedSynFamilyTyCon (Just ax)
+        -> do { eqns <- brListMapM reifyAxBranch $ coAxiomBranches ax
+              ; return $ Right eqns }
   | otherwise
   = panic "TcSplice.reifyFamFlavour: not a type family"
 

compiler/typecheck/TcTyClsDecls.hs

@@ -492,7 +492,7 @@ kcTyClDecl (ClassDecl { tcdLName = L _ name, tcdTyVars = hs_tvs
 -- do anything here
 kcTyClDecl (FamDecl (FamilyDecl { fdLName  = L _ fam_tc_name
                                 , fdTyVars = hs_tvs
-                                , fdInfo   = ClosedTypeFamily eqns }))
+                                , fdInfo   = ClosedTypeFamily (Just eqns) }))
   = do { tc_kind <- kcLookupKind fam_tc_name
        ; let fam_tc_shape = ( fam_tc_name, length (hsQTvBndrs hs_tvs), tc_kind)
        ; mapM_ (kcTyFamInstEqn fam_tc_shape) eqns }
@@ -673,11 +673,10 @@ tcFamDecl1 parent
   ; return [ATyCon tycon] }
 
 tcFamDecl1 parent
-            (FamilyDecl { fdInfo = ClosedTypeFamily eqns
+            (FamilyDecl { fdInfo = ClosedTypeFamily mb_eqns
                         , fdLName = lname@(L _ tc_name), fdTyVars = tvs })
 -- Closed type families are a little tricky, because they contain the definition
 -- of both the type family and the equations for a CoAxiom.
--- Note: eqns might be empty, in a hs-boot file!
   = do { traceTc "closed type family:" (ppr tc_name)
          -- the variables in the header have no scope:
        ; (tvs', kind) <- tcTyClTyVars tc_name tvs $ \ tvs' kind ->
@@ -685,6 +684,14 @@ tcFamDecl1 parent
 
        ; checkFamFlag tc_name -- make sure we have -XTypeFamilies
 
+         -- If Nothing, this is an abstract family in a hs-boot file;
+         -- but eqns might be empty in the Just case as well
+       ; case mb_eqns of
+           Nothing   -> do { tycon <- buildFamilyTyCon tc_name tvs'
+                                        AbstractClosedSynFamilyTyCon kind parent
+                           ; return [ATyCon tycon] }
+           Just eqns -> do {
+
          -- Process the equations, creating CoAxBranches
        ; tc_kind <- kcLookupKind tc_name
        ; let fam_tc_shape = (tc_name, length (hsQTvBndrs tvs), tc_kind)
@@ -705,20 +712,15 @@ tcFamDecl1 parent
        ; loc <- getSrcSpanM
        ; co_ax_name <- newFamInstAxiomName loc tc_name []
 
-         -- mkBranchedCoAxiom will fail on an empty list of branches, but
-         -- we'll never look at co_ax in this case
-       ; let co_ax = mkBranchedCoAxiom co_ax_name fam_tc branches
+         -- mkBranchedCoAxiom will fail on an empty list of branches
+       ; let mb_co_ax
+              | null eqns = Nothing
+              | otherwise = Just $ mkBranchedCoAxiom co_ax_name fam_tc branches
 
          -- now, finally, build the TyCon
-       ; let syn_rhs = if null eqns
-                       then AbstractClosedSynFamilyTyCon
-                       else ClosedSynFamilyTyCon co_ax
-       ; tycon <- buildFamilyTyCon tc_name tvs' syn_rhs kind parent
-
-       ; let result = if null eqns
-                      then [ATyCon tycon]
-                      else [ATyCon tycon, ACoAxiom co_ax]
-       ; return result }
+       ; tycon <- buildFamilyTyCon tc_name tvs'
+                      (ClosedSynFamilyTyCon mb_co_ax) kind parent
+       ; return $ ATyCon tycon : maybeToList (fmap ACoAxiom mb_co_ax) } }
 -- We check for instance validity later, when doing validity checking for
 -- the tycon
 
@@ -1446,11 +1448,12 @@ checkValidTyCon tc
 
   | Just fam_flav <- famTyConFlav_maybe tc
   = case fam_flav of
-    { ClosedSynFamilyTyCon ax      -> checkValidClosedCoAxiom ax
+    { ClosedSynFamilyTyCon (Just ax) -> checkValidClosedCoAxiom ax
+    ; ClosedSynFamilyTyCon Nothing   -> return ()
     ; AbstractClosedSynFamilyTyCon ->
       do { hsBoot <- tcIsHsBootOrSig
          ; checkTc hsBoot $
-           ptext (sLit "You may omit the equations in a closed type family") $$
+           ptext (sLit "You may define an abstract closed type family") $$
            ptext (sLit "only in a .hs-boot file") }
     ; OpenSynFamilyTyCon           -> return ()
     ; BuiltInSynFamTyCon _         -> return () }

compiler/types/FamInstEnv.hs

@@ -815,7 +815,7 @@ reduceTyFamApp_maybe envs role tc tys
         ty     = pSnd (coercionKind co)
     in Just (co, ty)
 
-  | Just ax <- isClosedSynFamilyTyCon_maybe tc
+  | Just ax <- isClosedSynFamilyTyConWithAxiom_maybe tc
   , Just (ind, inst_tys) <- chooseBranch ax tys
   = let co     = mkAxInstCo role ax ind inst_tys
         ty     = pSnd (coercionKind co)

compiler/types/TyCon.hs

@@ -46,7 +46,7 @@ module TyCon(
         isNewTyCon, isAbstractTyCon,
         isFamilyTyCon, isOpenFamilyTyCon,
         isTypeFamilyTyCon, isDataFamilyTyCon,
-        isOpenTypeFamilyTyCon, isClosedSynFamilyTyCon_maybe,
+        isOpenTypeFamilyTyCon, isClosedSynFamilyTyConWithAxiom_maybe,
         isBuiltInSynFamTyCon_maybe,
         isUnLiftedTyCon,
         isGadtSyntaxTyCon, isDistinctTyCon, isDistinctAlgRhs,
@@ -699,8 +699,8 @@ data FamTyConFlav
 
    -- | A closed type synonym family  e.g.
    -- @type family F x where { F Int = Bool }@
-   | ClosedSynFamilyTyCon
-       (CoAxiom Branched) -- The one axiom for this family
+   | ClosedSynFamilyTyCon (Maybe (CoAxiom Branched))
+     -- See Note [Closed type families]
 
    -- | A closed type synonym family declared in an hs-boot file with
    -- type family F a where ..
@@ -718,6 +718,11 @@ Note [Closed type families]
 * In a closed type family you can only put equations where the family
   is defined.
 
+A non-empty closed type family has a single axiom with multiple
+branches, stored in the 'ClosedSynFamilyTyCon' constructor.  A closed
+type family with no equations does not have an axiom, because there is
+nothing for the axiom to prove!
+
 
 Note [Promoted data constructors]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1361,11 +1366,12 @@ isOpenTypeFamilyTyCon :: TyCon -> Bool
 isOpenTypeFamilyTyCon (FamilyTyCon {famTcFlav = OpenSynFamilyTyCon }) = True
 isOpenTypeFamilyTyCon _                                               = False
 
--- leave out abstract closed families here
-isClosedSynFamilyTyCon_maybe :: TyCon -> Maybe (CoAxiom Branched)
-isClosedSynFamilyTyCon_maybe
-  (FamilyTyCon {famTcFlav = ClosedSynFamilyTyCon ax}) = Just ax
-isClosedSynFamilyTyCon_maybe _                        = Nothing
+-- | Is this a non-empty closed type family? Returns 'Nothing' for
+-- abstract or empty closed families.
+isClosedSynFamilyTyConWithAxiom_maybe :: TyCon -> Maybe (CoAxiom Branched)
+isClosedSynFamilyTyConWithAxiom_maybe
+  (FamilyTyCon {famTcFlav = ClosedSynFamilyTyCon mb}) = mb
+isClosedSynFamilyTyConWithAxiom_maybe _               = Nothing
 
 isBuiltInSynFamTyCon_maybe :: TyCon -> Maybe BuiltInSynFamily
 isBuiltInSynFamTyCon_maybe

docs/users_guide/glasgow_exts.xml

@@ -6032,7 +6032,18 @@ type family F a where
 
     <para>
       A closed type family's equations have the same restrictions as the
-      equations for an open type family instances.
+      equations for open type family instances.
+    </para>
+
+    <para>
+      A closed type family may be declared with no equations.  Such
+      closed type families are opaque type-level definitions that will
+      never reduce, are not necessarily injective (unlike empty data
+      types), and cannot be given any instances.  This is different
+      from omitting the equations of a closed type family in a
+      <filename>hs-boot</filename> file, which uses the syntax
+      <literal>where ..</literal>, as in that case there may or may
+      not be equations given in the <filename>hs</filename> file.
     </para>
   </sect3>
 
@@ -6053,6 +6064,7 @@ type family H a where                            -- OK!
   H Bool = Bool
   H a    = String
 type instance H Char = Char       -- WRONG: cannot have instances of closed family
+type family K a where                            -- OK!
 
 type family G a b :: * -> *
 type instance G Int            = (,)     -- WRONG: must be two type parameters

testsuite/tests/indexed-types/should_compile/T9840.hs

+{-# LANGUAGE TypeFamilies #-}
+
+module T9840 where
+
+import T9840a
+
+type family X :: * -> * where
+
+type family F (a :: * -> *) where
+
+foo :: G (F X) -> G (F X)
+foo x = x

testsuite/tests/indexed-types/should_compile/T9840.hs-boot

+{-# LANGUAGE TypeFamilies #-}
+
+module T9840 where
+
+-- X is an abstract type family (it might be empty or not, though it
+-- will turn out to be empty when we check the hs file)
+type family X :: * -> * where ..
+
+-- F is known to be empty in the hs-boot file
+type family F (a :: * -> *) where

testsuite/tests/indexed-types/should_compile/T9840a.hs

+{-# LANGUAGE TypeFamilies #-}
+
+module T9840a where
+
+import {-# SOURCE #-} T9840
+
+type family G a where
+
+bar :: X a -> X a
+bar = id

testsuite/tests/indexed-types/should_compile/all.T

@@ -249,6 +249,10 @@ test('Sock', normal, compile, [''])
 test('T9211', normal, compile, [''])
 test('T9747', normal, compile, [''])
 test('T9582', normal, compile, [''])
+test('T9840',
+     extra_clean(['T9840.hi-boot', 'T9840.o-boot', 'T9840a.hi', 'T9840a.o']),
+     multimod_compile,
+     ['T9840', '-v0'])
 test('T9090', normal, compile, [''])
 test('T10020', normal, compile, [''])
 test('T10079', normal, compile, [''])

testsuite/tests/indexed-types/should_fail/ClosedFam4.hs

@@ -2,4 +2,4 @@
 
 module ClosedFam4 where
 
-type family Foo a where ..
\ No newline at end of file
+type family Foo a where ..

testsuite/tests/indexed-types/should_fail/ClosedFam4.stderr

 
 ClosedFam4.hs:5:1:
-    You may omit the equations in a closed type family
+    You may define an abstract closed type family
     only in a .hs-boot file
     In the type family declaration for ‘Foo’

testsuite/tests/th/T10306.hs

+{-# LANGUAGE TemplateHaskell, TypeFamilies #-}
+
+module T10306 where
+
+import Language.Haskell.TH
+import GHC.TypeLits
+
+-- Attempting to reify a built-in type family like (+) previously
+-- caused a crash, because it has no equations
+$(do x <- reify ''(+)
+     case x of
+       FamilyI (ClosedTypeFamilyD _ _ _ []) _ -> return []
+       _                                      -> error $ show x
+ )

testsuite/tests/th/T8028.hs

-{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TemplateHaskell, TypeFamilies #-}
 
 module T8028 where
 
 import T8028a
 
-$(x)
\ No newline at end of file
+import Language.Haskell.TH
+
+$(x)
+
+-- Check that the empty closed type family F produced by $(x) can
+-- subsequently be reified
+$(do f <- reify ''F
+     case f of
+       FamilyI (ClosedTypeFamilyD _ _ _ []) _ -> return []
+       _                                      -> error $ show f
+ )

testsuite/tests/th/T8028.stderr

-
-T8028.hs:7:3:
-    Illegal empty closed type family
-    When splicing a TH declaration: type family F_0 where

testsuite/tests/th/TH_abstractFamily.hs

+module TH_abstractFamily where
+
+import Language.Haskell.TH
+
+-- Empty closed type families are okay...
+ds1 :: Q [Dec]
+ds1 = [d| type family F a where |]
+
+-- ...but abstract ones should result in a type error
+ds2 :: Q [Dec]
+ds2 = [d| type family G a where .. |]

testsuite/tests/th/TH_abstractFamily.stderr

+
+TH_abstractFamily.hs:11:7:
+    abstract closed type family not (yet) handled by Template Haskell
+      type family G a where
+        ..

testsuite/tests/th/all.T

@@ -285,7 +285,7 @@ test('ClosedFam2TH', normal, compile, ['-v0'])
 
 test('T8028',
      extra_clean(['T8028a.hi', 'T8028a.o']),
-     multimod_compile_fail,
+     multimod_compile,
      ['T8028', '-v0 ' + config.ghc_th_way_flags])
 
 test('TH_Roles1', normal, compile_fail, ['-v0'])
@@ -360,3 +360,6 @@ test('T8624', normal, run_command, ['$MAKE -s --no-print-directory T8624'])
 test('TH_Lift', normal, compile, ['-v0'])
 test('T10047', normal, ghci_script, ['T10047.script'])
 test('T10019', normal, ghci_script, ['T10019.script'])
+test('T10306', normal, compile, ['-v0'])
+
+test('TH_abstractFamily', normal, compile_fail, [''])

haddock @ 26a590c0

-Subproject commit 5bbae8b9bc17d2166c7e03d5f42f2b12fadf70b7
+Subproject commit 26a590c009005d77fbee9e2c79286bd93f7955f5