Commit 3fe3ef50 authored by Simon Peyton Jones's avatar Simon Peyton Jones
Browse files

More changes to kind inference for type and class declarations

These should fix #7024 and #7022, among others.

The main difficulty was that we were getting occ-name clashes
between kind and type variables in TyCons, when spat into an
interface file. The new scheme is to tidy TyCons during the
conversoin into IfaceSyn, rather than trying to generate them
pre-tidied, which was the already-unsatisfactory previous plan.

There is the usual wave of refactorig as well.
parent cdcd0749
......@@ -1433,19 +1433,45 @@ checkList (check:checks) = do recompile <- check
\begin{code}
tyThingToIfaceDecl :: TyThing -> IfaceDecl
-- Assumption: the thing is already tidied, so that locally-bound names
-- (lambdas, for-alls) already have non-clashing OccNames
-- Reason: Iface stuff uses OccNames, and the conversion here does
-- not do tidying on the way
tyThingToIfaceDecl (AnId id)
tyThingToIfaceDecl (AnId id) = idToIfaceDecl id
tyThingToIfaceDecl (ATyCon tycon) = tyConToIfaceDecl emptyTidyEnv tycon
tyThingToIfaceDecl (ACoAxiom ax) = coAxiomToIfaceDecl ax
tyThingToIfaceDecl (ADataCon dc) = pprPanic "toIfaceDecl" (ppr dc)
-- Should be trimmed out earlier
--------------------------
idToIfaceDecl :: Id -> IfaceDecl
-- The Id is already tidied, so that locally-bound names
-- (lambdas, for-alls) already have non-clashing OccNames
-- We can't tidy it here, locally, because it may have
-- free variables in its type or IdInfo
idToIfaceDecl id
= IfaceId { ifName = getOccName id,
ifType = toIfaceType (idType id),
ifIdDetails = toIfaceIdDetails (idDetails id),
ifIdInfo = toIfaceIdInfo (idInfo id) }
tyThingToIfaceDecl (ATyCon tycon)
--------------------------
coAxiomToIfaceDecl :: CoAxiom -> IfaceDecl
-- We *do* tidy Axioms, because they are not (and cannot
-- conveniently be) built in tidy form
coAxiomToIfaceDecl ax
= IfaceAxiom { ifName = name
, ifTyVars = toIfaceTvBndrs tv_bndrs
, ifLHS = tidyToIfaceType env (coAxiomLHS ax)
, ifRHS = tidyToIfaceType env (coAxiomRHS ax) }
where
name = getOccName ax
(env, tv_bndrs) = tidyTyVarBndrs emptyTidyEnv (coAxiomTyVars ax)
-----------------
tyConToIfaceDecl :: TidyEnv -> TyCon -> IfaceDecl
-- We *do* tidy TyCons, because they are not (and cannot
-- conveniently be) built in tidy form
tyConToIfaceDecl env tycon
| Just clas <- tyConClass_maybe tycon
= classToIfaceDecl clas
= classToIfaceDecl env clas
| isSynTyCon tycon
= IfaceSyn { ifName = getOccName tycon,
......@@ -1457,7 +1483,7 @@ tyThingToIfaceDecl (ATyCon tycon)
= IfaceData { ifName = getOccName tycon,
ifCType = tyConCType tycon,
ifTyVars = toIfaceTvBndrs tyvars,
ifCtxt = toIfaceContext (tyConStupidTheta tycon),
ifCtxt = tidyToIfaceContext env1 (tyConStupidTheta tycon),
ifCons = ifaceConDecls (algTyConRhs tycon),
ifRec = boolToRecFlag (isRecursiveTyCon tycon),
ifGadtSyntax = isGadtSyntaxTyCon tycon,
......@@ -1469,16 +1495,15 @@ tyThingToIfaceDecl (ATyCon tycon)
| otherwise = pprPanic "toIfaceDecl" (ppr tycon)
where
tyvars = tyConTyVars tycon
(env1, tyvars) = tidyTyVarBndrs env (tyConTyVars tycon)
(syn_rhs, syn_ki)
= case synTyConRhs tycon of
SynFamilyTyCon -> (Nothing, toIfaceType (synTyConResKind tycon))
SynonymTyCon ty -> (Just (toIfaceType ty), toIfaceType (typeKind ty))
SynFamilyTyCon -> (Nothing, tidyToIfaceType env1 (synTyConResKind tycon))
SynonymTyCon ty -> (Just (toIfaceType ty), tidyToIfaceType env1 (typeKind ty))
ifaceConDecls (NewTyCon { data_con = con }) =
IfNewTyCon (ifaceConDecl con)
ifaceConDecls (DataTyCon { data_cons = cons }) =
IfDataTyCon (map ifaceConDecl cons)
ifaceConDecls (NewTyCon { data_con = con }) = IfNewTyCon (ifaceConDecl con)
ifaceConDecls (DataTyCon { data_cons = cons }) = IfDataTyCon (map ifaceConDecl cons)
ifaceConDecls DataFamilyTyCon {} = IfDataFamTyCon
ifaceConDecls (AbstractTyCon distinct) = IfAbstractTyCon distinct
-- The last case happens when a TyCon has been trimmed during tidying
......@@ -1490,39 +1515,27 @@ tyThingToIfaceDecl (ATyCon tycon)
= IfCon { ifConOcc = getOccName (dataConName data_con),
ifConInfix = dataConIsInfix data_con,
ifConWrapper = isJust (dataConWrapId_maybe data_con),
ifConUnivTvs = toIfaceTvBndrs univ_tvs,
ifConExTvs = toIfaceTvBndrs ex_tvs,
ifConUnivTvs = toIfaceTvBndrs univ_tvs',
ifConExTvs = toIfaceTvBndrs ex_tvs',
ifConEqSpec = to_eq_spec eq_spec,
ifConCtxt = toIfaceContext theta,
ifConArgTys = map toIfaceType arg_tys,
ifConCtxt = tidyToIfaceContext env3 theta,
ifConArgTys = map (tidyToIfaceType env3) arg_tys,
ifConFields = map getOccName
(dataConFieldLabels data_con),
ifConStricts = dataConStrictMarks data_con }
where
(univ_tvs, ex_tvs, eq_spec, theta, arg_tys, _) = dataConFullSig data_con
(env2, univ_tvs') = tidyTyClTyVarBndrs env1 univ_tvs
(env3, ex_tvs') = tidyTyVarBndrs env2 ex_tvs
to_eq_spec spec = [ (getOccName (tidyTyVar env3 tv), tidyToIfaceType env3 ty)
| (tv,ty) <- spec]
to_eq_spec spec = [(getOccName tv, toIfaceType ty) | (tv,ty) <- spec]
tyThingToIfaceDecl (ACoAxiom ax)
= IfaceAxiom { ifName = name
, ifTyVars = tv_bndrs
, ifLHS = lhs
, ifRHS = rhs }
where
name = getOccName ax
tv_bndrs = toIfaceTvBndrs (coAxiomTyVars ax)
lhs = toIfaceType (coAxiomLHS ax)
rhs = toIfaceType (coAxiomRHS ax)
tyThingToIfaceDecl (ADataCon dc)
= pprPanic "toIfaceDecl" (ppr dc) -- Should be trimmed out earlier
classToIfaceDecl :: Class -> IfaceDecl
classToIfaceDecl clas
= IfaceClass { ifCtxt = toIfaceContext sc_theta,
classToIfaceDecl :: TidyEnv -> Class -> IfaceDecl
classToIfaceDecl env clas
= IfaceClass { ifCtxt = tidyToIfaceContext env1 sc_theta,
ifName = getOccName (classTyCon clas),
ifTyVars = toIfaceTvBndrs clas_tyvars,
ifTyVars = toIfaceTvBndrs clas_tyvars',
ifFDs = map toIfaceFD clas_fds,
ifATs = map toIfaceAT clas_ats,
ifSigs = map toIfaceClassOp op_stuff,
......@@ -1532,17 +1545,23 @@ classToIfaceDecl clas
= classExtraBigSig clas
tycon = classTyCon clas
(env1, clas_tyvars') = tidyTyVarBndrs env clas_tyvars
toIfaceAT :: ClassATItem -> IfaceAT
toIfaceAT (tc, defs)
= IfaceAT (tyThingToIfaceDecl (ATyCon tc))
(map to_if_at_def defs)
= IfaceAT (tyConToIfaceDecl env1 tc) (map to_if_at_def defs)
where
to_if_at_def (ATD tvs pat_tys ty _loc)
= IfaceATD (toIfaceTvBndrs tvs) (map toIfaceType pat_tys) (toIfaceType ty)
= IfaceATD (toIfaceTvBndrs tvs')
(map (tidyToIfaceType env2) pat_tys)
(tidyToIfaceType env2 ty)
where
(env2, tvs') = tidyTyClTyVarBndrs env1 tvs
toIfaceClassOp (sel_id, def_meth)
= ASSERT(sel_tyvars == clas_tyvars)
IfaceClassOp (getOccName sel_id) (toDmSpec def_meth) (toIfaceType op_ty)
IfaceClassOp (getOccName sel_id) (toDmSpec def_meth)
(tidyToIfaceType env1 op_ty)
where
-- Be careful when splitting the type, because of things
-- like class Foo a where
......@@ -1556,8 +1575,30 @@ classToIfaceDecl clas
toDmSpec (GenDefMeth _) = GenericDM
toDmSpec (DefMeth _) = VanillaDM
toIfaceFD (tvs1, tvs2) = (map getFS tvs1, map getFS tvs2)
toIfaceFD (tvs1, tvs2) = (map (getFS . tidyTyVar env1) tvs1,
map (getFS . tidyTyVar env1) tvs2)
--------------------------
tidyToIfaceType :: TidyEnv -> Type -> IfaceType
tidyToIfaceType env ty = toIfaceType (tidyType env ty)
tidyToIfaceContext :: TidyEnv -> ThetaType -> IfaceContext
tidyToIfaceContext env theta = map (tidyToIfaceType env) theta
tidyTyClTyVarBndrs :: TidyEnv -> [TyVar] -> (TidyEnv, [TyVar])
tidyTyClTyVarBndrs env tvs = mapAccumL tidyTyClTyVarBndr env tvs
tidyTyClTyVarBndr :: TidyEnv -> TyVar -> (TidyEnv, TyVar)
-- If the type variable "binder" is in scope, don't re-bind it
-- In a class decl, for example, the ATD binders mention
-- (amd must mention) the class tyvars
tidyTyClTyVarBndr env@(_, subst) tv
| Just tv' <- lookupVarEnv subst tv = (env, tv')
| otherwise = tidyTyVarBndr env tv
tidyTyVar :: TidyEnv -> TyVar -> TyVar
tidyTyVar (_, subst) tv = lookupVarEnv subst tv `orElse` tv
-- TcType.tidyTyVarOcc messes around with FlatSkols
getFS :: NamedThing a => a -> FastString
getFS x = occNameFS (getOccName x)
......
......@@ -30,7 +30,7 @@ module TcHsType (
tcHsContext, tcInferApps, tcHsArgTys,
ExpKind(..), ekConstraint, expArgKind, checkExpectedKind,
bindScopedKindVars, kindGeneralize,
kindGeneralize,
-- Sort-checking kinds
tcLHsKind,
......@@ -292,7 +292,7 @@ tcCheckHsTypeAndGen :: HsType Name -> Kind -> TcM Type
-- The result is not necessarily zonked, and has not been checked for validity
tcCheckHsTypeAndGen hs_ty kind
= do { ty <- tc_hs_type hs_ty (EK kind (ptext (sLit "Expected")))
; kvs <- kindGeneralize (tyVarsOfType ty)
; kvs <- kindGeneralize (tyVarsOfType ty) []
; return (mkForAllTys kvs ty) }
\end{code}
......@@ -583,16 +583,10 @@ tcTyVar name -- Could be a tyvar, a tycon, or a datacon
ty = dataConUserType dc
tc = buildPromotedDataCon dc
AFamDataCon -> bad_promote (ptext (sLit "it comes from a data family instance"))
ARecDataCon -> bad_promote (ptext (sLit "it is defined and used in the same recursive group"))
APromotionErr err -> promotionErr name err
_ -> wrongThingErr "type" thing name }
where
bad_promote reason
= failWithTc (hang (ptext (sLit "You can't use data constructor") <+> quotes (ppr name)
<+> ptext (sLit "here"))
2 (parens reason))
get_loopy_tc name
= do { env <- getGblEnv
; case lookupNameEnv (tcg_type_env env) name of
......@@ -793,42 +787,53 @@ then we'd also need
since we only have BOX for a super kind)
\begin{code}
bindScopedKindVars :: [Name] -> ([KindVar] -> TcM a) -> TcM a
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
-- kind skolem variable
bindScopedKindVars kv_ns thing_inside
= tcExtendTyVarEnv kvs (thing_inside kvs)
where
kvs = map mkKindSigVar kv_ns
kcScopedKindVars kv_ns thing_inside
= do { kvs <- mapM (\n -> newSigTyVar n superKind) kv_ns
-- NB: use mutable signature variables
; tcExtendTyVarEnv2 (kv_ns `zip` kvs) thing_inside }
kcHsTyVarBndrs :: Bool -- Default UserTyVar to *
-- and use KindVars not meta kind vars
-> LHsTyVarBndrs Name
-> ([TcKind] -> TcM r)
-> TcM r
kcHsTyVarBndrs default_to_star (HsQTvs { hsq_kvs = kvs, hsq_tvs = hs_tvs }) thing_inside
= bindScopedKindVars kvs $ \ _ ->
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)
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)) }
; tcExtendKindEnv nks (thing_inside (map snd nks)) } }
where
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
_ | default_to_star -> return liftedTypeKind
| otherwise -> newMetaKindVar
Just (AThing k) -> return k
_ | full_kind_sig -> return liftedTypeKind
| otherwise -> newMetaKindVar
; return (n, kind) }
kc_hs_tv (KindedTyVar n k)
= do { kind <- tcLHsKind k
; return (n, kind) }
tcScopedKindVars :: [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
-- kind skolem variable
tcScopedKindVars kv_ns thing_inside
= tcExtendTyVarEnv (map mkKindSigVar kv_ns) thing_inside
tcHsTyVarBndrs :: LHsTyVarBndrs Name
-> ([TyVar] -> TcM r)
-> TcM r
-- Bind the type variables to skolems, each with a meta-kind variable kind
tcHsTyVarBndrs (HsQTvs { hsq_kvs = kvs, hsq_tvs = hs_tvs }) thing_inside
= bindScopedKindVars kvs $ \ _ ->
= tcScopedKindVars kvs $
do { tvs <- mapM tcHsTyVarBndr hs_tvs
; traceTc "tcHsTyVarBndrs" (ppr hs_tvs $$ ppr tvs)
; tcExtendTyVarEnv tvs (thing_inside tvs) }
......@@ -857,13 +862,13 @@ tcHsTyVarBndr (L _ hs_tv)
; return (mkTcTyVar name kind (SkolemTv False)) } } }
------------------
kindGeneralize :: TyVarSet -> TcM [KindVar]
kindGeneralize tkvs
= do { gbl_tvs <- tcGetGlobalTyVars -- Already zonked
; tidy_env <- tcInitTidyEnv
; tkvs <- zonkTyVarsAndFV tkvs
kindGeneralize :: TyVarSet -> [Name] -> TcM [KindVar]
kindGeneralize tkvs _names_to_avoid
= do { gbl_tvs <- tcGetGlobalTyVars -- Already zonked
; tkvs <- zonkTyVarsAndFV tkvs
; let kvs_to_quantify = filter isKindVar (varSetElems (tkvs `minusVarSet` gbl_tvs))
-- Any type varaibles in tkvs will be in scope,
-- ToDo: remove the (filter isKindVar)
-- Any type variables in tkvs will be in scope,
-- and hence in gbl_tvs, so after removing gbl_tvs
-- we should only have kind variables left
--
......@@ -873,14 +878,16 @@ kindGeneralize tkvs
-- unification variable 'alpha', with no biding forall. We don't
-- want to kind-quantify it!
(_, tidy_kvs_to_quantify) = tidyTyVarBndrs tidy_env kvs_to_quantify
-- We do not get a later chance to tidy!
; traceTc "kindGeneralise" (vcat [ppr kvs_to_quantify])
; ASSERT2 (all isKindVar kvs_to_quantify, ppr kvs_to_quantify $$ ppr tkvs)
-- This assertion is obviosy true because of the filter isKindVar
-- This assertion is obviosly true because of the filter isKindVar
-- but we'll remove that when reorganising TH, and then the assertion
-- will mean something
zonkQuantifiedTyVars tidy_kvs_to_quantify }
-- If we tidied the kind variables, which should all be mutable,
-- this 'zonkQuantifiedTyVars' update the original TyVar to point to
-- the tided and skolemised one
zonkQuantifiedTyVars kvs_to_quantify }
\end{code}
Note [Kind generalisation]
......@@ -937,7 +944,7 @@ kcTyClTyVars :: Name -> LHsTyVarBndrs Name -> (TcKind -> TcM a) -> TcM a
-- Used for the type variables of a type or class decl,
-- when doing the initial kind-check.
kcTyClTyVars name (HsQTvs { hsq_kvs = kvs, hsq_tvs = hs_tvs }) thing_inside
= bindScopedKindVars kvs $ \ _ ->
= kcScopedKindVars kvs $
do { tc_kind <- kcLookupKind name
; let (arg_ks, res_k) = splitKindFunTysN (length hs_tvs) tc_kind
-- There should be enough arrows, because
......@@ -980,21 +987,24 @@ tcTyClTyVars :: Name -> LHsTyVarBndrs Name -- LHS of the type or class decl
--
-- No need to freshen the k's because they are just skolem
-- constants here, and we are at top level anyway.
tcTyClTyVars tycon tyvars thing_inside
= do { thing <- tcLookup tycon
tcTyClTyVars tycon (HsQTvs { hsq_kvs = kvs, hsq_tvs = hs_tvs }) thing_inside
= kcScopedKindVars kvs $
do { thing <- tcLookup tycon
; let { kind = case thing of
AThing kind -> kind
_ -> panic "tcTyClTyVars"
-- We only call tcTyClTyVars during typechecking in
-- TcTyClDecls, where the local env is extended with
-- the generalized_env (mapping Names to AThings).
; (kvs, body) = splitForAllTys kind
; (kinds, res) = splitKindFunTysN (length names) body
; names = hsLTyVarNames tyvars
; tvs = zipWith mkTyVar names kinds
; all_vs = kvs ++ tvs }
; tcExtendTyVarEnv all_vs (thing_inside all_vs res) }
; (kvs, body) = splitForAllTys kind
; (kinds, res) = splitKindFunTysN (length hs_tvs) body }
; tvs <- zipWithM tc_hs_tv hs_tvs kinds
; tcExtendTyVarEnv tvs (thing_inside (kvs ++ tvs) res) }
where
tc_hs_tv (L _ (UserTyVar n)) kind = return (mkTyVar n kind)
tc_hs_tv (L _ (KindedTyVar n hs_k)) kind = do { tc_kind <- tcLHsKind hs_k
; _ <- unifyKind kind tc_kind
; return (mkTyVar n kind) }
-----------------------------------
tcDataKindSig :: Kind -> TcM [TyVar]
......@@ -1384,19 +1394,19 @@ tc_kind_var_app name arg_kis
-- General case
tc_kind_var_app name arg_kis
= do { (_errs, mb_thing) <- tryTc (tcLookup name)
; case mb_thing of
Just (AGlobal (ATyCon tc))
= do { thing <- tcLookup name
; case thing of
AGlobal (ATyCon tc)
-> do { data_kinds <- xoptM Opt_DataKinds
; unless data_kinds $ addErr (dataKindsErr name)
; case isPromotableTyCon tc of
Just n | n == length arg_kis ->
return (mkTyConApp (buildPromotedTyCon tc) arg_kis)
Just _ -> err tc "is not fully applied"
Nothing -> err tc "is not promotable" }
Just _ -> tycon_err tc "is not fully applied"
Nothing -> tycon_err tc "is not promotable" }
-- A lexically scoped kind variable
Just (ATyVar _ kind_var)
ATyVar _ kind_var
| not (isKindVar kind_var)
-> failWithTc (ptext (sLit "Type variable") <+> quotes (ppr kind_var)
<+> ptext (sLit "used as a kind"))
......@@ -1408,19 +1418,32 @@ tc_kind_var_app name arg_kis
-> return (mkAppTys (mkTyVarTy kind_var) arg_kis)
-- It is in scope, but not what we expected
Just thing -> wrongThingErr "promoted type" thing name
-- It is not in scope, but it passed the renamer: staging error
Nothing
-> -- ASSERT2 ( isTyConName name, ppr name )
do { env <- getLclEnv
; traceTc "tc_kind_var_app" (ppr name $$ ppr (tcl_env env))
; failWithTc (ptext (sLit "Promoted kind") <+>
quotes (ppr name) <+>
ptext (sLit "used in a mutually recursive group")) } }
AThing _
| isTyVarName name
-> failWithTc (ptext (sLit "Type variable") <+> quotes (ppr name)
<+> ptext (sLit "used in a kind"))
| otherwise
-> failWithTc (hang (ptext (sLit "Type constructor") <+> quotes (ppr name)
<+> ptext (sLit "used in a kind"))
2 (ptext (sLit "inside its own recursive group")))
APromotionErr err -> promotionErr name err
_ -> wrongThingErr "promoted type" thing name
-- This really should not happen
}
where
err tc msg = failWithTc (quotes (ppr tc) <+> ptext (sLit "of kind")
<+> quotes (ppr (tyConKind tc)) <+> ptext (sLit msg))
tycon_err tc msg = failWithTc (quotes (ppr tc) <+> ptext (sLit "of kind")
<+> quotes (ppr (tyConKind tc)) <+> ptext (sLit msg))
promotionErr :: Name -> PromotionErr -> TcM a
promotionErr name err
= failWithTc (hang (pprPECategory err <+> quotes (ppr name) <+> ptext (sLit "cannot be used here"))
2 (parens reason))
where
reason = case err of
FamDataConPE -> ptext (sLit "it comes from a data family instance")
_ -> ptext (sLit "it is defined and used in the same recursive group")
\end{code}
%************************************************************************
......
......@@ -967,8 +967,8 @@ tcTyClsInstDecls :: ModDetails
HsValBinds Name) -- Supporting bindings for derived instances
tcTyClsInstDecls boot_details tycl_decls inst_decls deriv_decls
= tcExtendTcTyThingEnv [(con, AFamDataCon) | lid <- inst_decls
, con <- get_cons lid ] $
= tcExtendTcTyThingEnv [(con, APromotionErr FamDataConPE)
| lid <- inst_decls, con <- get_cons lid ] $
-- Note [AFamDataCon: not promoting data family constructors]
do { tcg_env <- tcTyAndClassDecls boot_details tycl_decls ;
; setGblEnv tcg_env $
......@@ -1890,7 +1890,9 @@ ppr_tydecls tycons
= vcat (map ppr_tycon (sortLe le_sig tycons))
where
le_sig tycon1 tycon2 = getOccName tycon1 <= getOccName tycon2
ppr_tycon tycon = ppr (tyThingToIfaceDecl (ATyCon tycon))
ppr_tycon tycon = vcat [ ppr (tyConName tycon) <+> dcolon <+> ppr (tyConKind tycon)
-- Temporarily print the kind signature too
, ppr (tyThingToIfaceDecl (ATyCon tycon)) ]
ppr_rules :: [CoreRule] -> SDoc
ppr_rules [] = empty
......
......@@ -38,7 +38,8 @@ module TcRnTypes(
WhereFrom(..), mkModDeps,
-- Typechecker types
TcTypeEnv, TcTyThing(..), pprTcTyThingCategory,
TcTypeEnv, TcTyThing(..), PromotionErr(..),
pprTcTyThingCategory, pprPECategory,
-- Template Haskell
ThStage(..), topStage, topAnnStage, topSpliceStage,
......@@ -580,10 +581,17 @@ data TcTyThing
-- Can be a mono-kind or a poly-kind; in TcTyClsDcls see
-- Note [Type checking recursive type and class declarations]
| AFamDataCon -- Data constructor for a data family
| APromotionErr PromotionErr
data PromotionErr
= TyConPE -- TyCon used in a kind before we are ready
-- data T :: T -> * where ...
| ClassPE -- Ditto Class
| FamDataConPE -- Data constructor for a data family
-- See Note [AFamDataCon: not promoting data family constructors] in TcRnDriver
| ARecDataCon -- Data constructor in a reuursive loop
| RecDataConPE -- Data constructor in a reuursive loop
-- See Note [ARecDataCon: recusion and promoting data constructors] in TcTyClsDecls
instance Outputable TcTyThing where -- Debugging only
......@@ -595,16 +603,26 @@ instance Outputable TcTyThing where -- Debugging only
<+> ppr (tct_level elt))
ppr (ATyVar tv _) = text "Type variable" <+> quotes (ppr tv)
ppr (AThing k) = text "AThing" <+> ppr k
ppr AFamDataCon = text "AFamDataCon"
ppr ARecDataCon = text "ARecDataCon"
ppr (APromotionErr err) = text "APromotionErr" <+> ppr err
instance Outputable PromotionErr where
ppr ClassPE = text "ClassPE"
ppr TyConPE = text "TyConPE"
ppr FamDataConPE = text "FamDataConPE"
ppr RecDataConPE = text "RecDataConPE"
pprTcTyThingCategory :: TcTyThing -> SDoc
pprTcTyThingCategory (AGlobal thing) = pprTyThingCategory thing
pprTcTyThingCategory (ATyVar {}) = ptext (sLit "Type variable")
pprTcTyThingCategory (ATcId {}) = ptext (sLit "Local identifier")
pprTcTyThingCategory (AThing {}) = ptext (sLit "Kinded thing")
pprTcTyThingCategory AFamDataCon = ptext (sLit "Family data con")
pprTcTyThingCategory ARecDataCon = ptext (sLit "Recursive data con")
pprTcTyThingCategory (AGlobal thing) = pprTyThingCategory thing
pprTcTyThingCategory (ATyVar {}) = ptext (sLit "Type variable")
pprTcTyThingCategory (ATcId {}) = ptext (sLit "Local identifier")
pprTcTyThingCategory (AThing {}) = ptext (sLit "Kinded thing")
pprTcTyThingCategory (APromotionErr pe) = pprPECategory pe
pprPECategory :: PromotionErr -> SDoc
pprPECategory ClassPE = ptext (sLit "Class")
pprPECategory TyConPE = ptext (sLit "Type constructor")
pprPECategory FamDataConPE = ptext (sLit "Data constructor")
pprPECategory RecDataConPE = ptext (sLit "Data constructor")
\end{code}
......
......@@ -166,7 +166,8 @@ tcRule (HsRule name act hs_bndrs lhs fv_lhs rhs fv_rhs)
; zonked_forall_tvs <- zonkTyVarsAndFV forall_tvs
; gbl_tvs <- tcGetGlobalTyVars -- Already zonked
; let tvs_to_quantify = varSetElems (zonked_forall_tvs `minusVarSet` gbl_tvs)
; qkvs <- kindGeneralize $ tyVarsOfTypes (map tyVarKind tvs_to_quantify)
; qkvs <- kindGeneralize (tyVarsOfTypes (map tyVarKind tvs_to_quantify))
(map getName tvs_to_quantify)
; qtvs <- zonkQuantifiedTyVars tvs_to_quantify
; let qtkvs = qkvs ++ qtvs
; traceTc "tcRule" (vcat [ doubleQuotes (ftext name)
......
......@@ -129,9 +129,9 @@ tcTyClGroup boot_details tyclds
-- Populate environment with knot-tied ATyCon for TyCons
-- NB: if the decls mention any ill-staged data cons
-- (see Note [ANothing] in typecheck/TcRnTypes.lhs) we
-- will have failed already in kcTyClGroup, so no worries here
; tcExtendRecEnv (zipRecTyClss tyclds rec_tyclss) $
-- (see Note [ARecDataCon: Recusion and promoting data constructors]
-- we will have failed already in kcTyClGroup, so no worries here
; tcExtendRecEnv (zipRecTyClss names_w_poly_kinds rec_tyclss) $
-- Also extend the local type envt with bindings giving
-- the (polymorphic) kind of each knot-tied TyCon or Class
......@@ -147,7 +147,7 @@ tcTyClGroup boot_details tyclds
-- expects well-formed TyCons
; tcExtendGlobalEnv tyclss $ do
{ traceTc "Starting validity check" (ppr tyclss)
; mapM_ (addLocM checkValidTyCl) tyclds
; mapM_ (addLocM checkValidTyCl) (flattenTyClDecls tyclds)
-- Step 4: Add the implicit things;
-- we want them in the environment because
......@@ -163,16 +163,15 @@ tcAddImplicits tyclss
implicit_things = concatMap implicitTyThings tyclss
rec_sel_binds = mkRecSelBinds tyclss
zipRecTyClss :: TyClGroup Name
zipRecTyClss :: [(Name, Kind)]
-> [TyThing] -- Knot-tied
-> [(Name,TyThing)]
-- Build a name-TyThing mapping for the things bound by decls
-- being careful not to look at the [TyThing]
-- The TyThings in the result list must have a visible ATyCon,
-- because typechecking types (in, say, tcTyClDecl) looks at this outer constructor
zipRecTyClss decls rec_things
= [ (name, ATyCon (get name))
| name <- tyClsBinders decls ]
zipRecTyClss kind_pairs rec_things
= [ (name, ATyCon (get name)) | (name, _kind) <- kind_pairs ]
where
rec_type_env :: TypeEnv
rec_type_env = mkTypeEnv rec_things
......@@ -181,13 +180,12 @@ zipRecTyClss decls rec_things
Just (ATyCon tc) -> tc
other -> pprPanic "zipRecTyClss" (ppr name <+> ppr other)
tyClsBinders :: TyClGroup Name -> [Name]
-- Just the tycon and class binders of a group (not the data constructors)
tyClsBinders decls
= concatMap get decls
where
get (L _ (ClassDecl { tcdLName = L _ n, tcdATs = ats })) = n : tyClsBinders ats
get (L _ d) = [tcdName d]
flattenTyClDecls :: [LTyClDecl Name] -> [LTyClDecl Name]
-- Lift out the associated type declaraitons to top level
flattenTyClDecls [] = []
flattenTyClDecls (ld@(L _ d) : lds)
| isClassDecl d = ld : tcdATs d ++ flattenTyClDecls lds
| otherwise = ld : flattenTyClDecls lds
\end{code}
......@@ -254,6 +252,7 @@ initial kind environment. (This is handled by `allDecls').
\begin{code}
kcTyClGroup :: TyClGroup Name -> TcM [(Name,Kind)]
-- Kind check this group, kind generalize, and return the resulting local env
-- This bindds the TyCons and Classes of the group, but not the DataCons
-- See Note [Kind checking for type and class decls]
kcTyClGroup decls
= do { mod <- getModule
......@@ -268,39 +267,49 @@ 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 TopLevel non_syn_decls
; traceTc "kcTyClGroup: initial kinds" (ppr initial_kinds)
; tcl_env <- tcExtendTcTyThingEnv initial_kinds $ do
do { -- Step 2: kind-check the synonyms, and extend envt
tcl_env <- kcSynDecls (calcSynCycles syn_decls)
-- Step 3: kind-check the synonyms
; setLclEnv tcl_env $
do { mapM_ kcLTyClDecl non_syn_decls
; getLclTypeEnv } }
-- Step 2: Set initial envt, kind-check the synonyms
; lcl_env <- tcExtendTcTyThingEnv initial_kinds $
kcSynDecls (calcSynCycles syn_decls)
-- Step 3: Set extended envt, kind-check the non-synonyms
; setLclEnv lcl_env $
mapM_ kcLTyClDecl non_syn_decls
-- Step 4: generalisation
-- Kind checking done for this group
-- Now we have to kind generalize the flexis
; res <- mapM (generalise tcl_env