diff options
| author | Simon Peyton Jones <simonpj@microsoft.com> | 2018-10-26 10:57:51 +0100 |
|---|---|---|
| committer | Simon Peyton Jones <simonpj@microsoft.com> | 2018-10-26 10:57:51 +0100 |
| commit | 339b814bb45d9ccb658c7ea9fb038a73f790ddd9 (patch) | |
| tree | b51ab1e58c23b151c6c53ec3acf9e98fe86e3ff5 | |
| parent | e6bf96c9700aacbd75169dbf2cc14c9216c0133f (diff) | |
| download | haskell-wip/T15791.tar.gz | |
Work in progress on Trac #15791wip/T15791
24 files changed, 148 insertions, 114 deletions
diff --git a/compiler/typecheck/ClsInst.hs b/compiler/typecheck/ClsInst.hs index 03adfdebbb..d199cca8c2 100644 --- a/compiler/typecheck/ClsInst.hs +++ b/compiler/typecheck/ClsInst.hs @@ -435,7 +435,7 @@ doTyApp :: Class -> Type -> Type -> KindOrType -> TcM ClsInstResult -- (Typeable f, Typeable Int, Typeable Char) --> (after some simp. steps) -- Typeable f doTyApp clas ty f tk - | isForAllTy (typeKind f) + | isForAllTy (tcTypeKind f) = return NoInstance -- We can't solve until we know the ctr. | otherwise = return $ OneInst { cir_new_theta = map (mk_typeable_pred clas) [f, tk] @@ -448,7 +448,7 @@ doTyApp clas ty f tk -- Emit a `Typeable` constraint for the given type. mk_typeable_pred :: Class -> Type -> PredType -mk_typeable_pred clas ty = mkClassPred clas [ typeKind ty, ty ] +mk_typeable_pred clas ty = mkClassPred clas [ tcTypeKind ty, ty ] -- Typeable is implied by KnownNat/KnownSymbol. In the case of a type literal -- we generate a sub-goal for the appropriate class. diff --git a/compiler/typecheck/FamInst.hs b/compiler/typecheck/FamInst.hs index 8f1f7ba5f6..cc8466cbbf 100644 --- a/compiler/typecheck/FamInst.hs +++ b/compiler/typecheck/FamInst.hs @@ -178,8 +178,8 @@ newFamInst flavor axiom@(CoAxiom { co_ax_tc = fam_tc }) , fi_rhs = rhs' , fi_axiom = axiom }) } where - lhs_kind = typeKind (mkTyConApp fam_tc lhs) - rhs_kind = typeKind rhs + lhs_kind = tcTypeKind (mkTyConApp fam_tc lhs) + rhs_kind = tcTypeKind rhs tcv_set = mkVarSet (tvs ++ cvs) pp_ax = pprCoAxiom axiom CoAxBranch { cab_tvs = tvs diff --git a/compiler/typecheck/Inst.hs b/compiler/typecheck/Inst.hs index 4f380d37a8..0fe41572bd 100644 --- a/compiler/typecheck/Inst.hs +++ b/compiler/typecheck/Inst.hs @@ -305,7 +305,7 @@ instTyVarsWith orig tvs tys ; go (extendTCvSubst subst tv (ty `mkCastTy` co)) tvs tys } where tv_kind = substTy subst (tyVarKind tv) - ty_kind = typeKind ty + ty_kind = tcTypeKind ty go _ _ _ = pprPanic "instTysWith" (ppr tvs $$ ppr tys) @@ -570,15 +570,15 @@ mkHEqBoxTy :: TcCoercion -> Type -> Type -> TcM Type mkHEqBoxTy co ty1 ty2 = return $ mkTyConApp (promoteDataCon heqDataCon) [k1, k2, ty1, ty2, mkCoercionTy co] - where k1 = typeKind ty1 - k2 = typeKind ty2 + where k1 = tcTypeKind ty1 + k2 = tcTypeKind ty2 -- | This takes @a ~# b@ and returns @a ~ b@. mkEqBoxTy :: TcCoercion -> Type -> Type -> TcM Type mkEqBoxTy co ty1 ty2 = return $ mkTyConApp (promoteDataCon eqDataCon) [k, ty1, ty2, mkCoercionTy co] - where k = typeKind ty1 + where k = tcTypeKind ty1 {- ************************************************************************ diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs index b576fc34b8..f3aa348db7 100644 --- a/compiler/typecheck/TcCanonical.hs +++ b/compiler/typecheck/TcCanonical.hs @@ -1319,8 +1319,8 @@ can_eq_app ev s1 t1 s2 t2 ; canEqNC evar_s NomEq s1 s2 } where - s1k = typeKind s1 - s2k = typeKind s2 + s1k = tcTypeKind s1 + s2k = tcTypeKind s2 k1 `mismatches` k2 = isForAllTy k1 && not (isForAllTy k2) @@ -1790,9 +1790,9 @@ canCFunEqCan ev fn tys fsk vcat [ text "Kind co:" <+> ppr kind_co , text "RHS:" <+> ppr fsk <+> dcolon <+> ppr (tyVarKind fsk) , text "LHS:" <+> hang (ppr (mkTyConApp fn tys)) - 2 (dcolon <+> ppr (typeKind (mkTyConApp fn tys))) + 2 (dcolon <+> ppr (tcTypeKind (mkTyConApp fn tys))) , text "New LHS" <+> hang (ppr new_lhs) - 2 (dcolon <+> ppr (typeKind new_lhs)) ] + 2 (dcolon <+> ppr (tcTypeKind new_lhs)) ] ; (ev', new_co, new_fsk) <- newFlattenSkolem flav (ctEvLoc ev) fn tys' ; let xi = mkTyVarTy new_fsk `mkCastTy` kind_co @@ -1882,7 +1882,7 @@ canEqTyVar ev eq_rel swapped tv1 ps_ty1 xi2 ps_xi2 xi1 = mkTyVarTy tv1 k1 = tyVarKind tv1 - k2 = typeKind xi2 + k2 = tcTypeKind xi2 loc = ctEvLoc ev flav = ctEvFlavour ev @@ -1936,7 +1936,7 @@ canEqTyVarHetero ev eq_rel tv1 co1 ki1 ps_tv1 xi2 ki2 ps_xi2 loc = ctev_loc ev role = eqRelRole eq_rel --- guaranteed that typeKind lhs == typeKind rhs +-- guaranteed that tcTypeKind lhs == tcTypeKind rhs canEqTyVarHomo :: CtEvidence -> EqRel -> SwapFlag -> TcTyVar -- lhs: tv1 @@ -2288,7 +2288,7 @@ rewriteEqEvidence :: CtEvidence -- Old evidence :: olhs ~ orhs (not swap -- or orhs ~ olhs (swapped) -> SwapFlag -> TcType -> TcType -- New predicate nlhs ~ nrhs - -- Should be zonked, because we use typeKind on nlhs/nrhs + -- Should be zonked, because we use tcTypeKind on nlhs/nrhs -> TcCoercion -- lhs_co, of type :: nlhs ~ olhs -> TcCoercion -- rhs_co, of type :: nrhs ~ orhs -> TcS CtEvidence -- Of type nlhs ~ nrhs @@ -2364,7 +2364,7 @@ unifyWanted :: CtLoc -> Role -- See Note [unifyWanted and unifyDerived] -- The returned coercion's role matches the input parameter unifyWanted loc Phantom ty1 ty2 - = do { kind_co <- unifyWanted loc Nominal (typeKind ty1) (typeKind ty2) + = do { kind_co <- unifyWanted loc Nominal (tcTypeKind ty1) (tcTypeKind ty2) ; return (mkPhantomCo kind_co ty1 ty2) } unifyWanted loc role orig_ty1 orig_ty2 diff --git a/compiler/typecheck/TcDeriv.hs b/compiler/typecheck/TcDeriv.hs index 6f749fc60f..33a804e51f 100644 --- a/compiler/typecheck/TcDeriv.hs +++ b/compiler/typecheck/TcDeriv.hs @@ -629,8 +629,8 @@ deriveStandalone (L loc (DerivDecl _ deriv_ty mbl_deriv_strat overlap_mode)) -- Perform an additional unification with the kind of the `via` -- type and the result of the previous kind unification. Just (ViaStrategy via_ty) -> do - let via_kind = typeKind via_ty - inst_ty_kind = typeKind inst_ty' + let via_kind = tcTypeKind via_ty + inst_ty_kind = tcTypeKind inst_ty' mb_match = tcUnifyTy inst_ty_kind via_kind checkTc (isJust mb_match) @@ -789,7 +789,7 @@ deriveTyData tvs tc tc_args mb_deriv_strat deriv_pred n_args_to_keep = tyConArity tc - n_args_to_drop (tc_args_to_keep, args_to_drop) = splitAt n_args_to_keep tc_args - inst_ty_kind = typeKind (mkTyConApp tc tc_args_to_keep) + inst_ty_kind = tcTypeKind (mkTyConApp tc tc_args_to_keep) -- Match up the kinds, and apply the resulting kind substitution -- to the types. See Note [Unify kinds in deriving] @@ -829,9 +829,9 @@ deriveTyData tvs tc tc_args mb_deriv_strat deriv_pred -- type and the result of the previous kind unification. Just (ViaStrategy via_ty) -> do let final_via_ty = via_ty - final_via_kind = typeKind final_via_ty + final_via_kind = tcTypeKind final_via_ty final_inst_ty_kind - = typeKind (mkTyConApp tc final_tc_args') + = tcTypeKind (mkTyConApp tc final_tc_args') via_match = tcUnifyTy final_inst_ty_kind final_via_kind checkTc (isJust via_match) diff --git a/compiler/typecheck/TcDerivInfer.hs b/compiler/typecheck/TcDerivInfer.hs index 3f4192fb42..0398b847ab 100644 --- a/compiler/typecheck/TcDerivInfer.hs +++ b/compiler/typecheck/TcDerivInfer.hs @@ -157,7 +157,7 @@ inferConstraintsDataConArgs inst_ty inst_tys is_generic = main_cls `hasKey` genClassKey is_generic1 = main_cls `hasKey` gen1ClassKey -- is_functor_like: see Note [Inferring the instance context] - is_functor_like = typeKind inst_ty `tcEqKind` typeToTypeKind + is_functor_like = tcTypeKind inst_ty `tcEqKind` typeToTypeKind || is_generic1 get_gen1_constraints :: Class -> CtOrigin -> TypeOrKind -> Type @@ -191,7 +191,7 @@ inferConstraintsDataConArgs inst_ty inst_tys -- message which points out the kind mismatch. -- See Note [Inferring the instance context] mk_functor_like_constraints orig t_or_k cls - = map $ \ty -> let ki = typeKind ty in + = map $ \ty -> let ki = tcTypeKind ty in ( [ mk_cls_pred orig t_or_k cls ty , mkPredOrigin orig KindLevel (mkPrimEqPred ki typeToTypeKind) ] @@ -232,7 +232,7 @@ inferConstraintsDataConArgs inst_ty inst_tys where constrs | main_cls `hasKey` dataClassKey - , all (isLiftedTypeKind . typeKind) rep_tc_args + , all (isLiftedTypeKind . tcTypeKind) rep_tc_args = [ mk_cls_pred deriv_origin t_or_k main_cls ty | (t_or_k, ty) <- zip t_or_ks rep_tc_args] | otherwise diff --git a/compiler/typecheck/TcErrors.hs b/compiler/typecheck/TcErrors.hs index 951107bbcf..72e2157bc3 100644 --- a/compiler/typecheck/TcErrors.hs +++ b/compiler/typecheck/TcErrors.hs @@ -599,7 +599,7 @@ reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_impl = implics }) is_user_type_error ct _ = isUserTypeErrorCt ct - is_homo_equality _ (EqPred _ ty1 ty2) = typeKind ty1 `tcEqType` typeKind ty2 + is_homo_equality _ (EqPred _ ty1 ty2) = tcTypeKind ty1 `tcEqType` tcTypeKind ty2 is_homo_equality _ _ = False is_equality _ (EqPred {}) = True @@ -1171,7 +1171,7 @@ mkHoleError tidy_simples ctxt ct@(CHoleCan { cc_hole = hole }) where occ = holeOcc hole hole_ty = ctEvPred (ctEvidence ct) - hole_kind = typeKind hole_ty + hole_kind = tcTypeKind hole_ty tyvars = tyCoVarsOfTypeList hole_ty hole_msg = case hole of @@ -1494,9 +1494,9 @@ mkEqErr1 ctxt ct -- Wanted or derived; || not (cty1 `pickyEqType` cty2) -> hang (text "When matching" <+> sub_what) 2 (vcat [ ppr cty1 <+> dcolon <+> - ppr (typeKind cty1) + ppr (tcTypeKind cty1) , ppr cty2 <+> dcolon <+> - ppr (typeKind cty2) ]) + ppr (tcTypeKind cty2) ]) _ -> text "When matching the kind of" <+> quotes (ppr cty1) msg2 = case sub_o of TypeEqOrigin {} @@ -1744,7 +1744,7 @@ mkTyVarEqErr' dflags ctxt report ct oriented tv1 co1 ty2 -- Not an occurs check, because F is a type function. where Pair _ k1 = tcCoercionKind co1 - k2 = typeKind ty2 + k2 = tcTypeKind ty2 ty1 = mkTyVarTy tv1 occ_check_expand = occCheckForErrors dflags tv1 ty2 @@ -2501,7 +2501,7 @@ mk_dict_err ctxt@(CEC {cec_encl = implics}) (ct, (matches, unifiers, unsafe_over , not (isTypeFamilyTyCon tc) = hang (text "GHC can't yet do polykinded") 2 (text "Typeable" <+> - parens (ppr ty <+> dcolon <+> ppr (typeKind ty))) + parens (ppr ty <+> dcolon <+> ppr (tcTypeKind ty))) | otherwise = empty diff --git a/compiler/typecheck/TcExpr.hs b/compiler/typecheck/TcExpr.hs index 17678a5cd1..55e7beda31 100644 --- a/compiler/typecheck/TcExpr.hs +++ b/compiler/typecheck/TcExpr.hs @@ -388,7 +388,7 @@ tcExpr expr@(OpApp fix arg1 op arg2) res_ty -- The *result* type can have any kind (Trac #8739), -- so we don't need to check anything for that ; _ <- unifyKind (Just (XHsType $ NHsCoreTy arg2_sigma)) - (typeKind arg2_sigma) liftedTypeKind + (tcTypeKind arg2_sigma) liftedTypeKind -- ignore the evidence. arg2_sigma must have type * or #, -- because we know arg2_sigma -> or_res_ty is well-kinded -- (because otherwise matchActualFunTys would fail) @@ -1348,7 +1348,7 @@ tcArgs fun orig_fun_ty fun_orig orig_args herald -- substitution is kind-respecting ; traceTc "VTA" (vcat [ppr tv, debugPprType kind , debugPprType ty_arg - , debugPprType (typeKind ty_arg) + , debugPprType (tcTypeKind ty_arg) , debugPprType inner_ty , debugPprType insted_ty ]) diff --git a/compiler/typecheck/TcFlatten.hs b/compiler/typecheck/TcFlatten.hs index add0a6f913..b3c41a5711 100644 --- a/compiler/typecheck/TcFlatten.hs +++ b/compiler/typecheck/TcFlatten.hs @@ -771,7 +771,7 @@ flattenArgsNom :: CtEvidence -> TyCon -> [TcType] -> TcS ([Xi], [TcCoercion], Tc -- ctEvFlavour ev = Nominal -- and we want to flatten all at nominal role -- The kind passed in is the kind of the type family or class, call it T --- The last coercion returned has type (typeKind(T xis) ~N typeKind(T tys)) +-- The last coercion returned has type (tcTypeKind(T xis) ~N tcTypeKind(T tys)) -- -- For Derived constraints the returned coercion may be undefined -- because flattening may use a Derived equality ([D] a ~ ty) @@ -800,8 +800,8 @@ flattenArgsNom ev tc tys Key invariants: (F0) co :: xi ~ zonk(ty) - (F1) typeKind(xi) succeeds and returns a fully zonked kind - (F2) typeKind(xi) `eqType` zonk(typeKind(ty)) + (F1) tcTypeKind(xi) succeeds and returns a fully zonked kind + (F2) tcTypeKind(xi) `eqType` zonk(tcTypeKind(ty)) Note that it is flatten's job to flatten *every type function it sees*. flatten is only called on *arguments* to type functions, by canEqGiven. @@ -814,7 +814,7 @@ Because flattening zonks and the returned coercion ("co" above) is also zonked, it's possible that (co :: xi ~ ty) isn't quite true. So, instead, we can rely on this fact: - (F1) typeKind(xi) succeeds and returns a fully zonked kind + (F1) tcTypeKind(xi) succeeds and returns a fully zonked kind Note that the left-hand type of co is *always* precisely xi. The right-hand type may or may not be ty, however: if ty has unzonked filled-in metavariables, @@ -824,14 +824,14 @@ occasionally have to explicitly zonk, when (co :: xi ~ ty) is important even before we zonk the whole program. For example, see the FTRNotFollowed case in flattenTyVar. -Why have these invariants on flattening? Because we sometimes use typeKind +Why have these invariants on flattening? Because we sometimes use tcTypeKind during canonicalisation, and we want this kind to be zonked (e.g., see TcCanonical.canEqTyVar). Flattening is always homogeneous. That is, the kind of the result of flattening is always the same as the kind of the input, modulo zonking. More formally: - (F2) typeKind(xi) `eqType` zonk(typeKind(ty)) + (F2) tcTypeKind(xi) `eqType` zonk(tcTypeKind(ty)) This invariant means that the kind of a flattened type might not itself be flat. @@ -1162,7 +1162,7 @@ flatten_args :: [TyCoBinder] -> Bool -- Binders, and True iff any of them are -> [Role] -> [Type] -- these are in 1-to-1 correspondence -> FlatM ([Xi], [Coercion], CoercionN) -- Coercions :: Xi ~ Type, at roles given --- Third coercion :: typeKind(fun xis) ~N typeKind(fun tys) +-- Third coercion :: tcTypeKind(fun xis) ~N tcTypeKind(fun tys) -- That is, the third coercion relates the kind of some function (whose kind is -- passed as the first parameter) instantiated at xis to the kind of that -- function instantiated at the tys. This is useful in keeping flattening @@ -1294,7 +1294,7 @@ flatten_args_slow orig_binders orig_inner_ki orig_fvs orig_roles orig_tys ; return (ty, mkReflCo Phantom ty) } -- By Note [Flattening] invariant (F2), - -- typeKind(xi) = typeKind(ty). But, it's possible that xi will be + -- tcTypeKind(xi) = tcTypeKind(ty). But, it's possible that xi will be -- used as an argument to a function whose kind is different, if -- earlier arguments have been flattened to new types. We thus -- need a coercion (kind_co :: old_kind ~ new_kind). @@ -1475,7 +1475,7 @@ flatten_app_ty_args fun_xi fun_co arg_tys do { let tc_roles = tyConRolesRepresentational tc arg_roles = dropList xis tc_roles ; (arg_xis, arg_cos, kind_co) - <- flatten_vector (typeKind fun_xi) arg_roles arg_tys + <- flatten_vector (tcTypeKind fun_xi) arg_roles arg_tys -- Here, we have fun_co :: T xi1 xi2 ~ ty -- and we need to apply fun_co to the arg_cos. The problem is @@ -1494,7 +1494,7 @@ flatten_app_ty_args fun_xi fun_co arg_tys ; return (app_xi, app_co, kind_co) } Nothing -> do { (arg_xis, arg_cos, kind_co) - <- flatten_vector (typeKind fun_xi) (repeat Nominal) arg_tys + <- flatten_vector (tcTypeKind fun_xi) (repeat Nominal) arg_tys ; let arg_xi = mkAppTys fun_xi arg_xis arg_co = mkAppCos fun_co arg_cos ; return (arg_xi, arg_co, kind_co) } @@ -1514,7 +1514,7 @@ flatten_ty_con_app tc tys homogenise_result :: Xi -- a flattened type -> Coercion -- :: xi ~r original ty -> Role -- r - -> CoercionN -- kind_co :: typeKind(xi) ~N typeKind(ty) + -> CoercionN -- kind_co :: tcTypeKind(xi) ~N tcTypeKind(ty) -> (Xi, Coercion) -- (xi |> kind_co, (xi |> kind_co) -- ~r original ty) homogenise_result xi co r kind_co @@ -1624,9 +1624,9 @@ flatten_fam_app tc tys -- Can be over-saturated flatten_exact_fam_app_fully :: TyCon -> [TcType] -> FlatM (Xi, Coercion) flatten_exact_fam_app_fully tc tys -- See Note [Reduce type family applications eagerly] - -- the following typeKind should never be evaluated, as it's just used in + -- the following tcTypeKind should never be evaluated, as it's just used in -- casting, and casts by refl are dropped - = do { let reduce_co = mkNomReflCo (typeKind (mkTyConApp tc tys)) + = do { let reduce_co = mkNomReflCo (tcTypeKind (mkTyConApp tc tys)) ; mOut <- try_to_reduce_nocache tc tys reduce_co id ; case mOut of Just out -> pure out @@ -1636,7 +1636,7 @@ flatten_exact_fam_app_fully tc tys <- setEqRel NomEq $ -- just do this once, instead of for -- each arg flatten_args_tc tc (repeat Nominal) tys - -- kind_co :: typeKind(F xis) ~N typeKind(F tys) + -- kind_co :: tcTypeKind(F xis) ~N tcTypeKind(F tys) ; eq_rel <- getEqRel ; cur_flav <- getFlavour ; let role = eqRelRole eq_rel @@ -1711,8 +1711,8 @@ flatten_exact_fam_app_fully tc tys try_to_reduce :: TyCon -- F, family tycon -> [Type] -- args, not necessarily flattened - -> CoercionN -- kind_co :: typeKind(F args) ~N - -- typeKind(F orig_args) + -> CoercionN -- kind_co :: tcTypeKind(F args) ~N + -- tcTypeKind(F orig_args) -- where -- orig_args is what was passed to the outer -- function @@ -1749,8 +1749,8 @@ flatten_exact_fam_app_fully tc tys try_to_reduce_nocache :: TyCon -- F, family tycon -> [Type] -- args, not necessarily flattened - -> CoercionN -- kind_co :: typeKind(F args) - -- ~N typeKind(F orig_args) + -> CoercionN -- kind_co :: tcTypeKind(F args) + -- ~N tcTypeKind(F orig_args) -- where -- orig_args is what was passed to the -- outer function @@ -2060,7 +2060,7 @@ unflattenWanteds tv_eqs funeqs -- NB: unlike unflattenFmv, filling a fmv here /does/ -- bump the unification count; it is "improvement" -- Note [Unflattening can force the solver to iterate] - = ASSERT2( tyVarKind tv `eqType` typeKind rhs, ppr ct ) + = ASSERT2( tyVarKind tv `eqType` tcTypeKind rhs, ppr ct ) -- CTyEqCan invariant should ensure this is true do { is_filled <- isFilledMetaTyVar tv ; elim <- case is_filled of diff --git a/compiler/typecheck/TcHsSyn.hs b/compiler/typecheck/TcHsSyn.hs index 3363aa2be0..37d1b8ea2b 100644 --- a/compiler/typecheck/TcHsSyn.hs +++ b/compiler/typecheck/TcHsSyn.hs @@ -1029,7 +1029,7 @@ zonk_cmd_top env (HsCmdTop (CmdTopTc stack_tys ty ids) cmd) new_ty <- zonkTcTypeToTypeX env ty new_ids <- mapSndM (zonkExpr env) ids - MASSERT( isLiftedTypeKind (typeKind new_stack_tys) ) + MASSERT( isLiftedTypeKind (tcTypeKind new_stack_tys) ) -- desugarer assumes that this is not levity polymorphic... -- but indeed it should always be lifted due to the typing -- rules for arrows diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs index 24299dd84b..bcb05b3a14 100644 --- a/compiler/typecheck/TcHsType.hs +++ b/compiler/typecheck/TcHsType.hs @@ -479,7 +479,7 @@ missing any patterns. Note [The tcType invariant] ~~~~~~~~~~~~~~~~~~~~~~~~~~~ (IT1) If tc_ty = tc_hs_type hs_ty exp_kind - then typeKind tc_ty = exp_kind + then tcTypeKind tc_ty = exp_kind without any zonking needed. The reason for this is that in tcInferApps we see (F ty), and we kind-check 'ty' with an expected-kind coming from F. Then, to make the resulting application @@ -492,17 +492,17 @@ The tcType invariant also applies to checkExpectedKind: (IT2) if (tc_ty, _, _) = checkExpectedKind ty act_ki exp_ki then - typeKind tc_ty = exp_ki + tcTypeKind tc_ty = exp_ki These other invariants are all necessary, too, as these functions are used within tc_hs_type: -(IT3) If (ty, ki) <- tc_infer_hs_type ..., then typeKind ty == ki. +(IT3) If (ty, ki) <- tc_infer_hs_type ..., then tcTypeKind ty == ki. (IT4) If (ty, ki) <- tc_infer_hs_type ..., then zonk ki == ki. (In other words, the result kind of tc_infer_hs_type is zonked.) -(IT5) If (ty, ki) <- tcTyVar ..., then typeKind ty == ki. +(IT5) If (ty, ki) <- tcTyVar ..., then tcTypeKind ty == ki. (IT6) If (ty, ki) <- tcTyVar ..., then zonk ki == ki. (In other words, the result kind of tcTyVar is zonked.) @@ -559,7 +559,7 @@ tc_infer_hs_type mode (HsSpliceTy _ (HsSpliced _ _ (HsSplicedTy ty))) tc_infer_hs_type mode (HsDocTy _ ty _) = tc_infer_lhs_type mode ty tc_infer_hs_type _ (XHsType (NHsCoreTy ty)) = do { ty <- zonkTcType ty -- (IT3) and (IT4) of Note [The tcType invariant] - ; return (ty, typeKind ty) } + ; return (ty, tcTypeKind ty) } tc_infer_hs_type mode other_ty = do { kv <- newMetaKindVar ; ty' <- tc_hs_type mode other_ty kv @@ -863,7 +863,7 @@ tcInferApps :: TcTyMode -> TcKind -- ^ Function kind (zonked) -> [LHsType GhcRn] -- ^ Args -> TcM (TcType, [TcType], TcKind) -- ^ (f args, args, result kind) --- Precondition: typeKind fun_ty = fun_ki +-- Precondition: tcTypeKind fun_ty = fun_ki -- Reason: we will return a type application like (fun_ty arg1 ... argn), -- and that type must be well-kinded -- See Note [The tcType invariant] @@ -1088,7 +1088,7 @@ tcTyVar mode name -- Could be a tyvar, a tycon, or a datacon -- want to zonk the kind, leaving the TyVar -- un-zonked (Trac #14873) do { ty <- zonkTcTyVar tv - ; return (ty, typeKind ty) } + ; return (ty, tcTypeKind ty) } ATcTyCon tc_tc -> do { -- See Note [GADT kind self-reference] unless diff --git a/compiler/typecheck/TcInteract.hs b/compiler/typecheck/TcInteract.hs index 32b4718577..57996479b0 100644 --- a/compiler/typecheck/TcInteract.hs +++ b/compiler/typecheck/TcInteract.hs @@ -1634,8 +1634,8 @@ solveByUnification wd tv xi ; traceTcS "Sneaky unification:" $ vcat [text "Unifies:" <+> ppr tv <+> text ":=" <+> ppr xi, text "Coercion:" <+> pprEq tv_ty xi, - text "Left Kind is:" <+> ppr (typeKind tv_ty), - text "Right Kind is:" <+> ppr (typeKind xi) ] + text "Left Kind is:" <+> ppr (tcTypeKind tv_ty), + text "Right Kind is:" <+> ppr (tcTypeKind xi) ] ; unifyTyVar tv xi ; setEvBindIfWanted wd (evCoercion (mkTcNomReflCo xi)) } diff --git a/compiler/typecheck/TcMType.hs b/compiler/typecheck/TcMType.hs index fb5f1b515a..4c267b1906 100644 --- a/compiler/typecheck/TcMType.hs +++ b/compiler/typecheck/TcMType.hs @@ -603,7 +603,7 @@ newFskTyVar fam_ty , mtv_ref = ref , mtv_tclvl = tclvl } name = mkMetaTyVarName uniq (fsLit "fsk") - ; return (mkTcTyVar name (typeKind fam_ty) details) } + ; return (mkTcTyVar name (tcTypeKind fam_ty) details) } {- Note [Kind substitution when instantiating] @@ -675,7 +675,7 @@ newFmvTyVar fam_ty , mtv_ref = ref , mtv_tclvl = tclvl } name = mkMetaTyVarName uniq (fsLit "s") - ; return (mkTcTyVar name (typeKind fam_ty) details) } + ; return (mkTcTyVar name (tcTypeKind fam_ty) details) } newMetaDetails :: MetaInfo -> TcM TcTyVarDetails newMetaDetails info @@ -756,8 +756,8 @@ writeMetaTyVarRef tyvar ref ty -- Zonk kinds to allow the error check to work ; zonked_tv_kind <- zonkTcType tv_kind ; zonked_ty <- zonkTcType ty - ; let zonked_ty_kind = typeKind zonked_ty -- need to zonk even before typeKind; - -- otherwise, we can panic in piResultTy + ; let zonked_ty_kind = tcTypeKind zonked_ty -- Need to zonk even before typeKind; + -- otherwise, we can panic in piResultTy kind_check_ok = tcIsConstraintKind zonked_tv_kind || tcEqKind zonked_ty_kind zonked_tv_kind -- Hack alert! tcIsConstraintKind: see TcHsType @@ -1812,4 +1812,4 @@ formatLevPolyErr ty , text "Kind:" <+> pprWithTYPE tidy_ki ]) where (tidy_env, tidy_ty) = tidyOpenType emptyTidyEnv ty - tidy_ki = tidyType tidy_env (typeKind ty) + tidy_ki = tidyType tidy_env (tcTypeKind ty) diff --git a/compiler/typecheck/TcPat.hs b/compiler/typecheck/TcPat.hs index ed797d389c..ae1a06e30b 100644 --- a/compiler/typecheck/TcPat.hs +++ b/compiler/typecheck/TcPat.hs @@ -350,7 +350,7 @@ tc_pat penv (LazyPat x pat) pat_ty thing_inside -- Check that the expected pattern type is itself lifted ; pat_ty <- readExpType pat_ty - ; _ <- unifyType Nothing (typeKind pat_ty) liftedTypeKind + ; _ <- unifyType Nothing (tcTypeKind pat_ty) liftedTypeKind ; return (LazyPat x pat', res) } diff --git a/compiler/typecheck/TcPatSyn.hs b/compiler/typecheck/TcPatSyn.hs index 8f59e39a4f..0a3d6e3d1d 100644 --- a/compiler/typecheck/TcPatSyn.hs +++ b/compiler/typecheck/TcPatSyn.hs @@ -194,8 +194,8 @@ mkProvEvidence :: EvId -> Maybe (PredType, EvTerm) -- See Note [Equality evidence in pattern synonyms] mkProvEvidence ev_id | EqPred r ty1 ty2 <- classifyPredType pred - , let k1 = typeKind ty1 - k2 = typeKind ty2 + , let k1 = tcTypeKind ty1 + k2 = tcTypeKind ty2 is_homo = k1 `tcEqType` k2 homo_tys = [k1, ty1, ty2] hetero_tys = [k1, k2, ty1, ty2] diff --git a/compiler/typecheck/TcRnDriver.hs b/compiler/typecheck/TcRnDriver.hs index 4d2141bddf..f439d45f17 100644 --- a/compiler/typecheck/TcRnDriver.hs +++ b/compiler/typecheck/TcRnDriver.hs @@ -2404,7 +2404,7 @@ tcRnType hsc_env normalise rdr_type ; return ty' } else return ty ; - ; return (ty', mkInvForAllTys kvs (typeKind ty')) } + ; return (ty', mkInvForAllTys kvs (tcTypeKind ty')) } {- Note [TcRnExprMode] ~~~~~~~~~~~~~~~~~~~~~~ diff --git a/compiler/typecheck/TcRnTypes.hs b/compiler/typecheck/TcRnTypes.hs index a41197521c..02484e6689 100644 --- a/compiler/typecheck/TcRnTypes.hs +++ b/compiler/typecheck/TcRnTypes.hs @@ -1699,7 +1699,7 @@ data Ct -- * tv not in tvs(rhs) (occurs check) -- * If tv is a TauTv, then rhs has no foralls -- (this avoids substituting a forall for the tyvar in other types) - -- * typeKind ty `tcEqKind` typeKind tv; Note [Ct kind invariant] + -- * tcTypeKind ty `tcEqKind` tcTypeKind tv; Note [Ct kind invariant] -- * rhs may have at most one top-level cast -- * rhs (perhaps under the one cast) is not necessarily function-free, -- but it has no top-level function. @@ -1722,7 +1722,7 @@ data Ct | CFunEqCan { -- F xis ~ fsk -- Invariants: -- * isTypeFamilyTyCon cc_fun - -- * typeKind (F xis) = tyVarKind fsk; Note [Ct kind invariant] + -- * tcTypeKind (F xis) = tyVarKind fsk; Note [Ct kind invariant] -- * always Nominal role cc_ev :: CtEvidence, -- See Note [Ct/evidence invariant] cc_fun :: TyCon, -- A type function diff --git a/compiler/typecheck/TcSimplify.hs b/compiler/typecheck/TcSimplify.hs index 562340f0da..03d7f97c2a 100644 --- a/compiler/typecheck/TcSimplify.hs +++ b/compiler/typecheck/TcSimplify.hs @@ -2110,7 +2110,7 @@ to ensure that instance declarations match. For example consider foo x = show (\_ -> True) Then we'll get a constraint (Show (p ->q)) where p has kind (TYPE r), -and that won't match the typeKind (*) in the instance decl. See tests +and that won't match the tcTypeKind (*) in the instance decl. See tests tc217 and tc175. We look only at touchable type variables. No further constraints @@ -2324,7 +2324,7 @@ floatEqualities skols given_ids ev_binds_var no_given_eqs is_float_eq_candidate ct | pred <- ctPred ct , EqPred NomEq ty1 ty2 <- classifyPredType pred - , typeKind ty1 `tcEqType` typeKind ty2 + , tcTypeKind ty1 `tcEqType` tcTypeKind ty2 = case (tcGetTyVar_maybe ty1, tcGetTyVar_maybe ty2) of (Just tv1, _) -> float_tv_eq_candidate tv1 ty2 (_, Just tv2) -> float_tv_eq_candidate tv2 ty1 diff --git a/compiler/typecheck/TcSplice.hs b/compiler/typecheck/TcSplice.hs index a4f81282b3..005a02cfbf 100644 --- a/compiler/typecheck/TcSplice.hs +++ b/compiler/typecheck/TcSplice.hs @@ -1197,7 +1197,7 @@ reifyInstances th_nm th_tys -- In particular, the type might have kind -- variables inside it (Trac #7477) - ; traceTc "reifyInstances" (ppr ty $$ ppr (typeKind ty)) + ; traceTc "reifyInstances" (ppr ty $$ ppr (tcTypeKind ty)) ; case splitTyConApp_maybe ty of -- This expands any type synonyms Just (tc, tys) -- See Trac #7910 | Just cls <- tyConClass_maybe tc @@ -1634,7 +1634,7 @@ annotThType :: Bool -- True <=> annotate annotThType _ _ th_ty@(TH.SigT {}) = return th_ty annotThType True ty th_ty | not $ isEmptyVarSet $ filterVarSet isTyVar $ tyCoVarsOfType ty - = do { let ki = typeKind ty + = do { let ki = tcTypeKind ty ; th_ki <- reifyKind ki ; return (TH.SigT th_ty th_ki) } annotThType _ _ th_ty = return th_ty @@ -1941,7 +1941,7 @@ reify_tc_app tc tys -- See Note [Kind annotations on TyConApps] maybe_sig_t th_type | needs_kind_sig - = do { let full_kind = typeKind (mkTyConApp tc tys) + = do { let full_kind = tcTypeKind (mkTyConApp tc tys) ; th_full_kind <- reifyKind full_kind ; return (TH.SigT th_type th_full_kind) } | otherwise diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs index 20c79bd46f..db8139b1dd 100644 --- a/compiler/typecheck/TcTyClsDecls.hs +++ b/compiler/typecheck/TcTyClsDecls.hs @@ -2262,8 +2262,8 @@ rejigConRes tmpl_bndrs res_tmpl dc_inferred_tvs dc_specified_tvs res_ty -- So we return ( [a,b,z], [x,y] -- , [], [x,y,z] -- , [a~(x,y),b~z], <arg-subst> ) - | Just subst <- ASSERT( isLiftedTypeKind (typeKind res_ty) ) - ASSERT( isLiftedTypeKind (typeKind res_tmpl) ) + | Just subst <- ASSERT( isLiftedTypeKind (tcTypeKind res_ty) ) + ASSERT( isLiftedTypeKind (tcTypeKind res_tmpl) ) tcMatchTy res_tmpl res_ty = let (univ_tvs, raw_eqs, kind_subst) = mkGADTVars tmpl_tvs dc_tvs subst raw_ex_tvs = dc_tvs `minusList` univ_tvs @@ -2783,8 +2783,8 @@ checkValidDataCon dflags existential_ok tc con orig_res_ty = dataConOrigResTy con ; traceTc "checkValidDataCon" (vcat [ ppr con, ppr tc, ppr tc_tvs - , ppr res_ty_tmpl <+> dcolon <+> ppr (typeKind res_ty_tmpl) - , ppr orig_res_ty <+> dcolon <+> ppr (typeKind orig_res_ty)]) + , ppr res_ty_tmpl <+> dcolon <+> ppr (tcTypeKind res_ty_tmpl) + , ppr orig_res_ty <+> dcolon <+> ppr (tcTypeKind orig_res_ty)]) ; checkTc (isJust (tcMatchTy res_ty_tmpl diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs index 5bbaa0fe81..d8f4590d15 100644 --- a/compiler/typecheck/TcType.hs +++ b/compiler/typecheck/TcType.hs @@ -123,7 +123,7 @@ module TcType ( -------------------------------- -- Rexported from Kind - Kind, typeKind, + Kind, typeKind, tcTypeKind, liftedTypeKind, constraintKind, isLiftedTypeKind, isUnliftedTypeKind, classifiesTypeWithValues, @@ -1380,7 +1380,7 @@ See also Note [The tcType invariant] in TcHsType. During type inference, we maintain this invariant - (INV-TK): it is legal to call 'typeKind' on any Type ty, + (INV-TK): it is legal to call 'tcTypeKind' on any Type ty, /without/ zonking ty For example, suppose @@ -1390,12 +1390,12 @@ For example, suppose a :: kappa then consider the type (a Int) -If we call typeKind on that, we'll crash, because the (un-zonked) +If we call tcTypeKind on that, we'll crash, because the (un-zonked) kind of 'a' is just kappa, not an arrow kind. If we zonk first we'd be fine, but that is too tiresome, so instead we maintain (INV-TK). So we do not form (a Int); instead we form (a |> co) Int -and typeKind has no problem with that. +and tcTypeKind has no problem with that. Bottom line: we want to keep that 'co' /even though it is Refl/. @@ -1647,7 +1647,7 @@ tcSplitFunTy_maybe :: Type -> Maybe (Type, Type) tcSplitFunTy_maybe ty | Just ty' <- tcView ty = tcSplitFunTy_maybe ty' tcSplitFunTy_maybe (FunTy arg res) | not (isPredTy arg) = Just (arg, res) tcSplitFunTy_maybe _ = Nothing - -- Note the typeKind guard + -- Note the tcTypeKind guard -- Consider (?x::Int) => Bool -- We don't want to treat this as a function type! -- A concrete example is test tc230: @@ -1798,8 +1798,8 @@ tcEqType ty1 ty2 = isNothing (tc_eq_type tcView ki1 ki2) && isNothing (tc_eq_type tcView ty1 ty2) where - ki1 = typeKind ty1 - ki2 = typeKind ty2 + ki1 = tcTypeKind ty1 + ki2 = tcTypeKind ty2 -- | Just like 'tcEqType', but will return True for types of different kinds -- as long as their non-coercion structure is identical. @@ -1816,8 +1816,8 @@ tcEqTypeVis :: TcType -> TcType -> Maybe Bool tcEqTypeVis ty1 ty2 = tc_eq_type tcView ty1 ty2 <!> invis (tc_eq_type tcView ki1 ki2) where - ki1 = typeKind ty1 - ki2 = typeKind ty2 + ki1 = tcTypeKind ty1 + ki2 = tcTypeKind ty2 -- convert Just True to Just False invis :: Maybe Bool -> Maybe Bool @@ -2054,8 +2054,8 @@ boxEqPred eq_rel ty1 ty2 -- so we can't abstract over it -- Nothing fundamental: we could add it where - k1 = typeKind ty1 - k2 = typeKind ty2 + k1 = tcTypeKind ty1 + k2 = tcTypeKind ty2 homo_kind = k1 `tcEqType` k2 pickCapturedPreds diff --git a/compiler/typecheck/TcUnify.hs b/compiler/typecheck/TcUnify.hs index 05a30fdf35..cf84bbe042 100644 --- a/compiler/typecheck/TcUnify.hs +++ b/compiler/typecheck/TcUnify.hs @@ -440,7 +440,7 @@ matchExpectedAppTy orig_ty ; co <- unifyType Nothing (mkAppTy ty1 ty2) orig_ty ; return (co, (ty1, ty2)) } - orig_kind = typeKind orig_ty + orig_kind = tcTypeKind orig_ty kind1 = mkFunTy liftedTypeKind orig_kind kind2 = liftedTypeKind -- m :: * -> k -- arg type :: * @@ -911,7 +911,7 @@ fill_infer_result orig_ty (IR { ir_uniq = u, ir_lvl = res_lvl = do { let ty_lvl = tcTypeLevel ty ; MASSERT2( not (ty_lvl `strictlyDeeperThan` res_lvl), ppr u $$ ppr res_lvl $$ ppr ty_lvl $$ - ppr ty <+> dcolon <+> ppr (typeKind ty) $$ ppr orig_ty ) + ppr ty <+> dcolon <+> ppr (tcTypeKind ty) $$ ppr orig_ty ) ; cts <- readTcRef ref ; case cts of Just already_there -> pprPanic "writeExpType" @@ -993,12 +993,12 @@ promoteTcType dest_lvl ty dont_promote_it :: TcM (TcCoercion, TcType) dont_promote_it -- Check that ty :: TYPE rr, for some (fresh) rr = do { res_kind <- newOpenTypeKind - ; let ty_kind = typeKind ty + ; let ty_kind = tcTypeKind ty kind_orig = TypeEqOrigin { uo_actual = ty_kind , uo_expected = res_kind , uo_thing = Nothing , uo_visible = False } - ; ki_co <- uType KindLevel kind_orig (typeKind ty) res_kind + ; ki_co <- uType KindLevel kind_orig (tcTypeKind ty) res_kind ; let co = mkTcGReflRightCo Nominal ty ki_co ; return (co, ty `mkCastTy` ki_co) } @@ -1632,10 +1632,10 @@ uUnfilledVar2 origin t_or_k swapped tv1 ty2 go dflags cur_lvl | canSolveByUnification cur_lvl tv1 ty2 , Just ty2' <- metaTyVarUpdateOK dflags tv1 ty2 - = do { co_k <- uType KindLevel kind_origin (typeKind ty2') (tyVarKind tv1) + = do { co_k <- uType KindLevel kind_origin (tcTypeKind ty2') (tyVarKind tv1) ; traceTc "uUnfilledVar2 ok" $ vcat [ ppr tv1 <+> dcolon <+> ppr (tyVarKind tv1) - , ppr ty2 <+> dcolon <+> ppr (typeKind ty2) + , ppr ty2 <+> dcolon <+> ppr (tcTypeKind ty2) , ppr (isTcReflCo co_k), ppr co_k ] ; if isTcReflCo co_k -- only proceed if the kinds matched. diff --git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs index 392c2543a6..7c50d24377 100644 --- a/compiler/typecheck/TcValidity.hs +++ b/compiler/typecheck/TcValidity.hs @@ -316,7 +316,7 @@ checkValidType :: UserTypeCtxt -> Type -> TcM () -- Assumes argument is fully zonked -- Not used for instance decls; checkValidInstance instead checkValidType ctxt ty - = do { traceTc "checkValidType" (ppr ty <+> text "::" <+> ppr (typeKind ty)) + = do { traceTc "checkValidType" (ppr ty <+> text "::" <+> ppr (tcTypeKind ty)) ; rankn_flag <- xoptM LangExt.RankNTypes ; impred_flag <- xoptM LangExt.ImpredicativeTypes ; let gen_rank :: Rank -> Rank @@ -376,7 +376,7 @@ checkValidType ctxt ty -- and there may be nested foralls for the subtype test to examine ; checkAmbiguity ctxt ty - ; traceTc "checkValidType done" (ppr ty <+> text "::" <+> ppr (typeKind ty)) } + ; traceTc "checkValidType done" (ppr ty <+> text "::" <+> ppr (tcTypeKind ty)) } checkValidMonoType :: Type -> TcM () -- Assumes argument is fully zonked @@ -397,7 +397,7 @@ checkTySynRhs ctxt ty | otherwise = return () where - actual_kind = typeKind ty + actual_kind = tcTypeKind ty -- | The kind expected in a certain context. data ContextKind = TheKind Kind -- ^ a specific kind @@ -487,7 +487,7 @@ check_type env ctxt rank ty tvs = binderVars tvbs (env', _) = tidyVarBndrs env tvs - tau_kind = typeKind tau + tau_kind = tcTypeKind tau phi_kind | null theta = tau_kind | otherwise = liftedTypeKind -- If there are any constraints, the kind is *. (#11405) @@ -1828,7 +1828,7 @@ checkConsistentFamInst (Just (clas, inst_tvs, mini_env)) fam_tc at_tys pp_hs_pat (tidy_env2, expected_args) = tidyOpenTypes tidy_env1 [ exp_ty `orElse` mk_tv at_ty | (exp_ty, at_ty) <- arg_shapes ] - mk_tv at_ty = mkTyVarTy (mkTyVar tv_name (typeKind at_ty)) + mk_tv at_ty = mkTyVarTy (mkTyVar tv_name (tcTypeKind at_ty)) tv_name = mkInternalName (mkAlphaTyVarUnique 1) (mkTyVarOcc "<tv>") noSrcSpan has_poly_args dflags = any (isNothing . fst) shapes diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs index 34639202db..ca008f1261 100644 --- a/compiler/types/Type.hs +++ b/compiler/types/Type.hs @@ -129,7 +129,7 @@ module Type ( Kind, -- ** Finding the kind of a type - typeKind, isTypeLevPoly, resultIsLevPoly, + typeKind, tcTypeKind, isTypeLevPoly, resultIsLevPoly, tcIsLiftedTypeKind, tcIsConstraintKind, tcReturnsConstraintKind, -- ** Common Kind @@ -2627,30 +2627,64 @@ nonDetCmpTc tc1 tc2 typeKind :: HasDebugCallStack => Type -> Kind typeKind (TyConApp tc tys) = piResultTys (tyConKind tc) tys -typeKind (AppTy fun arg) = typeKind_apps fun [arg] typeKind (LitTy l) = typeLiteralKind l typeKind (FunTy {}) = liftedTypeKind typeKind (TyVarTy tyvar) = tyVarKind tyvar typeKind (CastTy _ty co) = pSnd $ coercionKind co typeKind (CoercionTy co) = coercionType co + +typeKind (AppTy fun arg) + = go fun [arg] + where + -- Accumulate the type arugments, so we can call piResultTys, + -- rather than a succession of calls to piResultTy (which is + -- asymptotically costly as the number of arguments increases) + go (AppTy fun arg) args = go fun (arg:args) + go fun args = piResultTys (typeKind fun) args + typeKind ty@(ForAllTy (Bndr tv _) _) | isTyVar tv -- See Note [Weird typing rule for ForAllTy]. = case occCheckExpand tvs k of -- We must make sure tv does not occur in kind Just k' -> k' -- As it is already out of scope! Nothing -> pprPanic "typeKind" (ppr ty $$ ppr k $$ ppr tvs $$ ppr body) + | otherwise + = liftedTypeKind where (tvs, body) = splitTyVarForAllTys ty k = typeKind body -typeKind (ForAllTy {}) = liftedTypeKind - -typeKind_apps :: HasDebugCallStack => Type -> [Type] -> Kind --- The sole purpose of the function is to accumulate --- the type arugments, so we can call piResultTys, rather than --- a succession of calls to piResultTy (which is asymptotically --- less efficient as the number of arguments increases) -typeKind_apps (AppTy fun arg) args = typeKind_apps fun (arg:args) -typeKind_apps fun args = piResultTys (typeKind fun) args + +tcTypeKind :: HasDebugCallStack => Type -> Kind +tcTypeKind (TyConApp tc tys) = piResultTys (tyConKind tc) tys +tcTypeKind (LitTy l) = typeLiteralKind l +tcTypeKind (FunTy arg res) + | isPredTy arg = tcTypeKind res + | otherwise = liftedTypeKind +tcTypeKind (TyVarTy tyvar) = tyVarKind tyvar +tcTypeKind (CastTy _ty co) = pSnd $ coercionKind co +tcTypeKind (CoercionTy co) = coercionType co + +tcTypeKind (AppTy fun arg) + = go fun [arg] + where + -- Accumulate the type arugments, so we can call piResultTys, + -- rather than a succession of calls to piResultTy (which is + -- asymptotically costly as the number of arguments increases) + go (AppTy fun arg) args = go fun (arg:args) + go fun args = piResultTys (tcTypeKind fun) args + +tcTypeKind ty@(ForAllTy (Bndr tv _) _) + | isTyVar tv -- See Note [Weird typing rule for ForAllTy]. + = case occCheckExpand tvs k of -- We must make sure tv does not occur in kind + Just k' -> k' -- As it is already out of scope! + Nothing -> pprPanic "tcTypeKind" + (ppr ty $$ ppr k $$ ppr tvs $$ ppr body) + | otherwise + = liftedTypeKind + where + (tvs, body) = splitTyVarForAllTys ty + k = tcTypeKind body + -------------------------- typeLiteralKind :: TyLit -> Kind |