diff options
author | Simon Peyton Jones <simonpj@microsoft.com> | 2017-12-07 14:31:53 +0000 |
---|---|---|
committer | Simon Peyton Jones <simonpj@microsoft.com> | 2017-12-08 15:42:55 +0000 |
commit | de2044098ae96245aa741fe1b47a06a996a1c725 (patch) | |
tree | bab680b1439b3241a532b93fabe6c6246ea8913a /compiler | |
parent | e4a1f032da39d8ee58498962cdc9bf5fed7b376e (diff) | |
download | haskell-de2044098ae96245aa741fe1b47a06a996a1c725.tar.gz |
Refactor kcHsTyVarBndrs
This refactoring
* Renames kcHsTyVarBndrs to kcLHsQTyVars,
which is more truthful. It is only used in getInitialKind.
* Pulls out bind_telescope from that function, and calls it
kcLHsTyVarBndrs, again to reflect its argument
* Uses the new kcLHsTyVarBndrs in kcConDecl, where the old
function was wild overkill.
There should not be any change in behaviour
Diffstat (limited to 'compiler')
-rw-r--r-- | compiler/typecheck/TcHsType.hs | 146 | ||||
-rw-r--r-- | compiler/typecheck/TcTyClsDecls.hs | 8 |
2 files changed, 83 insertions, 71 deletions
diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs index cc826b9401..7807ab1b9c 100644 --- a/compiler/typecheck/TcHsType.hs +++ b/compiler/typecheck/TcHsType.hs @@ -27,8 +27,8 @@ module TcHsType ( -- Kind-checking types -- No kind generalisation, no checkValidType + kcLHsQTyVars, kcLHsTyVarBndrs, tcWildCardBinders, - kcHsTyVarBndrs, tcHsLiftedType, tcHsOpenType, tcHsLiftedTypeNC, tcHsOpenTypeNC, tcLHsType, tcLHsTypeUnsaturated, tcCheckLHsType, @@ -1315,7 +1315,7 @@ Note [Dependent LHsQTyVars] ~~~~~~~~~~~~~~~~~~~~~~~~~~~ We track (in the renamer) which explicitly bound variables in a LHsQTyVars are manifestly dependent; only precisely these variables -may be used within the LHsQTyVars. We must do this so that kcHsTyVarBndrs +may be used within the LHsQTyVars. We must do this so that kcLHsQTyVars can produce the right TyConBinders, and tell Anon vs. Required. Example data T k1 (a:k1) (b:k2) c @@ -1337,14 +1337,14 @@ and See Note [TyVarBndrs, TyVarBinders, TyConBinders, and visibility] in TyCoRep. -kcHsTyVarBndrs uses the hsq_dependent field to decide whether +kcLHsQTyVars uses the hsq_dependent field to decide whether k1, a, b, c should be Required or Anon. Earlier, thought it would work simply to do a free-variable check -during kcHsTyVarBndrs, but this is bogus, because there may be +during kcLHsQTyVars, but this is bogus, because there may be unsolved equalities about. And we don't want to eagerly solve the equalities, because we may get further information after -kcHsTyVarBndrs is called. (Recall that kcHsTyVarBndrs is usually +kcLHsQTyVars is called. (Recall that kcLHsQTyVars is usually called from getInitialKind. The only other case is in kcConDecl.) This is what implements the rule that all variables intended to be dependent must be manifestly so. @@ -1381,15 +1381,15 @@ tcWildCardBindersX new_wc wc_names thing_inside -- HsDecls. -- -- This function does not do telescope checking. -kcHsTyVarBndrs :: Name -- ^ of the thing being checked - -> TyConFlavour -- ^ What sort of 'TyCon' is being checked - -> Bool -- ^ True <=> the decl being checked has a CUSK - -> Bool -- ^ True <=> all the hsq_implicit are *kind* vars - -- (will give these kind * if -XNoTypeInType) - -> LHsQTyVars GhcRn - -> TcM (Kind, r) -- ^ The result kind, possibly with other info - -> TcM (TcTyCon, r) -- ^ A suitably-kinded TcTyCon -kcHsTyVarBndrs name flav cusk all_kind_vars +kcLHsQTyVars :: Name -- ^ of the thing being checked + -> TyConFlavour -- ^ What sort of 'TyCon' is being checked + -> Bool -- ^ True <=> the decl being checked has a CUSK + -> Bool -- ^ True <=> all the hsq_implicit are *kind* vars + -- (will give these kind * if -XNoTypeInType) + -> LHsQTyVars GhcRn + -> TcM (Kind, r) -- ^ The result kind, possibly with other info + -> TcM (TcTyCon, r) -- ^ A suitably-kinded TcTyCon +kcLHsQTyVars name flav cusk all_kind_vars (HsQTvs { hsq_implicit = kv_ns, hsq_explicit = hs_tvs , hsq_dependent = dep_names }) thing_inside | cusk @@ -1397,15 +1397,16 @@ kcHsTyVarBndrs name flav cusk all_kind_vars ; lvl <- getTcLevel ; let scoped_kvs = zipWith (mk_skolem_tv lvl) kv_ns kv_kinds ; tcExtendTyVarEnv2 (kv_ns `zip` scoped_kvs) $ - do { (tc_binders, res_kind, stuff) <- solveEqualities $ - bind_telescope hs_tvs thing_inside + do { (tc_tvs, (res_kind, stuff)) + <- solveEqualities $ + kcLHsTyVarBndrs open_fam hs_tvs thing_inside -- Now, because we're in a CUSK, quantify over the mentioned -- kind vars, in dependency order. - ; tc_binders <- mapM zonkTcTyVarBinder tc_binders + ; tc_tvs <- mapM zonkTcTyVarToTyVar tc_tvs ; res_kind <- zonkTcType res_kind - ; let tc_tvs = binderVars tc_binders - qkvs = tyCoVarsOfTypeWellScoped (mkTyConKind tc_binders res_kind) + ; let tc_binders = zipWith mk_tc_binder hs_tvs tc_tvs + qkvs = tyCoVarsOfTypeWellScoped (mkTyConKind tc_binders res_kind) -- the visibility of tvs doesn't matter here; we just -- want the free variables not to include the tvs @@ -1435,9 +1436,9 @@ kcHsTyVarBndrs name flav cusk all_kind_vars -- re-adding tvs to the env't doesn't cause -- harm - ; traceTc "kcHsTyVarBndrs: cusk" $ + ; traceTc "kcLHsQTyVars: cusk" $ vcat [ ppr name, ppr kv_ns, ppr hs_tvs, ppr dep_names - , ppr tc_binders, ppr (mkTyConKind tc_binders res_kind) + , ppr tc_tvs, ppr (mkTyConKind final_binders res_kind) , ppr qkvs, ppr meta_tvs, ppr good_tvs, ppr final_binders ] ; return (tycon, stuff) }} @@ -1446,21 +1447,31 @@ kcHsTyVarBndrs name flav cusk all_kind_vars = do { kv_kinds <- mk_kv_kinds ; scoped_kvs <- zipWithM newSigTyVar kv_ns kv_kinds -- the names must line up in splitTelescopeTvs - ; (binders, res_kind, stuff) + ; (tc_tvs, (res_kind, stuff)) <- tcExtendTyVarEnv2 (kv_ns `zip` scoped_kvs) $ - bind_telescope hs_tvs thing_inside + kcLHsTyVarBndrs open_fam hs_tvs thing_inside ; let -- NB: Don't add scoped_kvs to tyConTyVars, because they -- must remain lined up with the binders - tycon = mkTcTyCon name binders res_kind - (scoped_kvs ++ binderVars binders) flav + tc_binders = zipWith mk_tc_binder hs_tvs tc_tvs + tycon = mkTcTyCon name tc_binders res_kind + (scoped_kvs ++ binderVars tc_binders) flav - ; traceTc "kcHsTyVarBndrs: not-cusk" $ + ; traceTc "kcLHsQTyVars: not-cusk" $ vcat [ ppr name, ppr kv_ns, ppr hs_tvs, ppr dep_names - , ppr binders, ppr (mkTyConKind binders res_kind) ] + , ppr tc_tvs, ppr (mkTyConKind tc_binders res_kind) ] ; return (tycon, stuff) } where open_fam = tcFlavourIsOpen flav + mk_tc_binder :: LHsTyVarBndr GhcRn -> TyVar -> TyConBinder + -- See Note [Dependent LHsQTyVars] + mk_tc_binder hs_tv tv + | hsLTyVarName hs_tv `elemNameSet` dep_names + = mkNamedTyConBinder Required tv + | otherwise + = mkAnonTyConBinder tv + + -- if -XNoTypeInType and we know all the implicits are kind vars, -- just give the kind *. This prevents test -- dependent/should_fail/KindLevelsB from compiling, as it should @@ -1470,28 +1481,44 @@ kcHsTyVarBndrs name flav cusk all_kind_vars then return (map (const liftedTypeKind) kv_ns) else mapM (const newMetaKindVar) kv_ns } - -- there may be dependency between the explicit "ty" vars. So, we have - -- to handle them one at a time. - bind_telescope :: [LHsTyVarBndr GhcRn] - -> TcM (Kind, r) - -> TcM ([TyConBinder], TcKind, r) - bind_telescope [] thing - = do { (res_kind, stuff) <- thing - ; return ([], res_kind, stuff) } - bind_telescope (L _ hs_tv : hs_tvs) thing - = do { tv_pair@(tv, _) <- kc_hs_tv hs_tv + report_non_cusk_tvs all_tvs + = do { all_tvs <- mapM zonkTyCoVarKind all_tvs + ; let (_, tidy_tvs) = tidyOpenTyCoVars emptyTidyEnv all_tvs + (meta_tvs, other_tvs) = partition isMetaTyVar tidy_tvs + + ; addErr $ + vcat [ text "You have written a *complete user-suppled kind signature*," + , hang (text "but the following variable" <> plural meta_tvs <+> + isOrAre meta_tvs <+> text "undetermined:") + 2 (vcat (map pp_tv meta_tvs)) + , text "Perhaps add a kind signature." + , hang (text "Inferred kinds of user-written variables:") + 2 (vcat (map pp_tv other_tvs)) ] } + where + pp_tv tv = ppr tv <+> dcolon <+> ppr (tyVarKind tv) + + +kcLHsTyVarBndrs :: Bool -- True <=> Default un-annotated tyvar + -- binders to kind * + -> [LHsTyVarBndr GhcRn] + -> TcM r + -> TcM ([TyVar], r) +-- There may be dependency between the explicit "ty" vars. +-- So, we have to handle them one at a time. +kcLHsTyVarBndrs _ [] thing + = do { stuff <- thing; return ([], stuff) } + +kcLHsTyVarBndrs open_fam (L _ hs_tv : hs_tvs) thing + = do { tv_pair@(tv, _) <- kc_hs_tv hs_tv -- NB: Bring all tvs into scope, even non-dependent ones, -- as they're needed in type synonyms, data constructors, etc. - ; (binders, res_kind, stuff) <- bind_unless_scoped tv_pair $ - bind_telescope hs_tvs $ - thing - -- See Note [Dependent LHsQTyVars] - ; let new_binder | hsTyVarName hs_tv `elemNameSet` dep_names - = mkNamedTyConBinder Required tv - | otherwise - = mkAnonTyConBinder tv - ; return ( new_binder : binders - , res_kind, stuff ) } + + ; (tvs, stuff) <- bind_unless_scoped tv_pair $ + kcLHsTyVarBndrs open_fam hs_tvs $ + thing + + ; return ( tv : tvs, stuff ) } + where -- | Bind the tyvar in the env't unless the bool is True bind_unless_scoped :: (TcTyVar, Bool) -> TcM a -> TcM a @@ -1501,10 +1528,11 @@ kcHsTyVarBndrs name flav cusk all_kind_vars kc_hs_tv :: HsTyVarBndr GhcRn -> TcM (TcTyVar, Bool) kc_hs_tv (UserTyVar lname@(L _ name)) - = do { tv_pair@(tv, scoped) <- tcHsTyVarName Nothing name + = do { tv_pair@(tv, in_scope) <- tcHsTyVarName Nothing name - -- Open type/data families default their variables to kind *. - ; when (open_fam && not scoped) $ -- (don't default class tyvars) + -- Open type/data families default their variables to kind *. + -- But don't default in-scope class tyvars, of course + ; when (open_fam && not in_scope) $ discardResult $ unifyKind (Just (HsTyVar NotPromoted lname)) liftedTypeKind (tyVarKind tv) @@ -1514,22 +1542,6 @@ kcHsTyVarBndrs name flav cusk all_kind_vars = do { kind <- tcLHsKindSig lhs_kind ; tcHsTyVarName (Just kind) name } - report_non_cusk_tvs all_tvs - = do { all_tvs <- mapM zonkTyCoVarKind all_tvs - ; let (_, tidy_tvs) = tidyOpenTyCoVars emptyTidyEnv all_tvs - (meta_tvs, other_tvs) = partition isMetaTyVar tidy_tvs - - ; addErr $ - vcat [ text "You have written a *complete user-suppled kind signature*," - , hang (text "but the following variable" <> plural meta_tvs <+> - isOrAre meta_tvs <+> text "undetermined:") - 2 (vcat (map pp_tv meta_tvs)) - , text "Perhaps add a kind signature." - , hang (text "Inferred kinds of user-written variables:") - 2 (vcat (map pp_tv other_tvs)) ] } - where - pp_tv tv = ppr tv <+> dcolon <+> ppr (tyVarKind tv) - tcImplicitTKBndrs :: [Name] -> TcM (a, TyVarSet) -- vars are bound somewhere in the scope @@ -1769,7 +1781,7 @@ we check to make sure that k has been unified with some other variable it must be a free-floating kind var. Error. CUSK: When we determine the tycon's final, never-to-be-changed kind -in kcHsTyVarBndrs, we check to make sure all implicitly-bound kind +in kcLHsQTyVars, we check to make sure all implicitly-bound kind vars are indeed mentioned in a kind somewhere. If not, error. We also perform free-floating kind var analysis for type family instances diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs index e3b8b4d7bd..5c5cf2f651 100644 --- a/compiler/typecheck/TcTyClsDecls.hs +++ b/compiler/typecheck/TcTyClsDecls.hs @@ -484,7 +484,7 @@ getInitialKind :: TyClDecl GhcRn getInitialKind decl@(ClassDecl { tcdLName = L _ name, tcdTyVars = ktvs, tcdATs = ats }) = do { let cusk = hsDeclHasCusk decl ; (tycon, inner_prs) <- - kcHsTyVarBndrs name ClassFlavour cusk True ktvs $ + kcLHsQTyVars name ClassFlavour cusk True ktvs $ do { inner_prs <- getFamDeclInitialKinds (Just cusk) ats ; return (constraintKind, inner_prs) } ; return (extendEnvWithTcTyCon inner_prs tycon) } @@ -494,7 +494,7 @@ getInitialKind decl@(DataDecl { tcdLName = L _ name , tcdDataDefn = HsDataDefn { dd_kindSig = m_sig , dd_ND = new_or_data } }) = do { (tycon, _) <- - kcHsTyVarBndrs name flav (hsDeclHasCusk decl) True ktvs $ + kcLHsQTyVars name flav (hsDeclHasCusk decl) True ktvs $ do { res_k <- case m_sig of Just ksig -> tcLHsKindSig ksig Nothing -> return liftedTypeKind @@ -511,7 +511,7 @@ getInitialKind (FamDecl { tcdFam = decl }) getInitialKind decl@(SynDecl { tcdLName = L _ name , tcdTyVars = ktvs , tcdRhs = rhs }) - = do { (tycon, _) <- kcHsTyVarBndrs name TypeSynonymFlavour + = do { (tycon, _) <- kcLHsQTyVars name TypeSynonymFlavour (hsDeclHasCusk decl) True ktvs $ do { res_k <- case kind_annotation rhs of @@ -542,7 +542,7 @@ getFamDeclInitialKind mb_cusk decl@(FamilyDecl { fdLName = L _ name , fdResultSig = L _ resultSig , fdInfo = info }) = do { (tycon, _) <- - kcHsTyVarBndrs name flav cusk True ktvs $ + kcLHsQTyVars name flav cusk True ktvs $ do { res_k <- case resultSig of KindSig ki -> tcLHsKindSig ki TyVarSig (L _ (KindedTyVar _ ki)) -> tcLHsKindSig ki |