Commit 37445780 authored by Jan Stolarek's avatar Jan Stolarek

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
parent bd16e0bc
......@@ -12,7 +12,7 @@ have a standard form, namely:
- primitive operations
-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE CPP, DataKinds #-}
module MkId (
mkDictFunId, mkDictFunTy, mkDictSelId, mkDictSelRhs,
......@@ -911,7 +911,8 @@ wrapTypeFamInstBody :: CoAxiom br -> Int -> [Type] -> CoreExpr -> CoreExpr
wrapTypeFamInstBody axiom ind args body
= mkCast body (mkSymCo (mkAxInstCo Representational axiom ind args))
wrapTypeUnbranchedFamInstBody :: CoAxiom Unbranched -> [Type] -> CoreExpr -> CoreExpr
wrapTypeUnbranchedFamInstBody :: CoAxiom Unbranched -> [Type] -> CoreExpr
-> CoreExpr
wrapTypeUnbranchedFamInstBody axiom
= wrapTypeFamInstBody axiom 0
......@@ -926,7 +927,8 @@ unwrapTypeFamInstScrut :: CoAxiom br -> Int -> [Type] -> CoreExpr -> CoreExpr
unwrapTypeFamInstScrut axiom ind args scrut
= mkCast scrut (mkAxInstCo Representational axiom ind args)
unwrapTypeUnbranchedFamInstScrut :: CoAxiom Unbranched -> [Type] -> CoreExpr -> CoreExpr
unwrapTypeUnbranchedFamInstScrut :: CoAxiom Unbranched -> [Type] -> CoreExpr
-> CoreExpr
unwrapTypeUnbranchedFamInstScrut axiom
= unwrapTypeFamInstScrut axiom 0
......
......@@ -27,6 +27,7 @@ module VarSet (
import Var ( Var, TyVar, CoVar, Id )
import Unique
import UniqSet
import UniqFM( disjointUFM )
{-
************************************************************************
......@@ -98,7 +99,7 @@ lookupVarSet = lookupUniqSet
mapVarSet = mapUniqSet
sizeVarSet = sizeUniqSet
filterVarSet = filterUniqSet
extendVarSet_C = addOneToUniqSet_C
extendVarSet_C = addOneToUniqSet_C
delVarSetByKey = delOneFromUniqSet_Directly
elemVarSetByKey = elemUniqSet_Directly
partitionVarSet = partitionUniqSet
......@@ -107,7 +108,7 @@ mapUnionVarSet get_set xs = foldr (unionVarSet . get_set) emptyVarSet xs
-- See comments with type signatures
intersectsVarSet s1 s2 = not (s1 `disjointVarSet` s2)
disjointVarSet s1 s2 = isEmptyVarSet (s1 `intersectVarSet` s2)
disjointVarSet s1 s2 = disjointUFM s1 s2
subVarSet s1 s2 = isEmptyVarSet (s1 `minusVarSet` s2)
fixVarSet :: (VarSet -> VarSet) -- Map the current set to a new set
......
......@@ -43,6 +43,9 @@ module MkCore (
mkNilExpr, mkConsExpr, mkListExpr,
mkFoldrExpr, mkBuildExpr,
-- * Constructing Maybe expressions
mkNothingExpr, mkJustExpr,
-- * Error Ids
mkRuntimeErrorApp, mkImpossibleExpr, errorIds,
rEC_CON_ERROR_ID, iRREFUT_PAT_ERROR_ID, rUNTIME_ERROR_ID,
......@@ -602,6 +605,24 @@ mkBuildExpr elt_ty mk_build_inside = do
uniqs <- getUniquesM
return (zipWith setTyVarUnique tyvar_tmpls uniqs)
{-
************************************************************************
* *
Manipulating Maybe data type
* *
************************************************************************
-}
-- | Makes a Nothing for the specified type
mkNothingExpr :: Type -> CoreExpr
mkNothingExpr ty = mkConApp nothingDataCon [Type ty]
-- | Makes a Just from a value of the specified type
mkJustExpr :: Type -> CoreExpr -> CoreExpr
mkJustExpr ty val = mkConApp justDataCon [Type ty, val]
{-
************************************************************************
* *
......
......@@ -310,34 +310,69 @@ repSynDecl tc bndrs ty
; repTySyn tc bndrs ty1 }
repFamilyDecl :: LFamilyDecl Name -> DsM (SrcSpan, Core TH.DecQ)
repFamilyDecl decl@(L loc (FamilyDecl { fdInfo = info,
fdLName = tc,
fdTyVars = tvs,
fdKindSig = opt_kind }))
repFamilyDecl decl@(L loc (FamilyDecl { fdInfo = info,
fdLName = tc,
fdTyVars = tvs,
fdResultSig = L _ resultSig,
fdInjectivityAnn = injectivity }))
= do { tc1 <- lookupLOcc tc -- See note [Binders and occurrences]
; let mkHsQTvs tvs = HsQTvs { hsq_kvs = [], hsq_tvs = tvs }
resTyVar = case resultSig of
TyVarSig bndr -> mkHsQTvs [bndr]
_ -> mkHsQTvs []
; dec <- addTyClTyVarBinds tvs $ \bndrs ->
case (opt_kind, info) of
(_ , 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 (Just eqns)) ->
do { eqns1 <- mapM repTyFamEqn eqns
; eqns2 <- coreList tySynEqnQTyConName eqns1
; ki1 <- repLKind ki
; repClosedFamilyKind tc1 bndrs ki1 eqns2 }
(Nothing, _) ->
do { info' <- repFamilyInfo info
; repFamilyNoKind info' tc1 bndrs }
(Just ki, _) ->
do { info' <- repFamilyInfo info
; ki1 <- repLKind ki
; repFamilyKind info' tc1 bndrs ki1 }
addTyClTyVarBinds resTyVar $ \_ ->
case info of
ClosedTypeFamily Nothing ->
notHandled "abstract closed type family" (ppr decl)
ClosedTypeFamily (Just eqns) ->
do { eqns1 <- mapM repTyFamEqn eqns
; eqns2 <- coreList tySynEqnQTyConName eqns1
; result <- repFamilyResultSig resultSig
; inj <- repInjectivityAnn injectivity
; repClosedFamilyD tc1 bndrs result inj eqns2 }
OpenTypeFamily ->
do { result <- repFamilyResultSig resultSig
; inj <- repInjectivityAnn injectivity
; repOpenFamilyD tc1 bndrs result inj }
DataFamily ->
do { kind <- repFamilyResultSigToMaybeKind resultSig
; repDataFamilyD tc1 bndrs kind }
; return (loc, dec)
}
-- | Represent result signature of a type family
repFamilyResultSig :: FamilyResultSig Name -> DsM (Core TH.FamilyResultSig)
repFamilyResultSig NoSig = repNoSig
repFamilyResultSig (KindSig ki) = do { ki' <- repLKind ki
; repKindSig ki' }
repFamilyResultSig (TyVarSig bndr) = do { bndr' <- repTyVarBndr bndr
; repTyVarSig bndr' }
-- | Represent result signature using a Maybe Kind. Used with data families,
-- where the result signature can be either missing or a kind but never a named
-- result variable.
repFamilyResultSigToMaybeKind :: FamilyResultSig Name
-> DsM (Core (Maybe TH.Kind))
repFamilyResultSigToMaybeKind NoSig =
do { coreNothing kindTyConName }
repFamilyResultSigToMaybeKind (KindSig ki) =
do { ki' <- repLKind ki
; coreJust kindTyConName ki' }
repFamilyResultSigToMaybeKind _ = panic "repFamilyResultSigToMaybeKind"
-- | Represent injectivity annotation of a type family
repInjectivityAnn :: Maybe (LInjectivityAnn Name)
-> DsM (Core (Maybe TH.InjectivityAnn))
repInjectivityAnn Nothing =
do { coreNothing injAnnTyConName }
repInjectivityAnn (Just (L _ (InjectivityAnn lhs rhs))) =
do { lhs' <- lookupBinder (unLoc lhs)
; rhs1 <- mapM (lookupBinder . unLoc) rhs
; rhs2 <- coreList nameTyConName rhs1
; injAnn <- rep2 injectivityAnnName [unC lhs', unC rhs2]
; coreJust injAnnTyConName injAnn }
repFamilyDecls :: [LFamilyDecl Name] -> DsM [Core TH.DecQ]
repFamilyDecls fds = liftM de_loc (mapM repFamilyDecl fds)
......@@ -381,13 +416,6 @@ repLFunDep (L _ (xs, ys))
ys' <- repList nameTyConName (lookupBinder . unLoc) ys
repFunDep xs' ys'
-- represent family declaration flavours
--
repFamilyInfo :: FamilyInfo Name -> DsM (Core TH.FamFlavour)
repFamilyInfo OpenTypeFamily = rep2 typeFamName []
repFamilyInfo DataFamily = rep2 dataFamName []
repFamilyInfo ClosedTypeFamily {} = panic "repFamilyInfo"
-- Represent instance declarations
--
repInstD :: LInstDecl Name -> DsM (SrcSpan, Core TH.DecQ)
......@@ -831,6 +859,14 @@ repTyVarBndrWithKind (L _ (UserTyVar _)) nm
repTyVarBndrWithKind (L _ (KindedTyVar _ ki)) nm
= repLKind ki >>= repKindedTV nm
-- | Represent a type variable binder
repTyVarBndr :: LHsTyVarBndr Name -> DsM (Core TH.TyVarBndr)
repTyVarBndr (L _ (UserTyVar nm)) = do { nm' <- lookupBinder nm
; repPlainTV nm' }
repTyVarBndr (L _ (KindedTyVar (L _ nm) ki)) = do { nm' <- lookupBinder nm
; ki' <- repLKind ki
; repKindedTV nm' ki' }
-- represent a type context
--
repLContext :: LHsContext Name -> DsM (Core TH.CxtQ)
......@@ -1827,35 +1863,31 @@ repPragRule (MkC nm) (MkC bndrs) (MkC lhs) (MkC rhs) (MkC phases)
repPragAnn :: Core TH.AnnTarget -> Core TH.ExpQ -> DsM (Core TH.DecQ)
repPragAnn (MkC targ) (MkC e) = rep2 pragAnnDName [targ, e]
repFamilyNoKind :: Core TH.FamFlavour -> Core TH.Name -> Core [TH.TyVarBndr]
-> DsM (Core TH.DecQ)
repFamilyNoKind (MkC flav) (MkC nm) (MkC tvs)
= rep2 familyNoKindDName [flav, nm, tvs]
repFamilyKind :: Core TH.FamFlavour -> Core TH.Name -> Core [TH.TyVarBndr]
-> Core TH.Kind
-> DsM (Core TH.DecQ)
repFamilyKind (MkC flav) (MkC nm) (MkC tvs) (MkC ki)
= rep2 familyKindDName [flav, nm, tvs, ki]
repTySynInst :: Core TH.Name -> Core TH.TySynEqnQ -> DsM (Core TH.DecQ)
repTySynInst (MkC nm) (MkC eqn)
= rep2 tySynInstDName [nm, eqn]
repClosedFamilyNoKind :: Core TH.Name
-> Core [TH.TyVarBndr]
-> Core [TH.TySynEqnQ]
-> DsM (Core TH.DecQ)
repClosedFamilyNoKind (MkC nm) (MkC tvs) (MkC eqns)
= rep2 closedTypeFamilyNoKindDName [nm, tvs, eqns]
repClosedFamilyKind :: Core TH.Name
-> Core [TH.TyVarBndr]
-> Core TH.Kind
-> Core [TH.TySynEqnQ]
-> DsM (Core TH.DecQ)
repClosedFamilyKind (MkC nm) (MkC tvs) (MkC ki) (MkC eqns)
= rep2 closedTypeFamilyKindDName [nm, tvs, ki, eqns]
repDataFamilyD :: Core TH.Name -> Core [TH.TyVarBndr]
-> Core (Maybe TH.Kind) -> DsM (Core TH.DecQ)
repDataFamilyD (MkC nm) (MkC tvs) (MkC kind)
= rep2 dataFamilyDName [nm, tvs, kind]
repOpenFamilyD :: Core TH.Name
-> Core [TH.TyVarBndr]
-> Core TH.FamilyResultSig
-> Core (Maybe TH.InjectivityAnn)
-> DsM (Core TH.DecQ)
repOpenFamilyD (MkC nm) (MkC tvs) (MkC result) (MkC inj)
= rep2 openTypeFamilyDName [nm, tvs, result, inj]
repClosedFamilyD :: Core TH.Name
-> Core [TH.TyVarBndr]
-> Core TH.FamilyResultSig
-> Core (Maybe TH.InjectivityAnn)
-> Core [TH.TySynEqnQ]
-> DsM (Core TH.DecQ)
repClosedFamilyD (MkC nm) (MkC tvs) (MkC res) (MkC inj) (MkC eqns)
= rep2 closedTypeFamilyDName [nm, tvs, res, inj, eqns]
repTySynEqn :: Core [TH.TypeQ] -> Core TH.TypeQ -> DsM (Core TH.TySynEqnQ)
repTySynEqn (MkC lhs) (MkC rhs)
......@@ -2006,6 +2038,18 @@ repKStar = rep2 starKName []
repKConstraint :: DsM (Core TH.Kind)
repKConstraint = rep2 constraintKName []
----------------------------------------------------------
-- Type family result signature
repNoSig :: DsM (Core TH.FamilyResultSig)
repNoSig = rep2 noSigName []
repKindSig :: Core TH.Kind -> DsM (Core TH.FamilyResultSig)
repKindSig (MkC ki) = rep2 kindSigName [ki]
repTyVarSig :: Core TH.TyVarBndr -> DsM (Core TH.FamilyResultSig)
repTyVarSig (MkC bndr) = rep2 tyVarSigName [bndr]
----------------------------------------------------------
-- Literals
......@@ -2082,7 +2126,7 @@ repSequenceQ :: Type -> Core [TH.Q a] -> DsM (Core (TH.Q [a]))
repSequenceQ ty_a (MkC list)
= rep2 sequenceQName [Type ty_a, list]
------------ Lists and Tuples -------------------
------------ Lists -------------------
-- turn a list of patterns into a single pattern matching a list
repList :: Name -> (a -> DsM (Core b))
......@@ -2109,6 +2153,30 @@ nonEmptyCoreList xs@(MkC x:_) = MkC (mkListExpr (exprType x) (map unC xs))
coreStringLit :: String -> DsM (Core String)
coreStringLit s = do { z <- mkStringExpr s; return(MkC z) }
------------------- Maybe ------------------
-- | Construct Core expression for Nothing of a given type name
coreNothing :: Name -- ^ Name of the TyCon of the element type
-> DsM (Core (Maybe a))
coreNothing tc_name =
do { elt_ty <- lookupType tc_name; return (coreNothing' elt_ty) }
-- | Construct Core expression for Nothing of a given type
coreNothing' :: Type -- ^ The element type
-> Core (Maybe a)
coreNothing' elt_ty = MkC (mkNothingExpr elt_ty)
-- | Store given Core expression in a Just of a given type name
coreJust :: Name -- ^ Name of the TyCon of the element type
-> Core a -> DsM (Core (Maybe a))
coreJust tc_name es
= do { elt_ty <- lookupType tc_name; return (coreJust' elt_ty es) }
-- | Store given Core expression in a Just of a given type
coreJust' :: Type -- ^ The element type
-> Core a -> Core (Maybe a)
coreJust' elt_ty es = MkC (mkJustExpr elt_ty (unC es))
------------ Literals & Variables -------------------
coreIntLit :: Int -> DsM (Core Int)
......
......@@ -253,14 +253,11 @@ cvtDec (ForeignD ford)
= do { ford' <- cvtForD ford
; returnJustL $ ForD ford' }
cvtDec (FamilyD flav tc tvs kind)
cvtDec (DataFamilyD tc tvs kind)
= do { (_, tc', tvs') <- cvt_tycl_hdr [] tc tvs
; kind' <- cvtMaybeKind kind
; result <- cvtMaybeKindToFamilyResultSig kind
; returnJustL $ TyClD $ FamDecl $
FamilyDecl (cvtFamFlavour flav) tc' tvs' kind' }
where
cvtFamFlavour TypeFam = OpenTypeFamily
cvtFamFlavour DataFam = DataFamily
FamilyDecl DataFamily tc' tvs' result Nothing }
cvtDec (DataInstD ctxt tc tys constrs derivs)
= do { (ctxt', tc', typats') <- cvt_tyinst_hdr ctxt tc tys
......@@ -296,12 +293,21 @@ cvtDec (TySynInstD tc eqn)
{ tfid_inst = TyFamInstDecl { tfid_eqn = eqn'
, tfid_fvs = placeHolderNames } } }
cvtDec (ClosedTypeFamilyD tc tyvars mkind eqns)
cvtDec (OpenTypeFamilyD tc tvs result injectivity)
= do { (_, tc', tvs') <- cvt_tycl_hdr [] tc tvs
; result' <- cvtFamilyResultSig result
; injectivity' <- traverse cvtInjectivityAnnotation injectivity
; returnJustL $ TyClD $ FamDecl $
FamilyDecl OpenTypeFamily tc' tvs' result' injectivity' }
cvtDec (ClosedTypeFamilyD tc tyvars result injectivity eqns)
= do { (_, tc', tvs') <- cvt_tycl_hdr [] tc tyvars
; mkind' <- cvtMaybeKind mkind
; result' <- cvtFamilyResultSig result
; eqns' <- mapM (cvtTySynEqn tc') eqns
; injectivity' <- traverse cvtInjectivityAnnotation injectivity
; returnJustL $ TyClD $ FamDecl $
FamilyDecl (ClosedTypeFamily (Just eqns')) tc' tvs' mkind' }
FamilyDecl (ClosedTypeFamily (Just eqns')) tc' tvs' result'
injectivity' }
cvtDec (TH.RoleAnnotD tc roles)
= do { tc' <- tconNameL tc
......@@ -1132,10 +1138,31 @@ cvtOpAppT x op y
cvtKind :: TH.Kind -> CvtM (LHsKind RdrName)
cvtKind = cvtTypeKind "kind"
cvtMaybeKind :: Maybe TH.Kind -> CvtM (Maybe (LHsKind RdrName))
cvtMaybeKind Nothing = return Nothing
cvtMaybeKind (Just ki) = do { ki' <- cvtKind ki
; return (Just ki') }
-- | Convert Maybe Kind to a type family result signature. Used with data
-- families where naming of the result is not possible (thus only kind or no
-- signature is possible).
cvtMaybeKindToFamilyResultSig :: Maybe TH.Kind
-> CvtM (LFamilyResultSig RdrName)
cvtMaybeKindToFamilyResultSig Nothing = returnL Hs.NoSig
cvtMaybeKindToFamilyResultSig (Just ki) = do { ki' <- cvtKind ki
; returnL (Hs.KindSig ki') }
-- | Convert type family result signature. Used with both open and closed type
-- families.
cvtFamilyResultSig :: TH.FamilyResultSig -> CvtM (Hs.LFamilyResultSig RdrName)
cvtFamilyResultSig TH.NoSig = returnL Hs.NoSig
cvtFamilyResultSig (TH.KindSig ki) = do { ki' <- cvtKind ki
; returnL (Hs.KindSig ki') }
cvtFamilyResultSig (TH.TyVarSig bndr) = do { tv <- cvt_tv bndr
; returnL (Hs.TyVarSig tv) }
-- | Convert injectivity annotation of a type family.
cvtInjectivityAnnotation :: TH.InjectivityAnn
-> CvtM (Hs.LInjectivityAnn RdrName)
cvtInjectivityAnnotation (TH.InjectivityAnn annLHS annRHS)
= do { annLHS' <- tNameL annLHS
; annRHS' <- mapM tNameL annRHS
; returnL (Hs.InjectivityAnn annLHS' annRHS') }
-----------------------------------------------------------
cvtFixity :: TH.Fixity -> Hs.Fixity
......@@ -1165,7 +1192,7 @@ cvtFractionalLit r = FL { fl_text = show (fromRational r :: Double), fl_value =
--------------------------------------------------------------------
-- variable names
vNameL, cNameL, vcNameL, tconNameL :: TH.Name -> CvtM (Located RdrName)
vNameL, cNameL, vcNameL, tNameL, tconNameL :: TH.Name -> CvtM (Located RdrName)
vName, cName, vcName, tName, tconName :: TH.Name -> CvtM RdrName
-- Variable names
......@@ -1181,6 +1208,7 @@ vcNameL n = wrapL (vcName n)
vcName n = if isVarName n then vName n else cName n
-- Type variable names
tNameL n = wrapL (tName n)
tName n = cvtName OccName.tvName n
-- Type Constructor names
......
......@@ -72,6 +72,9 @@ module HsDecls (
AnnProvenance(..), annProvenanceName_maybe,
-- ** Role annotations
RoleAnnotDecl(..), LRoleAnnotDecl, roleAnnotDeclName,
-- ** Injective type families
FamilyResultSig(..), LFamilyResultSig, InjectivityAnn(..), LInjectivityAnn,
resultVariableName,
-- * Grouping
HsGroup(..), emptyRdrGroup, emptyRnGroup, appendGroups
......@@ -108,7 +111,6 @@ import Data.Data hiding (TyCon,Fixity)
import Data.Foldable ( Foldable )
import Data.Traversable ( Traversable )
#endif
import Data.Maybe
{-
************************************************************************
......@@ -465,9 +467,10 @@ data TyClDecl name
-- - 'ApiAnnotation.AnnKeywordId' : 'ApiAnnotation.AnnType',
-- 'ApiAnnotation.AnnData',
-- 'ApiAnnotation.AnnFamily','ApiAnnotation.AnnDcolon',
-- 'ApiAnnotation.AnnWhere',
-- 'ApiAnnotation.AnnOpen','ApiAnnotation.AnnDcolon',
-- 'ApiAnnotation.AnnClose'
-- 'ApiAnnotation.AnnWhere','ApiAnnotation.AnnOpenP',
-- 'ApiAnnotation.AnnDcolon','ApiAnnotation.AnnCloseP',
-- 'ApiAnnotation.AnnEqual','ApiAnnotation.AnnRarrow',
-- 'ApiAnnotation.AnnVbar'
-- For details on above see note [Api annotations] in ApiAnnotation
FamDecl { tcdFam :: FamilyDecl name }
......@@ -545,28 +548,9 @@ tyClGroupConcat = concatMap group_tyclds
mkTyClGroup :: [LTyClDecl name] -> TyClGroup name
mkTyClGroup decls = TyClGroup { group_tyclds = decls, group_roles = [] }
type LFamilyDecl name = Located (FamilyDecl name)
data FamilyDecl name = FamilyDecl
{ fdInfo :: FamilyInfo name -- type or data, closed or open
, fdLName :: Located name -- type constructor
, fdTyVars :: LHsTyVarBndrs name -- type variables
, fdKindSig :: Maybe (LHsKind name) } -- result kind
deriving( Typeable )
deriving instance (DataId id) => Data (FamilyDecl id)
data FamilyInfo name
= DataFamily
| OpenTypeFamily
-- | 'Nothing' if we're in an hs-boot file and the user
-- said "type family Foo x where .."
| ClosedTypeFamily (Maybe [LTyFamInstEqn name])
deriving( Typeable )
deriving instance (DataId name) => Data (FamilyInfo name)
{-
------------------------------
Simple classifiers
-}
-- Simple classifiers for TyClDecl
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-- | @True@ <=> argument is a @data@\/@newtype@
-- declaration.
......@@ -662,38 +646,8 @@ hsDeclHasCusk (SynDecl { tcdTyVars = tyvars, tcdRhs = rhs })
hsDeclHasCusk (DataDecl { tcdTyVars = tyvars }) = hsTvbAllKinded tyvars
hsDeclHasCusk (ClassDecl { tcdTyVars = tyvars }) = hsTvbAllKinded tyvars
-- | Does this family declaration have a complete, user-supplied kind signature?
famDeclHasCusk :: FamilyDecl name -> Bool
famDeclHasCusk (FamilyDecl { fdInfo = ClosedTypeFamily _
, fdTyVars = tyvars
, fdKindSig = m_sig })
= hsTvbAllKinded tyvars && isJust m_sig
famDeclHasCusk _ = True -- all open families have CUSKs!
{-
Note [Complete user-supplied kind signatures]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We kind-check declarations differently if they have a complete, user-supplied
kind signature (CUSK). This is because we can safely generalise a CUSKed
declaration before checking all of the others, supporting polymorphic recursion.
See https://ghc.haskell.org/trac/ghc/wiki/GhcKinds/KindInference#Proposednewstrategy
and #9200 for lots of discussion of how we got here.
A declaration has a CUSK if we can know its complete kind without doing any inference,
at all. Here are the rules:
- A class or datatype is said to have a CUSK if and only if all of its type
variables are annotated. Its result kind is, by construction, Constraint or *
respectively.
- A type synonym has a CUSK if and only if all of its type variables and its
RHS are annotated with kinds.
- A closed type family is said to have a CUSK if and only if all of its type
variables and its return type are annotated.
- An open type family always has a CUSK -- unannotated type variables (and return type) default to *.
-}
-- Pretty-printing TyClDecl
-- ~~~~~~~~~~~~~~~~~~~~~~~~
instance OutputableBndr name
=> Outputable (TyClDecl name) where
......@@ -729,15 +683,223 @@ instance OutputableBndr name => Outputable (TyClGroup name) where
= ppr tyclds $$
ppr roles
pp_vanilla_decl_head :: OutputableBndr name
=> Located name
-> LHsTyVarBndrs name
-> HsContext name
-> SDoc
pp_vanilla_decl_head thing tyvars context
= hsep [pprHsContext context, pprPrefixOcc (unLoc thing), ppr tyvars]
pprTyClDeclFlavour :: TyClDecl a -> SDoc
pprTyClDeclFlavour (ClassDecl {}) = ptext (sLit "class")
pprTyClDeclFlavour (SynDecl {}) = ptext (sLit "type")
pprTyClDeclFlavour (FamDecl { tcdFam = FamilyDecl { fdInfo = info }})
= pprFlavour info
pprTyClDeclFlavour (DataDecl { tcdDataDefn = HsDataDefn { dd_ND = nd } })
= ppr nd
{- *********************************************************************
* *
Data and type family declarations
* *
********************************************************************* -}
-- Note [FamilyResultSig]
-- ~~~~~~~~~~~~~~~~~~~~~~
--
-- This data type represents the return signature of a type family. Possible
-- values are:
--
-- * NoSig - the user supplied no return signature:
-- type family Id a where ...
--
-- * KindSig - the user supplied the return kind:
-- type family Id a :: * where ...
--
-- * TyVarSig - user named the result with a type variable and possibly
-- provided a kind signature for that variable:
-- type family Id a = r where ...
-- type family Id a = (r :: *) where ...
--
-- Naming result of a type family is required if we want to provide
-- injectivity annotation for a type family:
-- type family Id a = r | r -> a where ...
--
-- See also: Note [Injectivity annotation]
-- Note [Injectivity annotation]
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
--
-- A user can declare a type family to be injective:
--
-- type family Id a = r | r -> a where ...
--
-- * The part after the "|" is called "injectivity annotation".