Commit 9082111d authored by eir@cis.upenn.edu's avatar eir@cis.upenn.edu

Added support for writing and checking closed type families is hs-boot files.

As documented in the users' guide, you can now write

type family Foo a where ..

in a hs-boot file to declare an abstract closed type family.
parent 334131bc
......@@ -480,6 +480,8 @@ data FamilyDecl name = FamilyDecl
data FamilyInfo name
= DataFamily
| OpenTypeFamily
-- this list might be empty, if we're in an hs-boot file and the user
-- said "type family Foo x where .."
| ClosedTypeFamily [LTyFamInstEqn name]
deriving( Data, Typeable )
......@@ -622,7 +624,9 @@ instance (OutputableBndr name) => Outputable (FamilyDecl name) where
Just kind -> dcolon <+> ppr kind
(pp_where, pp_eqns) = case info of
ClosedTypeFamily eqns -> ( ptext (sLit "where")
, vcat $ map ppr eqns )
, if null eqns
then ptext (sLit "..")
else vcat $ map ppr eqns )
_ -> (empty, empty)
pprFlavour :: FamilyInfo name -> SDoc
......
......@@ -222,18 +222,21 @@ instance Binary IfaceDecl where
data IfaceSynTyConRhs
= IfaceOpenSynFamilyTyCon
| IfaceClosedSynFamilyTyCon IfExtName -- name of associated axiom
| IfaceAbstractClosedSynFamilyTyCon
| IfaceSynonymTyCon IfaceType
instance Binary IfaceSynTyConRhs where
put_ bh IfaceOpenSynFamilyTyCon = putByte bh 0
put_ bh (IfaceClosedSynFamilyTyCon ax) = putByte bh 1 >> put_ bh ax
put_ bh (IfaceSynonymTyCon ty) = putByte bh 2 >> put_ bh ty
put_ bh IfaceOpenSynFamilyTyCon = putByte bh 0
put_ bh (IfaceClosedSynFamilyTyCon ax) = putByte bh 1 >> put_ bh ax
put_ bh IfaceAbstractClosedSynFamilyTyCon = putByte bh 2
put_ bh (IfaceSynonymTyCon ty) = putByte bh 3 >> put_ bh ty
get bh = do { h <- getByte bh
; case h of
0 -> do { return IfaceOpenSynFamilyTyCon }
0 -> return IfaceOpenSynFamilyTyCon
1 -> do { ax <- get bh
; return (IfaceClosedSynFamilyTyCon ax) }
2 -> return IfaceAbstractClosedSynFamilyTyCon
_ -> do { ty <- get bh
; return (IfaceSynonymTyCon ty) } }
......@@ -1035,8 +1038,9 @@ pprIfaceDecl (IfaceSyn {ifName = tycon, ifTyVars = tyvars, ifRoles = roles,
= hang (ptext (sLit "type family") <+> pprIfaceDeclHead [] tycon tyvars roles)
4 (dcolon <+> ppr kind)
-- this case handles both abstract and instantiated closed family tycons
pprIfaceDecl (IfaceSyn {ifName = tycon, ifTyVars = tyvars, ifRoles = roles,
ifSynRhs = IfaceClosedSynFamilyTyCon {}, ifSynKind = kind })
ifSynRhs = _closedSynFamilyTyCon, ifSynKind = kind })
= hang (ptext (sLit "closed type family") <+> pprIfaceDeclHead [] tycon tyvars roles)
4 (dcolon <+> ppr kind)
......@@ -1352,9 +1356,10 @@ freeNamesIfIdDetails _ = emptyNameSet
-- All other changes are handled via the version info on the tycon
freeNamesIfSynRhs :: IfaceSynTyConRhs -> NameSet
freeNamesIfSynRhs (IfaceSynonymTyCon ty) = freeNamesIfType ty
freeNamesIfSynRhs IfaceOpenSynFamilyTyCon = emptyNameSet
freeNamesIfSynRhs (IfaceClosedSynFamilyTyCon ax) = unitNameSet ax
freeNamesIfSynRhs (IfaceSynonymTyCon ty) = freeNamesIfType ty
freeNamesIfSynRhs IfaceOpenSynFamilyTyCon = emptyNameSet
freeNamesIfSynRhs (IfaceClosedSynFamilyTyCon ax) = unitNameSet ax
freeNamesIfSynRhs IfaceAbstractClosedSynFamilyTyCon = emptyNameSet
freeNamesIfContext :: IfaceContext -> NameSet
freeNamesIfContext = fnList freeNamesIfType
......
......@@ -1513,9 +1513,12 @@ tyConToIfaceDecl env tycon
where
(env1, tyvars) = tidyTyClTyVarBndrs env (tyConTyVars tycon)
to_ifsyn_rhs OpenSynFamilyTyCon = IfaceOpenSynFamilyTyCon
to_ifsyn_rhs (ClosedSynFamilyTyCon ax) = IfaceClosedSynFamilyTyCon (coAxiomName ax)
to_ifsyn_rhs (SynonymTyCon ty) = IfaceSynonymTyCon (tidyToIfaceType env1 ty)
to_ifsyn_rhs OpenSynFamilyTyCon = IfaceOpenSynFamilyTyCon
to_ifsyn_rhs (ClosedSynFamilyTyCon ax)
= IfaceClosedSynFamilyTyCon (coAxiomName ax)
to_ifsyn_rhs AbstractClosedSynFamilyTyCon = IfaceAbstractClosedSynFamilyTyCon
to_ifsyn_rhs (SynonymTyCon ty)
= IfaceSynonymTyCon (tidyToIfaceType env1 ty)
ifaceConDecls (NewTyCon { data_con = con }) = IfNewTyCon (ifaceConDecl con)
ifaceConDecls (DataTyCon { data_cons = cons }) = IfDataTyCon (map ifaceConDecl cons)
......
......@@ -496,6 +496,7 @@ tc_iface_decl parent _ (IfaceSyn {ifName = occ_name, ifTyVars = tv_bndrs,
tc_syn_rhs (IfaceClosedSynFamilyTyCon ax_name)
= do { ax <- tcIfaceCoAxiom ax_name
; return (ClosedSynFamilyTyCon ax) }
tc_syn_rhs IfaceAbstractClosedSynFamilyTyCon = return AbstractClosedSynFamilyTyCon
tc_syn_rhs (IfaceSynonymTyCon ty) = do { rhs_ty <- tcIfaceType ty
; return (SynonymTyCon rhs_ty) }
......
......@@ -179,9 +179,9 @@ pprTyCon pefas ss tyCon
OpenSynFamilyTyCon -> pprTyConHdr pefas tyCon <+> dcolon <+>
pprTypeForUser pefas (GHC.synTyConResKind tyCon)
ClosedSynFamilyTyCon (CoAxiom { co_ax_branches = branches }) ->
hang (pprTyConHdr pefas tyCon <+> dcolon <+>
pprTypeForUser pefas (GHC.synTyConResKind tyCon) <+> ptext (sLit "where"))
hang closed_family_header
2 (vcat (brListMap (pprCoAxBranch tyCon) branches))
AbstractClosedSynFamilyTyCon -> closed_family_header <+> ptext (sLit "..")
SynonymTyCon rhs_ty -> hang (pprTyConHdr pefas tyCon <+> equals)
2 (ppr rhs_ty) -- Don't suppress foralls on RHS type!
-- e.g. type T = forall a. a->a
......@@ -190,6 +190,11 @@ pprTyCon pefas ss tyCon
| otherwise
= pprAlgTyCon pefas ss tyCon
where
closed_family_header
= pprTyConHdr pefas tyCon <+> dcolon <+>
pprTypeForUser pefas (GHC.synTyConResKind tyCon) <+> ptext (sLit "where")
pprAlgTyCon :: PrintExplicitForalls -> ShowSub -> TyCon -> SDoc
pprAlgTyCon pefas ss tyCon
| gadt = pprTyConHdr pefas tyCon <+> ptext (sLit "where") $$
......
......@@ -712,6 +712,8 @@ where_type_family :: { Located (FamilyInfo RdrName) }
ty_fam_inst_eqn_list :: { Located [LTyFamInstEqn RdrName] }
: '{' ty_fam_inst_eqns '}' { LL (unLoc $2) }
| vocurly ty_fam_inst_eqns close { $2 }
| '{' '..' '}' { LL [] }
| vocurly '..' close { let L loc _ = $2 in L loc [] }
ty_fam_inst_eqns :: { Located [LTyFamInstEqn RdrName] }
: ty_fam_inst_eqns ';' ty_fam_inst_eqn { LL ($3 : unLoc $1) }
......
......@@ -1070,6 +1070,7 @@ data KindCheckingStrategy -- See Note [Kind-checking strategies]
= ParametricKinds
| NonParametricKinds
| FullKindSignature
deriving (Eq)
-- determine the appropriate strategy for a decl
kcStrategy :: TyClDecl Name -> KindCheckingStrategy
......@@ -1082,10 +1083,10 @@ kcStrategy (DataDecl { tcdDataDefn = HsDataDefn { dd_kindSig = m_ksig }})
| otherwise = ParametricKinds
kcStrategy (ClassDecl {}) = ParametricKinds
-- if the ClosedTypeFamily has no equations, do the defaulting to *, etc.
kcStrategyFamDecl :: FamilyDecl Name -> KindCheckingStrategy
kcStrategyFamDecl (FamilyDecl { fdInfo = info })
| isClosedTypeFamilyInfo info = NonParametricKinds
| otherwise = FullKindSignature
kcStrategyFamDecl (FamilyDecl { fdInfo = ClosedTypeFamily (_:_) }) = NonParametricKinds
kcStrategyFamDecl _ = FullKindSignature
mkKindSigVar :: Name -> TcM KindVar
-- Use the specified name; don't clone it
......
......@@ -34,7 +34,7 @@ import TcHsSyn
import TcExpr
import TcRnMonad
import TcEvidence
import Coercion( pprCoAxiom )
import Coercion( pprCoAxiom, pprCoAxBranch )
import FamInst
import InstEnv
import FamInstEnv
......@@ -49,7 +49,6 @@ import TcInstDcls
import TcIface
import TcMType
import MkIface
import IfaceSyn
import TcSimplify
import TcTyClsDecls
import LoadIface
......@@ -75,7 +74,7 @@ import Outputable
import DataCon
import Type
import Class
import CoAxiom ( CoAxBranch(..) )
import CoAxiom
import Inst ( tcGetInstEnvs )
import Data.List ( sortBy )
import Data.IORef ( readIORef )
......@@ -660,10 +659,7 @@ checkHiBootIface
Just boot_thing <- mb_boot_thing
= when (not (checkBootDecl boot_thing real_thing))
$ addErrAt (nameSrcSpan (getName boot_thing))
(let boot_decl = tyThingToIfaceDecl
(fromJust mb_boot_thing)
real_decl = tyThingToIfaceDecl real_thing
in bootMisMatch real_thing boot_decl real_decl)
(bootMisMatch real_thing boot_thing)
| otherwise
= addErrTc (missingBootThing name "defined in")
......@@ -772,8 +768,10 @@ checkBootTyCon tc1 tc2
, Just env <- eqTyVarBndrs emptyRnEnv2 (tyConTyVars tc1) (tyConTyVars tc2)
= ASSERT(tc1 == tc2)
let eqSynRhs OpenSynFamilyTyCon OpenSynFamilyTyCon = True
eqSynRhs AbstractClosedSynFamilyTyCon (ClosedSynFamilyTyCon {}) = True
eqSynRhs (ClosedSynFamilyTyCon {}) AbstractClosedSynFamilyTyCon = True
eqSynRhs (ClosedSynFamilyTyCon ax1) (ClosedSynFamilyTyCon ax2)
= ax1 == ax2
= eqClosedFamilyAx ax1 ax2
eqSynRhs (SynonymTyCon t1) (SynonymTyCon t2)
= eqTypeX env t1 t2
eqSynRhs _ _ = False
......@@ -814,6 +812,19 @@ checkBootTyCon tc1 tc2
&& dataConFieldLabels c1 == dataConFieldLabels c2
&& eqType (dataConUserType c1) (dataConUserType c2)
eqClosedFamilyAx (CoAxiom { co_ax_branches = branches1 })
(CoAxiom { co_ax_branches = branches2 })
= brListLength branches1 == brListLength branches2
&& (and $ brListZipWith eqClosedFamilyBranch branches1 branches2)
eqClosedFamilyBranch (CoAxBranch { cab_tvs = tvs1, cab_lhs = lhs1, cab_rhs = rhs1 })
(CoAxBranch { cab_tvs = tvs2, cab_lhs = lhs2, cab_rhs = rhs2 })
| Just env <- eqTyVarBndrs emptyRnEnv2 tvs1 tvs2
= eqListBy (eqTypeX env) lhs1 lhs2 &&
eqTypeX env rhs1 rhs2
| otherwise = False
emptyRnEnv2 :: RnEnv2
emptyRnEnv2 = mkRnEnv2 emptyInScopeSet
......@@ -823,11 +834,25 @@ missingBootThing name what
= ppr name <+> ptext (sLit "is exported by the hs-boot file, but not")
<+> text what <+> ptext (sLit "the module")
bootMisMatch :: TyThing -> IfaceDecl -> IfaceDecl -> SDoc
bootMisMatch thing boot_decl real_decl
= vcat [ppr thing <+> ptext (sLit "has conflicting definitions in the module and its hs-boot file"),
ptext (sLit "Main module:") <+> ppr real_decl,
ptext (sLit "Boot file: ") <+> ppr boot_decl]
bootMisMatch :: TyThing -> TyThing -> SDoc
bootMisMatch real_thing boot_thing
= vcat [ppr real_thing <+>
ptext (sLit "has conflicting definitions in the module"),
ptext (sLit "and its hs-boot file"),
ptext (sLit "Main module:") <+> ppr_mismatch real_thing,
ptext (sLit "Boot file: ") <+> ppr_mismatch boot_thing]
where
-- closed type families need special treatment, because they might differ
-- in their equations, which are not stored in the corresponding IfaceDecl
ppr_mismatch thing
| ATyCon tc <- thing
, Just (ClosedSynFamilyTyCon ax) <- synTyConRhs_maybe tc
= hang (ppr iface_decl <+> ptext (sLit "where"))
2 (vcat $ brListMap (pprCoAxBranch tc) (coAxiomBranches ax))
| otherwise
= ppr iface_decl
where iface_decl = tyThingToIfaceDecl thing
instMisMatch :: ClsInst -> SDoc
instMisMatch inst
......
......@@ -1394,6 +1394,8 @@ reifyFamFlavour tc
| isOpenSynFamilyTyCon 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 }
......
......@@ -422,7 +422,6 @@ getFamDeclInitialKinds decls
getFamDeclInitialKind :: FamilyDecl Name
-> TcM [(Name, TcTyThing)]
getFamDeclInitialKind decl@(FamilyDecl { fdLName = L _ name
, fdInfo = info
, fdTyVars = ktvs
, fdKindSig = ksig })
= do { (fam_kind, _, _) <-
......@@ -435,7 +434,7 @@ getFamDeclInitialKind decl@(FamilyDecl { fdLName = L _ name
; return (res_k, ()) }
; return [ (name, AThing fam_kind) ] }
where
defaultResToStar = not $ isClosedTypeFamilyInfo info
defaultResToStar = (kcStrategyFamDecl decl == FullKindSignature)
----------------
kcSynDecls :: [SCC (LTyClDecl Name)]
......@@ -697,6 +696,7 @@ tcFamDecl1 parent
, 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 ->
......@@ -727,14 +727,22 @@ tcFamDecl1 parent
-- See [Zonking inside the knot] in TcHsType
; 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
-- now, finally, build the TyCon
; let syn_rhs = ClosedSynFamilyTyCon co_ax
; let syn_rhs = if null eqns
then AbstractClosedSynFamilyTyCon
else ClosedSynFamilyTyCon co_ax
roles = map (const Nominal) tvs'
; tycon <- buildSynTyCon tc_name tvs' roles syn_rhs kind parent
; return [ATyCon tycon, ACoAxiom co_ax] }
; let result = if null eqns
then [ATyCon tycon]
else [ATyCon tycon, ACoAxiom co_ax]
; return result }
-- We check for instance validity later, when doing validity checking for
-- the tycon
......@@ -1404,9 +1412,14 @@ checkValidTyCon tc mroles
| Just syn_rhs <- synTyConRhs_maybe tc
= case syn_rhs of
ClosedSynFamilyTyCon ax -> checkValidClosedCoAxiom ax
OpenSynFamilyTyCon -> return ()
SynonymTyCon ty ->
ClosedSynFamilyTyCon ax -> checkValidClosedCoAxiom ax
AbstractClosedSynFamilyTyCon ->
do { hsBoot <- tcIsHsBoot
; checkTc hsBoot $
ptext (sLit "You may omit the equations in a closed type family") $$
ptext (sLit "only in a .hs-boot file") }
OpenSynFamilyTyCon -> return ()
SynonymTyCon ty ->
do { check_roles
; checkValidType syn_ctxt ty }
......
......@@ -624,6 +624,10 @@ data SynTyConRhs
-- | A closed type synonym family e.g. @type family F x where { F Int = Bool }@
| ClosedSynFamilyTyCon
(CoAxiom Branched) -- The one axiom for this family
-- | A closed type synonym family declared in an hs-boot file with
-- type family F a where ..
| AbstractClosedSynFamilyTyCon
\end{code}
Note [Closed type families]
......@@ -1200,9 +1204,10 @@ isEnumerationTyCon _ = False
-- | Is this a 'TyCon', synonym or otherwise, that defines a family?
isFamilyTyCon :: TyCon -> Bool
isFamilyTyCon (SynTyCon {synTcRhs = OpenSynFamilyTyCon }) = True
isFamilyTyCon (SynTyCon {synTcRhs = ClosedSynFamilyTyCon {} }) = True
isFamilyTyCon (AlgTyCon {algTcRhs = DataFamilyTyCon {}}) = True
isFamilyTyCon (SynTyCon {synTcRhs = OpenSynFamilyTyCon }) = True
isFamilyTyCon (SynTyCon {synTcRhs = ClosedSynFamilyTyCon {} }) = True
isFamilyTyCon (SynTyCon {synTcRhs = AbstractClosedSynFamilyTyCon {} }) = True
isFamilyTyCon (AlgTyCon {algTcRhs = DataFamilyTyCon {}}) = True
isFamilyTyCon _ = False
-- | Is this a 'TyCon', synonym or otherwise, that defines an family with
......@@ -1214,14 +1219,16 @@ isOpenFamilyTyCon _ = False
-- | Is this a synonym 'TyCon' that can have may have further instances appear?
isSynFamilyTyCon :: TyCon -> Bool
isSynFamilyTyCon (SynTyCon {synTcRhs = OpenSynFamilyTyCon {}}) = True
isSynFamilyTyCon (SynTyCon {synTcRhs = ClosedSynFamilyTyCon {}}) = True
isSynFamilyTyCon (SynTyCon {synTcRhs = OpenSynFamilyTyCon {}}) = True
isSynFamilyTyCon (SynTyCon {synTcRhs = ClosedSynFamilyTyCon {}}) = True
isSynFamilyTyCon (SynTyCon {synTcRhs = AbstractClosedSynFamilyTyCon {}}) = True
isSynFamilyTyCon _ = False
isOpenSynFamilyTyCon :: TyCon -> Bool
isOpenSynFamilyTyCon (SynTyCon {synTcRhs = OpenSynFamilyTyCon }) = True
isOpenSynFamilyTyCon _ = False
-- leave out abstract closed families here
isClosedSynFamilyTyCon_maybe :: TyCon -> Maybe (CoAxiom Branched)
isClosedSynFamilyTyCon_maybe
(SynTyCon {synTcRhs = ClosedSynFamilyTyCon ax}) = Just ax
......
......@@ -836,7 +836,13 @@ values. For example:
</programlisting>
</para></listitem>
<listitem><para> Fixity declarations are exactly as in Haskell.</para></listitem>
<listitem><para> Type synonym declarations are exactly as in Haskell.</para></listitem>
<listitem><para> Vanilla type synonym declarations are exactly as in Haskell.</para></listitem>
<listitem><para> Open type and data family declarations are exactly as in Haskell.</para></listitem>
<listitem><para> A closed type family may optionally omit its equations, as in the following example:
<programlisting>
type family ClosedFam a where ..
</programlisting>
The <literal>..</literal> is meant literally -- you should write two dots in your file. Note that the <literal>where</literal> clause is still necessary to distinguish closed families from open ones. If you give any equations of a closed family, you must give all of them, in the same order as they appear in the accompanying Haskell file.</para></listitem>
<listitem><para> A data type declaration can either be given in full, exactly as in Haskell, or it
can be given abstractly, by omitting the '=' sign and everything that follows. For example:
<programlisting>
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment