diff options
Diffstat (limited to 'compiler')
| -rw-r--r-- | compiler/iface/MkIface.lhs | 129 | ||||
| -rw-r--r-- | compiler/typecheck/TcHsType.lhs | 143 | ||||
| -rw-r--r-- | compiler/typecheck/TcRnDriver.lhs | 8 | ||||
| -rw-r--r-- | compiler/typecheck/TcRnTypes.lhs | 40 | ||||
| -rw-r--r-- | compiler/typecheck/TcRules.lhs | 3 | ||||
| -rw-r--r-- | compiler/typecheck/TcTyClsDecls.lhs | 110 | ||||
| -rw-r--r-- | compiler/types/Kind.lhs | 9 |
7 files changed, 267 insertions, 175 deletions
diff --git a/compiler/iface/MkIface.lhs b/compiler/iface/MkIface.lhs index 7420dd8c32..d51fdd460a 100644 --- a/compiler/iface/MkIface.lhs +++ b/compiler/iface/MkIface.lhs @@ -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) diff --git a/compiler/typecheck/TcHsType.lhs b/compiler/typecheck/TcHsType.lhs index 7808c6b44c..1e30d7c328 100644 --- a/compiler/typecheck/TcHsType.lhs +++ b/compiler/typecheck/TcHsType.lhs @@ -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} %************************************************************************ diff --git a/compiler/typecheck/TcRnDriver.lhs b/compiler/typecheck/TcRnDriver.lhs index d4eb93113a..778a4b266f 100644 --- a/compiler/typecheck/TcRnDriver.lhs +++ b/compiler/typecheck/TcRnDriver.lhs @@ -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 diff --git a/compiler/typecheck/TcRnTypes.lhs b/compiler/typecheck/TcRnTypes.lhs index 1ed3d0d198..ac35c37df2 100644 --- a/compiler/typecheck/TcRnTypes.lhs +++ b/compiler/typecheck/TcRnTypes.lhs @@ -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} diff --git a/compiler/typecheck/TcRules.lhs b/compiler/typecheck/TcRules.lhs index 4f2dab07fe..f4f8c96964 100644 --- a/compiler/typecheck/TcRules.lhs +++ b/compiler/typecheck/TcRules.lhs @@ -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) diff --git a/compiler/typecheck/TcTyClsDecls.lhs b/compiler/typecheck/TcTyClsDecls.lhs index a22697d217..ab2880488d 100644 --- a/compiler/typecheck/TcTyClsDecls.lhs +++ b/compiler/typecheck/TcTyClsDecls.lhs @@ -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) (tyClsBinders decls) + ; res <- mapM (generalise (tcl_env lcl_env)) (flattenTyClDecls decls) ; traceTc "kcTyClGroup result" (ppr res) ; return res } where - generalise :: TcTypeEnv -> Name -> TcM (Name, Kind) + generalise :: TcTypeEnv -> LTyClDecl Name -> TcM (Name, Kind) -- For polymorphic things this is a no-op - generalise kind_env name - = do { traceTc "Generalise type of" (ppr name) + generalise kind_env (L _ decl) + = do { let name = tcdName decl + tvs = tcdTyVars decl ; let kc_kind = case lookupNameEnv kind_env name of Just (AThing k) -> k _ -> pprPanic "kcTyClGroup" (ppr name $$ ppr kind_env) - ; kvs <- kindGeneralize (tyVarsOfType kc_kind) - ; kc_kind' <- zonkTcKind kc_kind + ; kvs <- kindGeneralize (tyVarsOfType kc_kind) (hsLTyVarNames tvs) + ; kc_kind' <- zonkTcKind kc_kind -- Make sure kc_kind' has the final, + -- skolemised kind variables + ; traceTc "Generalise kind" (vcat [ ppr name, ppr kc_kind, ppr kvs, ppr kc_kind' ]) ; return (name, mkForAllTys kvs kc_kind') } getInitialKinds :: TopLevelFlag -> [LTyClDecl Name] -> TcM [(Name, TcTyThing)] -getInitialKinds top_lvl = concatMapM (addLocM (getInitialKind top_lvl)) +getInitialKinds top_lvl decls + = tcExtendTcTyThingEnv [ (tcdName d, APromotionErr (mk_promotion_err d)) + | L _ d <- flattenTyClDecls decls] $ + concatMapM (addLocM (getInitialKind top_lvl)) decls + where + mk_promotion_err (ClassDecl {}) = ClassPE + mk_promotion_err _ = TyConPE getInitialKind :: TopLevelFlag -> TyClDecl Name -> TcM [(Name, TcTyThing)] -- Allocate a fresh kind variable for each TyCon and Class @@ -311,8 +320,8 @@ getInitialKind :: TopLevelFlag -> TyClDecl Name -> TcM [(Name, TcTyThing)] -- Example: data T a b = ... -- return (T, kv1 -> kv2 -> kv3) -- --- ALSO for each datacon, return (dc, ANothing) --- See Note [ANothing] in TcRnTypes +-- ALSO for each datacon, return (dc, ARecDataCon) +-- Note [ARecDataCon: Recusion and promoting data constructors] -- -- No family instances are passed to getInitialKinds @@ -347,14 +356,14 @@ getInitialKind top_lvl decl@(TyDecl { tcdLName = L _ name, tcdTyVars = ktvs, tcd ; 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), ARecDataCon) | L _ con <- cons ] + inner_prs = [(unLoc (con_name con), APromotionErr RecDataConPE) | L _ con <- cons ] -- See Note [ARecDataCon: Recusion and promoting data constructors] ; return (main_pr : inner_prs) } | TyData { td_cons = cons } <- defn = kcHsTyVarBndrs False ktvs $ \ arg_kinds -> do { let main_pr = (name, AThing (mkArrowKinds arg_kinds liftedTypeKind)) - inner_prs = [(unLoc (con_name con), ARecDataCon) | L _ con <- cons ] + inner_prs = [(unLoc (con_name con), APromotionErr RecDataConPE) | L _ con <- cons ] -- See Note [ARecDataCon: Recusion and promoting data constructors] ; return (main_pr : inner_prs) } @@ -622,13 +631,19 @@ tcTyDefn calc_isrec tc_name tvs kind final_tvs = tvs ++ extra_tvs ; stupid_theta <- tcHsContext ctxt ; kind_signatures <- xoptM Opt_KindSignatures - ; existential_ok <- xoptM Opt_ExistentialQuantification - ; gadt_ok <- xoptM Opt_GADTs + ; existential_ok <- xoptM Opt_ExistentialQuantification + ; gadt_ok <- xoptM Opt_GADTs ; is_boot <- tcIsHsBoot -- Are we compiling an hs-boot file? ; let ex_ok = existential_ok || gadt_ok -- Data cons can have existential context -- Check that we don't use kind signatures without Glasgow extensions - ; checkTc (kind_signatures || isNothing mb_ksig) (badSigTyDecl tc_name) + ; + ; case mb_ksig of + Nothing -> return () + Just hs_k -> do { checkTc (kind_signatures) (badSigTyDecl tc_name) + ; tc_kind <- tcLHsKind hs_k + ; _ <- unifyKind kind tc_kind + ; return () } ; dataDeclChecks tc_name new_or_data stupid_theta cons @@ -717,7 +732,6 @@ tcSynFamInstDecl :: TyCon -> FamInstDecl Name -> TcM ([TyVar], [Type], Type) tcSynFamInstDecl fam_tc (FamInstDecl { fid_pats = pats, fid_defn = defn@(TySynonym { td_synRhs = hs_ty }) }) = do { checkTc (isSynTyCon fam_tc) (wrongKindOfFamily fam_tc) - ; tcFamTyPats fam_tc pats (kcTyDefn defn) $ \tvs' pats' res_kind -> do { rhs_ty <- tcCheckLHsType hs_ty res_kind ; rhs_ty <- zonkTcTypeToType emptyZonkEnv rhs_ty @@ -965,7 +979,7 @@ tcConDecl new_or_data existential_ok rep_tycon res_tmpl -- Data types -- Generalise the kind variables (returning quantifed TcKindVars) -- and quanify the type variables (substiting their kinds) - ; kvs <- kindGeneralize (tyVarsOfType pretend_con_ty) + ; kvs <- kindGeneralize (tyVarsOfType pretend_con_ty) (map getName tvs) ; tvs <- zonkQuantifiedTyVars tvs -- Zonk to Types @@ -1069,7 +1083,7 @@ rejigConRes (tmpl_tvs, res_tmpl) dc_tvs (ResTyGADT res_ty) -- /Lazily/ figure out the univ_tvs etc -- Each univ_tv is either a dc_tv or a tmpl_tv - (univ_tvs, eq_spec) = foldr choose ([], []) tidy_tmpl_tvs + (univ_tvs, eq_spec) = foldr choose ([], []) tmpl_tvs choose tmpl (univs, eqs) | Just ty <- lookupTyVar subst tmpl = case tcGetTyVar_maybe ty of @@ -1081,17 +1095,6 @@ rejigConRes (tmpl_tvs, res_tmpl) dc_tvs (ResTyGADT res_ty) | otherwise = pprPanic "tcResultType" (ppr res_ty) ex_tvs = dc_tvs `minusList` univ_tvs - -- NB: tmpl_tvs and dc_tvs are distinct, but - -- we want them to be *visibly* distinct, both for - -- interface files and general confusion. So rename - -- the tc_tvs, since they are not used yet (no - -- consequential renaming needed) - (_, tidy_tmpl_tvs) = mapAccumL tidy_one init_occ_env tmpl_tvs - init_occ_env = initTidyOccEnv (map getOccName dc_tvs) - tidy_one env tv = (env', setTyVarName tv (tidyNameOcc name occ')) - where - name = tyVarName tv - (env', occ') = tidyOccName env (getOccName name) {- Note [Substitution in template variables kinds] @@ -1258,9 +1261,6 @@ checkValidTyCl decl ATyCon tc -> do traceTc " of kind" (ppr (tyConKind tc)) checkValidTyCon tc - case decl of - ClassDecl { tcdATs = ats } -> mapM_ (addLocM checkValidTyCl) ats - _ -> return () AnId _ -> return () -- Generic default methods are checked -- with their parent class _ -> panic "checkValidTyCl" diff --git a/compiler/types/Kind.lhs b/compiler/types/Kind.lhs index 5f567eba36..7318891d87 100644 --- a/compiler/types/Kind.lhs +++ b/compiler/types/Kind.lhs @@ -34,7 +34,8 @@ module Kind ( -- ** Predicates on Kinds isLiftedTypeKind, isUnliftedTypeKind, isOpenTypeKind, - isConstraintKind, isConstraintOrLiftedKind, isKind, isKindVar, + isConstraintKind, isConstraintOrLiftedKind, returnsConstraintKind, + isKind, isKindVar, isSuperKind, isSuperKindTyCon, isLiftedTypeKindCon, isConstraintKindCon, isAnyKind, isAnyKindCon, @@ -135,6 +136,12 @@ isConstraintOrLiftedKind (TyConApp tc _) = isConstraintKindCon tc || isLiftedTypeKindCon tc isConstraintOrLiftedKind _ = False +returnsConstraintKind :: Kind -> Bool +returnsConstraintKind (ForAllTy _ k) = returnsConstraintKind k +returnsConstraintKind (FunTy _ k) = returnsConstraintKind k +returnsConstraintKind (TyConApp tc _) = isConstraintKindCon tc +returnsConstraintKind _ = False + -------------------------------------------- -- Kinding for arrow (->) -- Says when a kind is acceptable on lhs or rhs of an arrow |