diff options
| author | Simon Peyton Jones <simonpj@microsoft.com> | 2018-12-03 11:30:22 +0000 |
|---|---|---|
| committer | Simon Peyton Jones <simonpj@microsoft.com> | 2018-12-03 13:42:40 +0000 |
| commit | 03d4852658e1b7407abb4da84b1b03bfa6f6db3b (patch) | |
| tree | f957494f1aa0933f71a783c5e006f2f03d807a58 | |
| parent | 89d80921d9328499ffca9877e7dea540350be9c1 (diff) | |
| download | haskell-03d4852658e1b7407abb4da84b1b03bfa6f6db3b.tar.gz | |
Introduce tcTypeKind, and use it
In the type checker Constraint and * are distinct; and the function
that takes the kind of a type should respect that distinction
(Trac #15971).
This patch implements the change:
* Introduce Type.tcTypeKind, and use it throughout the type
inference engine
* Add new Note [Kinding rules for types] for the kinding
rules, especially for foralls.
* Redefine
isPredTy ty = tcIsConstraintKind (tcTypeKind ty)
(it had a much more complicated definition before)
Some miscellaneous refactoring
* Get rid of TyCoRep.isTYPE, Kind.isTYPEApp,
in favour of TyCoRep.kindRep, kindRep_maybe
* Rename Type.getRuntimeRepFromKind_maybe
to getRuntimeRep_maybe
I did some spot-checks on compiler perf, and it really doesn't
budge (as expected).
27 files changed, 304 insertions, 313 deletions
diff --git a/compiler/typecheck/ClsInst.hs b/compiler/typecheck/ClsInst.hs index c777c4b381..1b6ab12d0f 100644 --- a/compiler/typecheck/ClsInst.hs +++ b/compiler/typecheck/ClsInst.hs @@ -459,7 +459,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] @@ -472,7 +472,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 623d465e63..144b315bed 100644 --- a/compiler/typecheck/FamInst.hs +++ b/compiler/typecheck/FamInst.hs @@ -187,8 +187,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 afc6370c17..284d6a95d3 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) @@ -581,15 +581,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 46e5d821b4..dce9a10aff 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 e2a314c6a2..4bbb42d4b3 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) @@ -788,7 +788,7 @@ deriveTyData tvs tc tc_args mb_deriv_strat deriv_pred -- See Note [tc_args and tycon arity] (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] @@ -828,9 +828,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 b026f1d68c..ba45e09dc5 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 cfd364fb47..df307f240c 100644 --- a/compiler/typecheck/TcErrors.hs +++ b/compiler/typecheck/TcErrors.hs @@ -38,7 +38,7 @@ import HsBinds ( PatSynBind(..) ) import Name import RdrName ( lookupGlobalRdrEnv, lookupGRE_Name, GlobalRdrEnv , mkRdrUnqual, isLocalGRE, greSrcSpan ) -import PrelNames ( typeableClassName, hasKey, liftedRepDataConKey, tYPETyConKey ) +import PrelNames ( typeableClassName ) import Id import Var import VarSet @@ -603,7 +603,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 @@ -1177,7 +1177,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 @@ -1500,9 +1500,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 {} @@ -1750,7 +1750,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 @@ -1919,12 +1919,10 @@ misMatchMsg ct oriented ty1 ty2 -- These next two cases are when we're about to report, e.g., that -- 'LiftedRep doesn't match 'VoidRep. Much better just to say -- lifted vs. unlifted - | Just (tc1, []) <- splitTyConApp_maybe ty1 - , tc1 `hasKey` liftedRepDataConKey + | isLiftedRuntimeRep ty1 = lifted_vs_unlifted - | Just (tc2, []) <- splitTyConApp_maybe ty2 - , tc2 `hasKey` liftedRepDataConKey + | isLiftedRuntimeRep ty2 = lifted_vs_unlifted | otherwise -- So now we have Nothing or (Just IsSwapped) @@ -2060,14 +2058,13 @@ mkExpectedActualMsg ty1 ty2 ct@(TypeEqOrigin { uo_actual = act kind_desc | tcIsConstraintKind exp = text "a constraint" -- TYPE t0 - | Just (tc, [arg]) <- tcSplitTyConApp_maybe exp - , tc `hasKey` tYPETyConKey - , tcIsTyVarTy arg = sdocWithDynFlags $ \dflags -> - if gopt Opt_PrintExplicitRuntimeReps dflags - then text "kind" <+> quotes (ppr exp) - else text "a type" + | Just arg <- kindRep_maybe exp + , tcIsTyVarTy arg = sdocWithDynFlags $ \dflags -> + if gopt Opt_PrintExplicitRuntimeReps dflags + then text "kind" <+> quotes (ppr exp) + else text "a type" - | otherwise = text "kind" <+> quotes (ppr exp) + | otherwise = text "kind" <+> quotes (ppr exp) num_args_msg = case level of KindLevel @@ -2520,7 +2517,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 9eaead5935..8afcc8b666 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) @@ -1347,7 +1347,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 16cee703b8..6834af9f41 100644 --- a/compiler/typecheck/TcHsSyn.hs +++ b/compiler/typecheck/TcHsSyn.hs @@ -1039,7 +1039,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 4a4d49b81e..3b36281d4a 100644 --- a/compiler/typecheck/TcHsType.hs +++ b/compiler/typecheck/TcHsType.hs @@ -507,7 +507,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 @@ -520,17 +520,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.) @@ -587,7 +587,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 @@ -745,7 +745,7 @@ tc_hs_type mode rn_ty@(HsSumTy _ hs_tys) exp_kind = do { let arity = length hs_tys ; arg_kinds <- mapM (\_ -> newOpenTypeKind) hs_tys ; tau_tys <- zipWithM (tc_lhs_type mode) hs_tys arg_kinds - ; let arg_reps = map getRuntimeRepFromKind arg_kinds + ; let arg_reps = map kindRep arg_kinds arg_tys = arg_reps ++ tau_tys ; checkExpectedKind rn_ty (mkTyConApp (sumTyCon arity) arg_tys) @@ -872,7 +872,7 @@ finish_tuple rn_ty tup_sort tau_tys tau_kinds exp_kind ; checkExpectedKind rn_ty (mkTyConApp tycon arg_tys) res_kind exp_kind } where arity = length tau_tys - tau_reps = map getRuntimeRepFromKind tau_kinds + tau_reps = map kindRep tau_kinds res_kind = case tup_sort of UnboxedTuple -> unboxedTupleKind tau_reps BoxedTuple -> liftedTypeKind @@ -897,7 +897,7 @@ tcInferApps :: TcTyMode -> TcKind -- ^ Function kind (zonked) -> [LHsType GhcRn] -- ^ Args -> TcM (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] @@ -1079,7 +1079,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 0833b3329e..277e3249d4 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 3500b72a54..1516480789 100644 --- a/compiler/typecheck/TcMType.hs +++ b/compiler/typecheck/TcMType.hs @@ -684,7 +684,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) } newFmvTyVar :: TcType -> TcM TcTyVar -- Very like newMetaTyVar, except sets mtv_tclvl to one less @@ -697,7 +697,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 @@ -785,8 +785,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 @@ -2190,4 +2190,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 19ec6de622..ba3603fb42 100644 --- a/compiler/typecheck/TcPat.hs +++ b/compiler/typecheck/TcPat.hs @@ -351,7 +351,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 4942a8be83..ea1f483268 100644 --- a/compiler/typecheck/TcPatSyn.hs +++ b/compiler/typecheck/TcPatSyn.hs @@ -193,8 +193,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 2250f725d0..b13ae21b20 100644 --- a/compiler/typecheck/TcRnDriver.hs +++ b/compiler/typecheck/TcRnDriver.hs @@ -2415,7 +2415,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 ad3122badc..205a2bda03 100644 --- a/compiler/typecheck/TcRnTypes.hs +++ b/compiler/typecheck/TcRnTypes.hs @@ -1700,7 +1700,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. @@ -1723,7 +1723,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 ac283fad7c..4e8fe3b6e4 100644 --- a/compiler/typecheck/TcSimplify.hs +++ b/compiler/typecheck/TcSimplify.hs @@ -2121,7 +2121,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 @@ -2335,7 +2335,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 d3e146434f..7e34dae005 100644 --- a/compiler/typecheck/TcSplice.hs +++ b/compiler/typecheck/TcSplice.hs @@ -1199,7 +1199,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 @@ -1639,7 +1639,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 @@ -1944,7 +1944,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 c097d50ab3..eda86f9277 100644 --- a/compiler/typecheck/TcTyClsDecls.hs +++ b/compiler/typecheck/TcTyClsDecls.hs @@ -2441,8 +2441,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 @@ -2962,8 +2962,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 df1ec91cf2..90d4408126 100644 --- a/compiler/typecheck/TcType.hs +++ b/compiler/typecheck/TcType.hs @@ -122,7 +122,7 @@ module TcType ( -------------------------------- -- Rexported from Kind - Kind, typeKind, + Kind, typeKind, tcTypeKind, liftedTypeKind, constraintKind, isLiftedTypeKind, isUnliftedTypeKind, classifiesTypeWithValues, @@ -1296,7 +1296,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 @@ -1306,12 +1306,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/. @@ -1563,7 +1563,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: @@ -1714,8 +1714,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. @@ -1732,8 +1732,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 @@ -1970,8 +1970,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/TcTypeable.hs b/compiler/typecheck/TcTypeable.hs index 90a4a836d1..1fe2c68ae0 100644 --- a/compiler/typecheck/TcTypeable.hs +++ b/compiler/typecheck/TcTypeable.hs @@ -28,7 +28,6 @@ import TysWiredIn ( tupleTyCon, sumTyCon, runtimeRepTyCon import Name import Id import Type -import Kind ( isTYPEApp ) import TyCon import DataCon import Module @@ -430,7 +429,7 @@ typeIsTypeable :: Type -> Bool typeIsTypeable ty | Just ty' <- coreView ty = typeIsTypeable ty' typeIsTypeable ty - | Just _ <- isTYPEApp ty = True + | isJust (kindRep_maybe ty) = True typeIsTypeable (TyVarTy _) = True typeIsTypeable (AppTy a b) = typeIsTypeable a && typeIsTypeable b typeIsTypeable (FunTy a b) = typeIsTypeable a && typeIsTypeable b @@ -549,11 +548,15 @@ mkKindRepRhs :: TypeableStuff mkKindRepRhs stuff@(Stuff {..}) in_scope = new_kind_rep where new_kind_rep k - -- We handle TYPE separately to make it clear to consumers - -- (e.g. serializers) that there is a loop here (as - -- TYPE :: RuntimeRep -> TYPE 'LiftedRep) - | Just rr <- isTYPEApp k - = return $ nlHsDataCon kindRepTYPEDataCon `nlHsApp` nlHsDataCon rr + -- We handle (TYPE LiftedRep) etc separately to make it + -- clear to consumers (e.g. serializers) that there is + -- a loop here (as TYPE :: RuntimeRep -> TYPE 'LiftedRep) + | not (tcIsConstraintKind k) -- Typeable respects the Constraint/* distinction + -- so do not follow the special case here + , Just arg <- kindRep_maybe k + , Just (tc, []) <- splitTyConApp_maybe arg + , Just dc <- isPromotedDataCon_maybe tc + = return $ nlHsDataCon kindRepTYPEDataCon `nlHsApp` nlHsDataCon dc new_kind_rep (TyVarTy v) | Just idx <- lookupCME in_scope v diff --git a/compiler/typecheck/TcUnify.hs b/compiler/typecheck/TcUnify.hs index fd661c9b0e..f51c7241a8 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) } @@ -1639,10 +1639,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 a3f4e2f20b..f82e394590 100644 --- a/compiler/typecheck/TcValidity.hs +++ b/compiler/typecheck/TcValidity.hs @@ -319,7 +319,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 @@ -382,7 +382,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 @@ -403,7 +403,7 @@ checkTySynRhs ctxt ty | otherwise = return () where - actual_kind = typeKind ty + actual_kind = tcTypeKind ty {- Note [Higher rank types] @@ -506,7 +506,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) diff --git a/compiler/types/Kind.hs b/compiler/types/Kind.hs index f88bbe1c0d..17c8041821 100644 --- a/compiler/types/Kind.hs +++ b/compiler/types/Kind.hs @@ -7,7 +7,6 @@ module Kind ( -- ** Predicates on Kinds isLiftedTypeKind, isUnliftedTypeKind, - isTYPEApp, isConstraintKindCon, classifiesTypeWithValues, @@ -18,9 +17,7 @@ module Kind ( import GhcPrelude -import {-# SOURCE #-} Type ( coreView - , splitTyConApp_maybe ) -import {-# SOURCE #-} DataCon ( DataCon ) +import {-# SOURCE #-} Type ( coreView ) import TyCoRep import TyCon @@ -28,6 +25,7 @@ import PrelNames import Outputable import Util +import Data.Maybe( isJust ) {- ************************************************************************ @@ -64,15 +62,6 @@ during type inference. isConstraintKindCon :: TyCon -> Bool isConstraintKindCon tc = tyConUnique tc == constraintKindTyConKey -isTYPEApp :: Kind -> Maybe DataCon -isTYPEApp (TyConApp tc args) - | tc `hasKey` tYPETyConKey - , [arg] <- args - , Just (tc, []) <- splitTyConApp_maybe arg - , Just dc <- isPromotedDataCon_maybe tc - = Just dc -isTYPEApp _ = Nothing - -- | Tests whether the given kind (which should look like @TYPE x@) -- is something other than a constructor tree (that is, constructors at every node). -- E.g. True of TYPE k, TYPE (F Int) @@ -92,12 +81,7 @@ isKindLevPoly k = ASSERT2( isLiftedTypeKind k || _is_type, ppr k ) go CastTy{} = True go CoercionTy{} = True - _is_type - | TyConApp typ [_] <- k - = typ `hasKey` tYPETyConKey - | otherwise - = False - + _is_type = classifiesTypeWithValues k ----------------------------------------- -- Subkinding @@ -110,4 +94,4 @@ isKindLevPoly k = ASSERT2( isLiftedTypeKind k || _is_type, ppr k ) -- like *, #, TYPE Lifted, TYPE v, Constraint. classifiesTypeWithValues :: Kind -> Bool -- ^ True of any sub-kind of OpenTypeKind -classifiesTypeWithValues = isTYPE (const True) +classifiesTypeWithValues k = isJust (kindRep_maybe k) diff --git a/compiler/types/TyCoRep.hs b/compiler/types/TyCoRep.hs index db82deb470..c7592c5ffd 100644 --- a/compiler/types/TyCoRep.hs +++ b/compiler/types/TyCoRep.hs @@ -44,8 +44,10 @@ module TyCoRep ( mkForAllTy, mkTyCoPiTy, mkTyCoPiTys, mkPiTys, - isTYPE, + + kindRep_maybe, kindRep, isLiftedTypeKind, isUnliftedTypeKind, + isLiftedRuntimeRep, isUnliftedRuntimeRep, isRuntimeRepTy, isRuntimeRepVar, sameVis, @@ -857,40 +859,61 @@ mkTyConTy tycon = TyConApp tycon [] Some basic functions, put here to break loops eg with the pretty printer -} --- | If a type is @'TYPE' r@ for some @r@, run the predicate argument on @r@. --- Otherwise, return 'False'. --- --- This function does not distinguish between 'Constraint' and 'Type'. For a --- version which does distinguish between the two, see 'tcIsTYPE'. -isTYPE :: ( Type -- the single argument to TYPE; not a synonym - -> Bool ) -- what to return - -> Kind -> Bool -isTYPE f ki | Just ki' <- coreView ki = isTYPE f ki' -isTYPE f (TyConApp tc [arg]) - | tc `hasKey` tYPETyConKey - = go arg - where - go ty | Just ty' <- coreView ty = go ty' - go ty = f ty -isTYPE _ _ = False +-- | Extract the RuntimeRep classifier of a type from its kind. For example, +-- @kindRep * = LiftedRep@; Panics if this is not possible. +-- Treats * and Constraint as the same +kindRep :: HasDebugCallStack => Kind -> Type +kindRep k = case kindRep_maybe k of + Just r -> r + Nothing -> pprPanic "kindRep" (ppr k) + +-- | Given a kind (TYPE rr), extract its RuntimeRep classifier rr. +-- For example, @kindRep_maybe * = Just LiftedRep@ +-- Returns 'Nothing' if the kind is not of form (TYPE rr) +-- Treats * and Constraint as the same +kindRep_maybe :: HasDebugCallStack => Kind -> Maybe Type +kindRep_maybe kind + | Just kind' <- coreView kind = kindRep_maybe kind' + | TyConApp tc [arg] <- kind + , tc `hasKey` tYPETyConKey = Just arg + | otherwise = Nothing -- | This version considers Constraint to be the same as *. Returns True -- if the argument is equivalent to Type/Constraint and False otherwise. -- See Note [Kind Constraint and kind Type] isLiftedTypeKind :: Kind -> Bool -isLiftedTypeKind = isTYPE is_lifted - where - is_lifted (TyConApp lifted_rep []) = lifted_rep `hasKey` liftedRepDataConKey - is_lifted _ = False +isLiftedTypeKind kind + = case kindRep_maybe kind of + Just rep -> isLiftedRuntimeRep rep + Nothing -> False -- | Returns True if the kind classifies unlifted types and False otherwise. -- Note that this returns False for levity-polymorphic kinds, which may -- be specialized to a kind that classifies unlifted types. isUnliftedTypeKind :: Kind -> Bool -isUnliftedTypeKind = isTYPE is_unlifted - where - is_unlifted (TyConApp rr _args) = elem (getUnique rr) unliftedRepDataConKeys - is_unlifted _ = False +isUnliftedTypeKind kind + = case kindRep_maybe kind of + Just rep -> isUnliftedRuntimeRep rep + Nothing -> False + +isLiftedRuntimeRep, isUnliftedRuntimeRep :: Type -> Bool +-- isLiftedRuntimeRep is true of LiftedRep :: RuntimeRep +-- Similarly isUnliftedRuntimeRep +isLiftedRuntimeRep rep + | Just rep' <- coreView rep = isLiftedRuntimeRep rep' + | TyConApp rr_tc args <- rep + , rr_tc `hasKey` liftedRepDataConKey = ASSERT( null args ) True + | otherwise = False + +isUnliftedRuntimeRep rep + | Just rep' <- coreView rep = isUnliftedRuntimeRep rep' + | TyConApp rr_tc args <- rep + , isUnliftedRuntimeRepTyCon rr_tc = ASSERT( null args ) True + | otherwise = False + +isUnliftedRuntimeRepTyCon :: TyCon -> Bool +isUnliftedRuntimeRepTyCon rr_tc + = elem (getUnique rr_tc) unliftedRepDataConKeys -- | Is this the type 'RuntimeRep'? isRuntimeRepTy :: Type -> Bool diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs index e489551aa4..0fff81c2ab 100644 --- a/compiler/types/Type.hs +++ b/compiler/types/Type.hs @@ -53,7 +53,7 @@ module Type ( mkStrLitTy, isStrLitTy, isLitTy, - getRuntimeRep_maybe, getRuntimeRepFromKind_maybe, + getRuntimeRep_maybe, kindRep_maybe, kindRep, mkCastTy, mkCoercionTy, splitCastTy_maybe, @@ -126,13 +126,13 @@ module Type ( isPrimitiveType, isStrictType, isRuntimeRepTy, isRuntimeRepVar, isRuntimeRepKindedTy, dropRuntimeRepArgs, - getRuntimeRep, getRuntimeRepFromKind, + getRuntimeRep, -- * Main data types representing Kinds Kind, -- ** Finding the kind of a type - typeKind, isTypeLevPoly, resultIsLevPoly, + typeKind, tcTypeKind, isTypeLevPoly, resultIsLevPoly, tcIsLiftedTypeKind, tcIsConstraintKind, tcReturnsConstraintKind, -- ** Common Kind @@ -246,7 +246,8 @@ import Class import TyCon import TysPrim import {-# SOURCE #-} TysWiredIn ( listTyCon, typeNatKind, unitTy - , typeSymbolKind, liftedTypeKind ) + , typeSymbolKind, liftedTypeKind + , constraintKind ) import PrelNames import CoAxiom import {-# SOURCE #-} Coercion( mkNomReflCo, mkGReflCo, mkReflCo @@ -336,12 +337,14 @@ import Control.Monad ( guard ) Note [coreView vs tcView] ~~~~~~~~~~~~~~~~~~~~~~~~~ -So far as the typechecker is concerned, 'Constraint' and 'TYPE LiftedRep' are distinct kinds. +So far as the typechecker is concerned, 'Constraint' and 'TYPE +LiftedRep' are distinct kinds. But in Core these two are treated as identical. -We implement this by making 'coreView' convert 'Constraint' to 'TYPE LiftedRep' on the fly. -The function tcView (used in the type checker) does not do this. +We implement this by making 'coreView' convert 'Constraint' to 'TYPE +LiftedRep' on the fly. The function tcView (used in the type checker) +does not do this. See also Trac #11715, which tracks removing this inconsistency. @@ -1240,22 +1243,6 @@ newTyConInstRhs tycon tys CastTy ~~~~~~ A casted type has its *kind* casted into something new. - -Note [Weird typing rule for ForAllTy] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Here is the (truncated) typing rule for the dependent ForAllTy: - -inner : kind ------------------------------------- -ForAllTy (Bndr tyvar vis) inner : kind - -inner : TYPE r ------------------------------------- -ForAllTy (Bndr covar vis) inner : TYPE - -Note that when inside the binder is a tyvar, neither the inner type nor for -ForAllTy itself have to have kind *! But, it means that we should push any kind -casts through the ForAllTy. The only trouble is avoiding capture. -} splitCastTy_maybe :: Type -> Maybe (Type, Coercion) @@ -1764,27 +1751,6 @@ When treated as a user type, predicates are invisible and are implicitly instantiated; but coercion types, and non-pred evidence types, are just regular old types. -Note [isPredTy complications] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -You would think that we could define - isPredTy ty = isConstraintKind (typeKind ty) -But there are a number of complications: - -* isPredTy is used when printing types, which can happen in debug - printing during type checking of not-fully-zonked types. So it's - not cool to say isConstraintKind (typeKind ty) because, absent - zonking, the type might be ill-kinded, and typeKind crashes. Hence the - rather tiresome story here - -* isPredTy must return "True" to *unlifted* coercions, such as (t1 ~# t2) - and (t1 ~R# t2), which are not of kind Constraint! Currently they are - of kind #. - -* If we do form the type '(C a => C [a]) => blah', then we'd like to - print it as such. But that means that isPredTy must return True for - (C a => C [a]). Admittedly that type is illegal in Haskell, but we - want to print it nicely in error messages. - Note [Evidence for quantified constraints] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ The superclass mechanism in TcCanonical.makeSuperClasses risks @@ -1830,11 +1796,9 @@ tcIsConstraintKind ty -- treats them as the same type, see 'isLiftedTypeKind'. tcIsLiftedTypeKind :: Kind -> Bool tcIsLiftedTypeKind ty - | Just (type_tc, [arg]) <- tcSplitTyConApp_maybe ty - , type_tc `hasKey` tYPETyConKey - , Just (lifted_rep_tc, args) <- tcSplitTyConApp_maybe arg - , lifted_rep_tc `hasKey` liftedRepDataConKey - = ASSERT2( null args, ppr ty ) True + | Just (tc, [arg]) <- tcSplitTyConApp_maybe ty -- Note: tcSplit here + , tc `hasKey` tYPETyConKey + = isLiftedRuntimeRep arg | otherwise = False @@ -1868,57 +1832,6 @@ isCoVarType ty = True isCoVarType _ = False --- | Is the type suitable to classify a given/wanted in the typechecker? -isPredTy :: Type -> Bool --- See Note [isPredTy complications] --- NB: /not/ true of (t1 ~# t2) or (t1 ~R# t2) --- See Note [Types for coercions, predicates, and evidence] -isPredTy ty = go ty [] - where - go :: Type -> [KindOrType] -> Bool - -- Since we are looking at the kind, - -- no need to look through type synonyms - go (AppTy ty1 ty2) args = go ty1 (ty2 : args) - go (TyVarTy tv) args = go_k (tyVarKind tv) args - go (TyConApp tc tys) args = ASSERT( null args ) -- TyConApp invariant - go_k (tyConKind tc) tys - go (FunTy arg res) [] - | isPredTy arg = isPredTy res -- (Eq a => C a) - | otherwise = False -- (Int -> Bool) - go (ForAllTy _ ty) [] = go ty [] - go (CastTy _ co) args = go_k (pSnd (coercionKind co)) args - go _ _ = False - - go_k :: Kind -> [KindOrType] -> Bool - -- True <=> ('k' applied to 'kts') = Constraint - go_k k [] = tcIsConstraintKind k - go_k k (arg:args) = case piResultTy_maybe k arg of - Just k' -> go_k k' args - Nothing -> WARN( True, text "isPredTy" <+> ppr ty ) - False - -- This last case shouldn't happen under most circumstances. It can - -- occur if we call isPredTy during kind checking, especially if one - -- of the following happens: - -- - -- 1. There is actually a kind error. Example in which this showed up: - -- polykinds/T11399 - -- - -- 2. A type constructor application appears to be oversaturated. An - -- example of this occurred in GHC Trac #13187: - -- - -- {-# LANGUAGE PolyKinds #-} - -- type Const a b = b - -- f :: Const Int (,) Bool Char -> Char - -- - -- We call isPredTy (Const k1 k2 Int (,) Bool Char - -- where k1,k2 are unification variables that have been - -- unified to *, and (*->*->*) resp, /but not zonked/. - -- This shows that isPredTy can report a false negative - -- if a constraint is similarly oversaturated, but - -- it's hard to do better than isPredTy currently does without - -- zonking, so we punt on such cases for now. This only happens - -- during debug-printing, so it doesn't matter. - isClassPred, isEqPred, isNomEqPred, isIPPred :: PredType -> Bool isClassPred ty = case tyConAppTyCon_maybe ty of Just tyCon | isClassTyCon tyCon -> True @@ -2350,10 +2263,9 @@ isLiftedType_maybe :: HasDebugCallStack => Type -> Maybe Bool isLiftedType_maybe ty = go (getRuntimeRep ty) where go rr | Just rr' <- coreView rr = go rr' - go (TyConApp lifted_rep []) - | lifted_rep `hasKey` liftedRepDataConKey = Just True - go (TyConApp {}) = Just False -- everything else is unlifted - go _ = Nothing -- levity polymorphic + | isLiftedRuntimeRep rr = Just True + | TyConApp {} <- rr = Just False -- Everything else is unlifted + | otherwise = Nothing -- levity polymorphic -- | See "Type#type_classification" for what an unlifted type is. -- Panics on levity polymorphic types. @@ -2385,7 +2297,7 @@ dropRuntimeRepArgs = dropWhile isRuntimeRepKindedTy -- possible. getRuntimeRep_maybe :: HasDebugCallStack => Type -> Maybe Type -getRuntimeRep_maybe = getRuntimeRepFromKind_maybe . typeKind +getRuntimeRep_maybe = kindRep_maybe . typeKind -- | Extract the RuntimeRep classifier of a type. For instance, -- @getRuntimeRep_maybe Int = LiftedRep@. Panics if this is not possible. @@ -2395,30 +2307,6 @@ getRuntimeRep ty Just r -> r Nothing -> pprPanic "getRuntimeRep" (ppr ty <+> dcolon <+> ppr (typeKind ty)) --- | Extract the RuntimeRep classifier of a type from its kind. For example, --- @getRuntimeRepFromKind * = LiftedRep@; Panics if this is not possible. -getRuntimeRepFromKind :: HasDebugCallStack - => Type -> Type -getRuntimeRepFromKind k = - case getRuntimeRepFromKind_maybe k of - Just r -> r - Nothing -> pprPanic "getRuntimeRepFromKind" - (ppr k <+> dcolon <+> ppr (typeKind k)) - --- | Extract the RuntimeRep classifier of a type from its kind. For example, --- @getRuntimeRepFromKind * = LiftedRep@; Returns 'Nothing' if this is not --- possible. -getRuntimeRepFromKind_maybe :: HasDebugCallStack - => Type -> Maybe Type -getRuntimeRepFromKind_maybe = go - where - go k | Just k' <- coreView k = go k' - go k - | Just (_tc, [arg]) <- splitTyConApp_maybe k - = ASSERT2( _tc `hasKey` tYPETyConKey, ppr k ) - Just arg - go _ = Nothing - isUnboxedTupleType :: Type -> Bool isUnboxedTupleType ty = tyConAppTyCon (getRuntimeRep ty) `hasKey` tupleRepDataConKey @@ -2752,34 +2640,130 @@ nonDetCmpTc tc1 tc2 The kind of a type * * ************************************************************************ + +Note [typeKind vs tcTypeKind] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +We have two functions to get the kind of a type + + * typeKind ignores the distinction between Constraint and * + * tcTypeKind respects the distinction between Constraint and * + +tcTypeKind is used by the type inference engine, for which Constraint +and * are different; after that we use typeKind. + +See also Note [coreView vs tcView] + +Note [Kinding rules for types] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +In typeKind we consider Constraint and (TYPE LiftedRep) to be identical. +We then have + + t1 : TYPE rep1 + t2 : TYPE rep2 + (FUN) ---------------- + t1 -> t2 : Type + + ty : TYPE rep + `a` is not free in rep +(FORALL) ----------------------- + forall a. ty : TYPE rep + +In tcTypeKind we consider Constraint and (TYPE LiftedRep) to be distinct: + + t1 : TYPE rep1 + t2 : TYPE rep2 + (FUN) ---------------- + t1 -> t2 : Type + + t1 : Constraint + t2 : TYPE rep + (PRED1) ---------------- + t1 => t2 : Type + + t1 : Constraint + t2 : Constraint + (PRED2) --------------------- + t1 => t2 : Constraint + + ty : TYPE rep + `a` is not free in rep +(FORALL1) ----------------------- + forall a. ty : TYPE rep + + ty : Constraint +(FORALL2) ------------------------- + forall a. ty : Constraint + +Note that: +* The only way we distinguish '->' from '=>' is by the fact + that the argument is a PredTy. Both are FunTys -} +----------------------------- 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 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! + +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 {}) + = case occCheckExpand tvs body_kind 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) + (ppr ty $$ ppr tvs $$ ppr body <+> dcolon <+> ppr body_kind) + where + (tvs, body) = splitTyVarForAllTys ty + body_kind = typeKind body + +----------------------------- +tcTypeKind :: HasDebugCallStack => Type -> Kind +tcTypeKind (TyConApp tc tys) = piResultTys (tyConKind tc) tys +tcTypeKind (LitTy l) = typeLiteralKind l +tcTypeKind (TyVarTy tyvar) = tyVarKind tyvar +tcTypeKind (CastTy _ty co) = pSnd $ coercionKind co +tcTypeKind (CoercionTy co) = coercionType co + +tcTypeKind (FunTy arg res) + | isPredTy arg && isPredTy res = constraintKind + | otherwise = liftedTypeKind + +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 {}) + | tcIsConstraintKind body_kind + = constraintKind + + | otherwise + = case occCheckExpand tvs body_kind 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 tvs $$ ppr body <+> dcolon <+> ppr body_kind) 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 + body_kind = tcTypeKind body + + +isPredTy :: Type -> Bool +-- See Note [Types for coercions, predicates, and evidence] +isPredTy ty = tcIsConstraintKind (tcTypeKind ty) -------------------------- typeLiteralKind :: TyLit -> Kind |