Commit 8c5e7346 authored by eir@cis.upenn.edu's avatar eir@cis.upenn.edu

Fix Trac #7939, and add kind inference to closed type families.

Now, all open type families have result kinds that default to
*. Top-level type families have all arguments default to *,
and associated type families have all arguments that are not
mentioned in the class header default to *. Closed type
families perform kind inference, but generalize only over
those kind variables that are parametric in their use.

This is all a little fiddly and specific, but it seems to follow
use cases. This commit also includes a large
Note [Kind-checking strategies] in TcHsType that helps keep all
of this straight.
parent a7798e95
......@@ -18,6 +18,7 @@ module HsDecls (
TyClDecl(..), LTyClDecl, TyClGroup,
isClassDecl, isDataDecl, isSynDecl, tcdName,
isFamilyDecl, isTypeFamilyDecl, isDataFamilyDecl,
isOpenTypeFamilyInfo, isClosedTypeFamilyInfo,
tyFamInstDeclName, tyFamInstDeclLName,
countTyClDecls, pprTyClDeclFlavour,
tyClDeclLName, tyClDeclTyVars,
......@@ -517,10 +518,21 @@ isTypeFamilyDecl (FamDecl (FamilyDecl { fdInfo = info })) = case info of
_ -> False
isTypeFamilyDecl _ = False
-- | open type family info
isOpenTypeFamilyInfo :: FamilyInfo name -> Bool
isOpenTypeFamilyInfo OpenTypeFamily = True
isOpenTypeFamilyInfo _ = False
-- | closed type family info
isClosedTypeFamilyInfo :: FamilyInfo name -> Bool
isClosedTypeFamilyInfo (ClosedTypeFamily {}) = True
isClosedTypeFamilyInfo _ = False
-- | data family declaration
isDataFamilyDecl :: TyClDecl name -> Bool
isDataFamilyDecl (FamDecl (FamilyDecl { fdInfo = DataFamily })) = True
isDataFamilyDecl _other = False
\end{code}
Dealing with names
......
......@@ -24,7 +24,8 @@ module TcHsType (
-- Kind-checking types
-- No kind generalisation, no checkValidType
kcHsTyVarBndrs, tcHsTyVarBndrs,
KindCheckingStrategy(..), kcStrategy, kcStrategyFamDecl,
kcHsTyVarBndrs, tcHsTyVarBndrs,
tcHsLiftedType, tcHsOpenType,
tcLHsType, tcCheckLHsType,
tcHsContext, tcInferApps, tcHsArgTys,
......@@ -922,7 +923,191 @@ then we'd also need
k is a UserKiVar -> kind variable (they don't need annotation,
since we only have BOX for a super kind)
Note [Kind-checking strategies]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
There are three main declarations that we have to kind check carefully in the
presence of -XPolyKinds: classes, datatypes, and data/type families. They each
have a different kind-checking strategy (labeled in the parentheses above each
section). This should potentially be cleaned up in the future, but this is how
it stands now (June 2013).
Classes (ParametricKinds):
- kind-polymorphic by default
- each un-annotated type variable is given a fresh meta kind variable
- every explicit kind variable becomes a SigTv during inference
- no generalisation is done while kind-checking the recursive group
Taken together, this means that classes cannot participate in polymorphic
recursion. Thus, the following is not definable:
class Fugly (a :: k) where
foo :: forall (b :: k -> *). Fugly b => b a
But, because explicit kind variables are SigTvs, it is OK for the kind to
be forced to be the same kind that is used in a separate declaration. See
test case polykinds/T7020.hs.
Datatypes:
Here we have two cases, whether or not a Full Kind Signature is provided.
A Full Kind Signature means that there is a top-level :: in the definition
of the datatype. For example:
data T1 :: k -> Bool -> * where ... -- YES
data T2 (a :: k) :: Bool -> * where ... -- YES
data T3 (a :: k) (b :: Bool) :: * where ... -- YES
data T4 (a :: k) (b :: Bool) where ... -- NO
Kind signatures are not allowed on datatypes declared in the H98 style,
so those always have no Full Kind Signature.
Full Kind Signature (FullKindSignature):
- each un-annotated type variable defaults to *
- every explicit kind variable becomes a skolem during type inference
- these kind variables are generalised *before* kind-checking the group
With these rules, polymorphic recursion is possible. This is essentially
because of the generalisation step before kind-checking the group -- it
gives the kind-checker enough flexibility to supply the right kind arguments
to support polymorphic recursion.
no Full Kind Signature (ParametricKinds):
- kind-polymorphic by default
- each un-annotated type variable is given a fresh meta kind variable
- every explicit kind variable becomes a SigTv during inference
- no generalisation is done while kind-checking the recursive group
Thus, no polymorphic recursion in this case. See also Trac #6093 & #6049.
Type families:
Here we have three cases: open top-level families, closed top-level families,
and open associated types. (There are no closed associated types, for good
reason.)
Open top-level families (FullKindSignature):
- All open top-level families are considered to have a Full Kind Signature
- All arguments and the result default to *
- All kind variables are skolems
- All kind variables are generalised before kind-checking the group
This behaviour supports kind-indexed type and data families, because we
need to have generalised before kind-checking for this to work. For example:
type family F (a :: k)
type instance F Int = Bool
type instance F Maybe = Char
type instance F (x :: * -> * -> *) = Double
Closed top-level families (NonParametricKinds):
- kind-monomorphic by default
- each un-annotated type variable is given a fresh meta kind variable
- every explicit kind variable becomes a skolem during inference
- all such skolems are generalised before kind-checking; other kind
variables are not generalised
- all unconstrained meta kind variables are defaulted to * at the
end of kind checking
This behaviour is to allow kind inference to occur in closed families, but
without becoming too polymorphic. For example:
type family F a where
F Int = Bool
F Bool = Char
We would want F to have kind * -> * from this definition, although something
like k1 -> k2 would be perfectly sound. The reason we want this restriction is
that it is better to have (F Maybe) be a kind error than simply stuck.
The kind inference gives us also
type family Not b where
Not False = True
Not True = False
With an open family, the above would need kind annotations in its header.
The tricky case is
type family G a (b :: k) where
G Int Int = False
G Bool Maybe = True
We want this to work. But, we also want (G Maybe Maybe) to be a kind error
(in the first argument). So, we need to generalise the skolem "k" but not
the meta kind variable associated with "a".
Associated families (FullKindSignature):
- Kind-monomorphic by default
- Result kind defaults to *
- Each type variable is either in the class header or not:
- Type variables in the class header are given the kind inherited from
the class header (and checked against an annotation, if any)
- Un-annotated type variables default to *
- Each kind variable mentioned in the class header becomes a SigTv during
kind inference.
- Each kind variable not mentioned in the class header becomes a skolem during
kind inference.
- Only the skolem kind variables are generalised before kind checking.
Here are some examples:
class Foo1 a b where
type Bar1 (a :: k) (b :: k)
The kind of Foo1 will be k -> k -> Constraint. Kind annotations on associated
type declarations propagate to the header because the type variables in Bar1's
declaration inherit the (meta) kinds of the class header.
class Foo2 a where
type Bar2 a
The kind of Bar2 will be k -> *.
class Foo3 a where
type Bar3 a (b :: k)
meth :: Bar3 a Maybe -> ()
The kind of Bar3 will be k1 -> k2 -> *. This only kind-checks because the kind
of b is generalised before kind-checking.
class Foo4 a where
type Bar4 a b
Here, the kind of Bar4 will be k -> * -> *, because b is not mentioned in the
class header, so it defaults to *.
\begin{code}
data KindCheckingStrategy -- See Note [Kind-checking strategies]
= ParametricKinds
| NonParametricKinds
| FullKindSignature
-- determine the appropriate strategy for a decl
kcStrategy :: TyClDecl Name -> KindCheckingStrategy
kcStrategy d@(ForeignType {}) = pprPanic "kcStrategy" (ppr d)
kcStrategy (FamDecl fam_decl)
= kcStrategyFamDecl fam_decl
kcStrategy (SynDecl {}) = ParametricKinds
kcStrategy (DataDecl { tcdDataDefn = HsDataDefn { dd_kindSig = m_ksig }})
| Just _ <- m_ksig = FullKindSignature
| otherwise = ParametricKinds
kcStrategy (ClassDecl {}) = ParametricKinds
kcStrategyFamDecl :: FamilyDecl Name -> KindCheckingStrategy
kcStrategyFamDecl (FamilyDecl { fdInfo = info })
| isClosedTypeFamilyInfo info = NonParametricKinds
| otherwise = FullKindSignature
mkKindSigVar :: Name -> TcM KindVar
-- Use the specified name; don't clone it
mkKindSigVar n
= do { mb_thing <- tcLookupLcl_maybe n
; case mb_thing of
Just (AThing k)
| Just kvar <- getTyVar_maybe k
-> return kvar
_ -> return $ mkTcTyVar n superKind (SkolemTv False) }
kcScopedKindVars :: [Name] -> TcM a -> TcM a
-- Given some tyvar binders like [a (b :: k -> *) (c :: k)]
-- bind each scoped kind variable (k in this case) to a fresh
......@@ -932,28 +1117,39 @@ kcScopedKindVars kv_ns thing_inside
-- NB: use mutable signature variables
; tcExtendTyVarEnv2 (kv_ns `zip` kvs) thing_inside }
kcHsTyVarBndrs :: Bool -- True <=> full kind signature provided
-- Default UserTyVar to *
-- and use KindVars not meta kind vars
kcHsTyVarBndrs :: KindCheckingStrategy
-> LHsTyVarBndrs Name
-> ([TcKind] -> TcM r)
-> TcM r
-> TcM (Kind, r) -- the result kind, possibly with other info
-> TcM (Kind, r)
-- Used in getInitialKind
kcHsTyVarBndrs full_kind_sig (HsQTvs { hsq_kvs = kv_ns, hsq_tvs = hs_tvs }) thing_inside
= do { kvs <- if full_kind_sig
then return (map mkKindSigVar kv_ns)
kcHsTyVarBndrs strat (HsQTvs { hsq_kvs = kv_ns, hsq_tvs = hs_tvs }) thing_inside
= do { kvs <- if skolem_kvs
then mapM mkKindSigVar kv_ns
else mapM (\n -> newSigTyVar n superKind) kv_ns
; tcExtendTyVarEnv2 (kv_ns `zip` kvs) $
do { nks <- mapM (kc_hs_tv . unLoc) hs_tvs
; tcExtendKindEnv nks (thing_inside (map snd nks)) } }
; (res_kind, stuff) <- tcExtendKindEnv nks thing_inside
; let full_kind = mkArrowKinds (map snd nks) res_kind
kvs = filter (not . isMetaTyVar) $
varSetElems $ tyVarsOfType full_kind
gen_kind = if generalise
then mkForAllTys kvs full_kind
else full_kind
; return (gen_kind, stuff) } }
where
-- See Note [Kind-checking strategies]
(skolem_kvs, default_to_star, generalise) = case strat of
ParametricKinds -> (False, False, False)
NonParametricKinds -> (True, False, True)
FullKindSignature -> (True, True, True)
kc_hs_tv :: HsTyVarBndr Name -> TcM (Name, TcKind)
kc_hs_tv (UserTyVar n)
= do { mb_thing <- tcLookupLcl_maybe n
; kind <- case mb_thing of
Just (AThing k) -> return k
_ | full_kind_sig -> return liftedTypeKind
| otherwise -> newMetaKindVar
Just (AThing k) -> return k
_ | default_to_star -> return liftedTypeKind
| otherwise -> newMetaKindVar
; return (n, kind) }
kc_hs_tv (KindedTyVar n k)
= do { kind <- tcLHsKind k
......@@ -973,7 +1169,7 @@ tcHsTyVarBndrs :: LHsTyVarBndrs Name
-- Bind the kind variables to fresh skolem variables
-- and type variables to skolems, each with a meta-kind variable kind
tcHsTyVarBndrs (HsQTvs { hsq_kvs = kv_ns, hsq_tvs = hs_tvs }) thing_inside
= do { let kvs = map mkKindSigVar kv_ns
= do { kvs <- mapM mkKindSigVar kv_ns
; tcExtendTyVarEnv kvs $ do
{ tvs <- mapM tcHsTyVarBndr hs_tvs
; traceTc "tcHsTyVarBndrs {" (vcat [ text "Hs kind vars:" <+> ppr kv_ns
......
......@@ -25,7 +25,7 @@ module TcMType (
newFlexiTyVarTy, -- Kind -> TcM TcType
newFlexiTyVarTys, -- Int -> Kind -> TcM [TcType]
newPolyFlexiTyVarTy,
newMetaKindVar, newMetaKindVars, mkKindSigVar,
newMetaKindVar, newMetaKindVars,
mkTcTyVarName, cloneMetaTyVar,
newMetaTyVar, readMetaTyVar, writeMetaTyVar, writeMetaTyVarRef,
......@@ -112,10 +112,6 @@ newMetaKindVar = do { uniq <- newUnique
newMetaKindVars :: Int -> TcM [TcKind]
newMetaKindVars n = mapM (\ _ -> newMetaKindVar) (nOfThem n ())
mkKindSigVar :: Name -> KindVar
-- Use the specified name; don't clone it
mkKindSigVar n = mkTcTyVar n superKind (SkolemTv False)
\end{code}
......@@ -527,13 +523,12 @@ quantifyTyVars gbl_tvs tkvs
-- may make quantifyTyVars return a shorter list
-- than it was passed, but that's ok
; poly_kinds <- xoptM Opt_PolyKinds
; qkvs <- if poly_kinds
; qkvs <- if poly_kinds
then return kvs2
else do { let (meta_kvs, skolem_kvs) = partition is_meta kvs2
is_meta kv = isTcTyVar kv && isMetaTyVar kv
; mapM_ defaultKindVarToStar meta_kvs
; WARN( not (null skolem_kvs), ppr skolem_kvs )
return skolem_kvs } -- Should be empty
; return skolem_kvs } -- should be empty
; mapM zonk_quant (qkvs ++ qtvs) }
-- Because of the order, any kind variables
......
......@@ -199,9 +199,9 @@ Note [Kind checking for type and class decls]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Kind checking is done thus:
1. Make up a kind variable for each parameter of the *data* type,
and class, decls, and extend the kind environment (which is in
the TcLclEnv)
1. Make up a kind variable for each parameter of the *data* type, class,
and closed type family decls, and extend the kind environment (which is
in the TcLclEnv)
2. Dependency-analyse the type *synonyms* (which must be non-recursive),
and kind-check them in dependency order. Extend the kind envt.
......@@ -236,18 +236,17 @@ So we must infer their kinds from their right-hand sides *first* and then
use them, whereas for the mutually recursive data types D we bring into
scope kind bindings D -> k, where k is a kind variable, and do inference.
Type families
~~~~~~~~~~~~~
Open type families
~~~~~~~~~~~~~~~~~~
This treatment of type synonyms only applies to Haskell 98-style synonyms.
General type functions can be recursive, and hence, appear in `alg_decls'.
The kind of a type family is solely determinded by its kind signature;
The kind of an open type family is solely determinded by its kind signature;
hence, only kind signatures participate in the construction of the initial
kind environment (as constructed by `getInitialKind'). In fact, we ignore
instances of families altogether in the following. However, we need to
include the kinds of *associated* families into the construction of the
initial kind environment. (This is handled by `allDecls').
kind environment (as constructed by `getInitialKind'). In fact, we ignore
instances of families altogether in the following. However, we need to include
the kinds of *associated* families into the construction of the initial kind
environment. (This is handled by `allDecls').
\begin{code}
kcTyClGroup :: TyClGroup Name -> TcM [(Name,Kind)]
......@@ -267,7 +266,7 @@ kcTyClGroup decls
-- Step 1: Bind kind variables for non-synonyms
; let (syn_decls, non_syn_decls) = partition (isSynDecl . unLoc) decls
; initial_kinds <- getInitialKinds TopLevel non_syn_decls
; initial_kinds <- getInitialKinds non_syn_decls
; traceTc "kcTyClGroup: initial kinds" (ppr initial_kinds)
-- Step 2: Set initial envt, kind-check the synonyms
......@@ -314,7 +313,6 @@ kcTyClGroup decls
= pprPanic "generaliseTCD" (ppr decl)
| otherwise
-- Note: tcdTyVars is safe here because we've eliminated FamDecl and ForeignType
= do { res <- generalise kind_env (tcdName decl)
; return [res] }
......@@ -334,12 +332,13 @@ mk_thing_env (decl : decls)
= (tcdName (unLoc decl), APromotionErr TyConPE) :
(mk_thing_env decls)
getInitialKinds :: TopLevelFlag -> [LTyClDecl Name] -> TcM [(Name, TcTyThing)]
getInitialKinds top_lvl decls
getInitialKinds :: [LTyClDecl Name] -> TcM [(Name, TcTyThing)]
getInitialKinds decls
= tcExtendTcTyThingEnv (mk_thing_env decls) $
concatMapM (addLocM (getInitialKind top_lvl)) decls
concatMapM (addLocM getInitialKind) decls
getInitialKind :: TopLevelFlag -> TyClDecl Name -> TcM [(Name, TcTyThing)]
-- See Note [Kind-checking strategies] in TcHsType
getInitialKind :: TyClDecl Name -> TcM [(Name, TcTyThing)]
-- Allocate a fresh kind variable for each TyCon and Class
-- For each tycon, return (tc, AThing k)
-- where k is the kind of tc, derived from the LHS
......@@ -357,39 +356,36 @@ getInitialKind :: TopLevelFlag -> TyClDecl Name -> TcM [(Name, TcTyThing)]
--
-- No family instances are passed to getInitialKinds
getInitialKind _ (ClassDecl { tcdLName = L _ name, tcdTyVars = ktvs, tcdATs = ats })
= kcHsTyVarBndrs False ktvs $ \ arg_kinds ->
do { inner_prs <- getFamDeclInitialKinds ats
; let main_pr = (name, AThing (mkArrowKinds arg_kinds constraintKind))
; return (main_pr : inner_prs) }
getInitialKind top_lvl (DataDecl { tcdLName = L _ name, tcdTyVars = ktvs, tcdDataDefn = defn })
| HsDataDefn { dd_kindSig = Just ksig, dd_cons = cons } <- defn
= ASSERT( isTopLevel top_lvl )
kcHsTyVarBndrs True ktvs $ \ arg_kinds ->
do { res_k <- tcLHsKind ksig
; let body_kind = mkArrowKinds arg_kinds res_k
kvs = varSetElems (tyVarsOfType body_kind)
main_pr = (name, AThing (mkForAllTys kvs body_kind))
inner_prs = [(unLoc (con_name con), APromotionErr RecDataConPE) | L _ con <- cons ]
-- See Note [Recusion and promoting data constructors]
getInitialKind decl@(ClassDecl { tcdLName = L _ name, tcdTyVars = ktvs, tcdATs = ats })
= do { (cl_kind, inner_prs) <-
kcHsTyVarBndrs (kcStrategy decl) ktvs $
do { inner_prs <- getFamDeclInitialKinds ats
; return (constraintKind, inner_prs) }
; let main_pr = (name, AThing cl_kind)
; return (main_pr : inner_prs) }
| HsDataDefn { dd_cons = cons } <- defn
= kcHsTyVarBndrs False ktvs $ \ arg_kinds ->
do { let main_pr = (name, AThing (mkArrowKinds arg_kinds liftedTypeKind))
getInitialKind decl@(DataDecl { tcdLName = L _ name
, tcdTyVars = ktvs
, tcdDataDefn = HsDataDefn { dd_kindSig = m_sig
, dd_cons = cons } })
= do { (decl_kind, _) <-
kcHsTyVarBndrs (kcStrategy decl) ktvs $
do { res_k <- case m_sig of
Just ksig -> tcLHsKind ksig
Nothing -> return liftedTypeKind
; return (res_k, ()) }
; let main_pr = (name, AThing decl_kind)
inner_prs = [ (unLoc (con_name con), APromotionErr RecDataConPE)
| L _ con <- cons ]
-- See Note [Recusion and promoting data constructors]
; return (main_pr : inner_prs) }
getInitialKind top_lvl (FamDecl { tcdFam = decl })
= getFamDeclInitialKind top_lvl decl
getInitialKind (FamDecl { tcdFam = decl })
= getFamDeclInitialKind decl
getInitialKind _ (ForeignType { tcdLName = L _ name })
getInitialKind (ForeignType { tcdLName = L _ name })
= return [(name, AThing liftedTypeKind)]
getInitialKind _top_lvl decl@(SynDecl {})
getInitialKind decl@(SynDecl {})
= pprPanic "getInitialKind" (ppr decl)
---------------------------------
......@@ -397,29 +393,25 @@ getFamDeclInitialKinds :: [LFamilyDecl Name] -> TcM [(Name, TcTyThing)]
getFamDeclInitialKinds decls
= tcExtendTcTyThingEnv [ (n, APromotionErr TyConPE)
| L _ (FamilyDecl { fdLName = L _ n }) <- decls] $
concatMapM (addLocM (getFamDeclInitialKind NotTopLevel)) decls
concatMapM (addLocM getFamDeclInitialKind) decls
getFamDeclInitialKind :: TopLevelFlag
-> FamilyDecl Name
getFamDeclInitialKind :: FamilyDecl Name
-> TcM [(Name, TcTyThing)]
getFamDeclInitialKind top_lvl (FamilyDecl { fdLName = L _ name
, fdTyVars = ktvs
, fdKindSig = ksig })
| isTopLevel top_lvl
= kcHsTyVarBndrs True ktvs $ \ arg_kinds ->
do { res_k <- case ksig of
Just k -> tcLHsKind k
Nothing -> return liftedTypeKind
; let body_kind = mkArrowKinds arg_kinds res_k
kvs = varSetElems (tyVarsOfType body_kind)
; return [ (name, AThing (mkForAllTys kvs body_kind)) ] }
| otherwise
= kcHsTyVarBndrs False ktvs $ \ arg_kinds ->
do { res_k <- case ksig of
Just k -> tcLHsKind k
Nothing -> newMetaKindVar
; return [ (name, AThing (mkArrowKinds arg_kinds res_k)) ] }
getFamDeclInitialKind decl@(FamilyDecl { fdLName = L _ name
, fdInfo = info
, fdTyVars = ktvs
, fdKindSig = ksig })
= do { (fam_kind, _) <-
kcHsTyVarBndrs (kcStrategyFamDecl decl) ktvs $
do { res_k <- case ksig of
Just k -> tcLHsKind k
Nothing
| defaultResToStar -> return liftedTypeKind
| otherwise -> newMetaKindVar
; return (res_k, ()) }
; return [ (name, AThing fam_kind) ] }
where
defaultResToStar = not $ isClosedTypeFamilyInfo info
----------------
kcSynDecls :: [SCC (LTyClDecl Name)] -> TcM TcLclEnv -- Kind bindings
......@@ -440,13 +432,13 @@ kcSynDecl decl@(SynDecl { tcdTyVars = hs_tvs, tcdLName = L _ name
, tcdRhs = rhs })
-- Returns a possibly-unzonked kind
= tcAddDeclCtxt decl $
kcHsTyVarBndrs False hs_tvs $ \ ks ->
do { traceTc "kcd1" (ppr name <+> brackets (ppr hs_tvs)
<+> brackets (ppr ks))
; (_, rhs_kind) <- tcLHsType rhs
; traceTc "kcd2" (ppr name)
; let tc_kind = mkArrowKinds ks rhs_kind
; return (name, tc_kind) }
do { (syn_kind, _) <-
kcHsTyVarBndrs (kcStrategy decl) hs_tvs $
do { traceTc "kcd1" (ppr name <+> brackets (ppr hs_tvs))
; (_, rhs_kind) <- tcLHsType rhs
; traceTc "kcd2" (ppr name)
; return (rhs_kind, ()) }
; return (name, syn_kind) }
kcSynDecl decl = pprPanic "kcSynDecl" (ppr decl)
------------------------------------------------------------------------
......@@ -485,6 +477,13 @@ kcTyClDecl (ClassDecl { tcdLName = L _ name, tcdTyVars = hs_tvs
kc_sig _ = return ()
kcTyClDecl (ForeignType {}) = return ()
-- closed type families look at their equations, but other families don't
-- do anything here
kcTyClDecl (FamDecl (FamilyDecl { fdLName = L _ fam_tc_name
, fdInfo = ClosedTypeFamily eqns }))
= do { k <- kcLookupKind fam_tc_name
; mapM_ (kcTyFamInstEqn fam_tc_name k) eqns }
kcTyClDecl (FamDecl {}) = return ()
-------------------
......@@ -492,10 +491,11 @@ kcConDecl :: ConDecl Name -> TcM ()
kcConDecl (ConDecl { con_name = name, con_qvars = ex_tvs
, con_cxt = ex_ctxt, con_details = details, con_res = res })
= addErrCtxt (dataConCtxt name) $
kcHsTyVarBndrs False ex_tvs $ \ _ ->
do { _ <- tcHsContext ex_ctxt
; mapM_ (tcHsOpenType . getBangType) (hsConDeclArgTys details)
; _ <- tcConRes res
do { _ <- kcHsTyVarBndrs ParametricKinds ex_tvs $
do { _ <- tcHsContext ex_ctxt
; mapM_ (tcHsOpenType . getBangType) (hsConDeclArgTys details)
; _ <- tcConRes res
; return (panic "kcConDecl", ()) }
; return () }
\end{code}
......@@ -845,6 +845,13 @@ tcSynFamInstNames (L _ first) names
= setSrcSpan loc $
failWithTc (msg_fun name)
kcTyFamInstEqn :: Name -> Kind -> LTyFamInstEqn Name -> TcM ()
kcTyFamInstEqn fam_tc_name kind
(L loc (TyFamInstEqn { tfie_pats = pats, tfie_rhs = hs_ty }))
= setSrcSpan loc $
discardResult $
tc_fam_ty_pats fam_tc_name kind pats (discardResult . (tcCheckLHsType hs_ty))
tcTyFamInstEqn :: Name -> Kind -> LTyFamInstEqn Name -> TcM CoAxBranch
tcTyFamInstEqn fam_tc_name kind
(L loc (TyFamInstEqn { tfie_pats = pats, tfie_rhs = hs_ty }))
......@@ -873,26 +880,36 @@ kcResultKind Nothing res_k
kcResultKind (Just k) res_k
= do { k' <- tcLHsKind k
; checkKind k' res_k }
\end{code}
-------------------------
-- Kind check type patterns and kind annotate the embedded type variables.
-- type instance F [a] = rhs
--
-- * Here we check that a type instance matches its kind signature, but we do
-- not check whether there is a pattern for each type index; the latter
-- check is only required for type synonym instances.
Kind check type patterns and kind annotate the embedded type variables.
type instance F [a] = rhs
* Here we check that a type instance matches its kind signature, but we do
not check whether there is a pattern for each type index; the latter
check is only required for type synonym instances.
Note [tc_fam_ty_pats vs tcFamTyPats]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
tc_fam_ty_pats does the type checking of the patterns, but it doesn't
zonk or generate any desugaring. It is used when kind-checking closed
type families.
tcFamTyPats type checks the patterns, zonks, and then calls thing_inside
to generate a desugaring. It is used during type-checking (not kind-checking).
\begin{code}
-----------------
-- Note that we can't use the family TyCon, because this is sometimes called
-- from within a type-checking knot. So, we ask our callers to do a little more
-- work.
tcFamTyPats :: Name -- of the family TyCon
-> Kind -- of the family TyCon
-> HsWithBndrs [LHsType Name] -- Patterns
-> (TcKind -> TcM ()) -- Kind checker for RHS
-- result is ignored
-> ([TKVar] -> [TcType] -> Kind -> TcM a)
-> TcM a
-- See Note [tc_fam_ty_pats vs tcFamTyPats]
tc_fam_ty_pats :: Name -- of the family TyCon
-> Kind -- of the family TyCon
-> HsWithBndrs [LHsType Name] -- Patterns
-> (TcKind -> TcM ()) -- Kind checker for RHS
-- result is ignored
-> TcM ([Kind], [Type], Kind)
-- Check the type patterns of a type or data family instance
-- type instance F <pat1> <pat2> = <type>
-- The 'tyvars' are the free type variables of pats
......@@ -904,9 +921,9 @@ tcFamTyPats :: Name -- of the family TyCon
-- In that case, the type variable 'a' will *already be in scope*
-- (and, if C is poly-kinded, so will its kind parameter).
tcFamTyPats fam_tc_name kind
(HsWB { hswb_cts = arg_pats, hswb_kvs = kvars, hswb_tvs = tvars })
kind_checker thing_inside
tc_fam_ty_pats fam_tc_name kind
(HsWB { hswb_cts = arg_pats, hswb_kvs = kvars, hswb_tvs = tvars })
kind_checker
= do { let (fam_kvs, fam_body) = splitForAllTys kind
-- We wish to check that the pattern has the right number of arguments
......@@ -934,6 +951,19 @@ tcFamTyPats fam_tc_name kind
; typats <- tcHsTyVarBndrs hs_tvs $ \ _ ->
do { kind_checker res_kind
; tcHsArgTys (quotes (ppr fam_tc_name)) arg_pats arg_kinds }
; return (fam_arg_kinds, typats, res_kind) }
-- See Note [tc_fam_ty_pats vs tcFamTyPats]
tcFamTyPats :: Name -- of the family ToCon
-> Kind -- of the family TyCon
-> HsWithBndrs [LHsType Name] -- patterns
-> (TcKind -> TcM ()) -- kind-checker for RHS
-> ([TKVar] -> [TcType] -> Kind -> TcM a)
-> TcM a
tcFamTyPats fam_tc_name kind pats kind_checker thing_inside
= do { (fam_arg_kinds, typats, res_kind)
<- tc_fam_ty_pats fam_tc_name kind pats kind_checker
; let all_args = fam_arg_kinds ++ typats
-- Find free variables (after zonking) and turn
......
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