Commit 03d48526 authored by Simon Peyton Jones's avatar Simon Peyton Jones

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).
parent 89d80921
...@@ -459,7 +459,7 @@ doTyApp :: Class -> Type -> Type -> KindOrType -> TcM ClsInstResult ...@@ -459,7 +459,7 @@ doTyApp :: Class -> Type -> Type -> KindOrType -> TcM ClsInstResult
-- (Typeable f, Typeable Int, Typeable Char) --> (after some simp. steps) -- (Typeable f, Typeable Int, Typeable Char) --> (after some simp. steps)
-- Typeable f -- Typeable f
doTyApp clas ty f tk doTyApp clas ty f tk
| isForAllTy (typeKind f) | isForAllTy (tcTypeKind f)
= return NoInstance -- We can't solve until we know the ctr. = return NoInstance -- We can't solve until we know the ctr.
| otherwise | otherwise
= return $ OneInst { cir_new_theta = map (mk_typeable_pred clas) [f, tk] = return $ OneInst { cir_new_theta = map (mk_typeable_pred clas) [f, tk]
...@@ -472,7 +472,7 @@ doTyApp clas ty f tk ...@@ -472,7 +472,7 @@ doTyApp clas ty f tk
-- Emit a `Typeable` constraint for the given type. -- Emit a `Typeable` constraint for the given type.
mk_typeable_pred :: Class -> Type -> PredType 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 -- Typeable is implied by KnownNat/KnownSymbol. In the case of a type literal
-- we generate a sub-goal for the appropriate class. -- we generate a sub-goal for the appropriate class.
......
...@@ -187,8 +187,8 @@ newFamInst flavor axiom@(CoAxiom { co_ax_tc = fam_tc }) ...@@ -187,8 +187,8 @@ newFamInst flavor axiom@(CoAxiom { co_ax_tc = fam_tc })
, fi_rhs = rhs' , fi_rhs = rhs'
, fi_axiom = axiom }) } , fi_axiom = axiom }) }
where where
lhs_kind = typeKind (mkTyConApp fam_tc lhs) lhs_kind = tcTypeKind (mkTyConApp fam_tc lhs)
rhs_kind = typeKind rhs rhs_kind = tcTypeKind rhs
tcv_set = mkVarSet (tvs ++ cvs) tcv_set = mkVarSet (tvs ++ cvs)
pp_ax = pprCoAxiom axiom pp_ax = pprCoAxiom axiom
CoAxBranch { cab_tvs = tvs CoAxBranch { cab_tvs = tvs
......
...@@ -305,7 +305,7 @@ instTyVarsWith orig tvs tys ...@@ -305,7 +305,7 @@ instTyVarsWith orig tvs tys
; go (extendTCvSubst subst tv (ty `mkCastTy` co)) tvs tys } ; go (extendTCvSubst subst tv (ty `mkCastTy` co)) tvs tys }
where where
tv_kind = substTy subst (tyVarKind tv) tv_kind = substTy subst (tyVarKind tv)
ty_kind = typeKind ty ty_kind = tcTypeKind ty
go _ _ _ = pprPanic "instTysWith" (ppr tvs $$ ppr tys) go _ _ _ = pprPanic "instTysWith" (ppr tvs $$ ppr tys)
...@@ -581,15 +581,15 @@ mkHEqBoxTy :: TcCoercion -> Type -> Type -> TcM Type ...@@ -581,15 +581,15 @@ mkHEqBoxTy :: TcCoercion -> Type -> Type -> TcM Type
mkHEqBoxTy co ty1 ty2 mkHEqBoxTy co ty1 ty2
= return $ = return $
mkTyConApp (promoteDataCon heqDataCon) [k1, k2, ty1, ty2, mkCoercionTy co] mkTyConApp (promoteDataCon heqDataCon) [k1, k2, ty1, ty2, mkCoercionTy co]
where k1 = typeKind ty1 where k1 = tcTypeKind ty1
k2 = typeKind ty2 k2 = tcTypeKind ty2
-- | This takes @a ~# b@ and returns @a ~ b@. -- | This takes @a ~# b@ and returns @a ~ b@.
mkEqBoxTy :: TcCoercion -> Type -> Type -> TcM Type mkEqBoxTy :: TcCoercion -> Type -> Type -> TcM Type
mkEqBoxTy co ty1 ty2 mkEqBoxTy co ty1 ty2
= return $ = return $
mkTyConApp (promoteDataCon eqDataCon) [k, ty1, ty2, mkCoercionTy co] mkTyConApp (promoteDataCon eqDataCon) [k, ty1, ty2, mkCoercionTy co]
where k = typeKind ty1 where k = tcTypeKind ty1
{- {-
************************************************************************ ************************************************************************
......
...@@ -1319,8 +1319,8 @@ can_eq_app ev s1 t1 s2 t2 ...@@ -1319,8 +1319,8 @@ can_eq_app ev s1 t1 s2 t2
; canEqNC evar_s NomEq s1 s2 } ; canEqNC evar_s NomEq s1 s2 }
where where
s1k = typeKind s1 s1k = tcTypeKind s1
s2k = typeKind s2 s2k = tcTypeKind s2
k1 `mismatches` k2 k1 `mismatches` k2
= isForAllTy k1 && not (isForAllTy k2) = isForAllTy k1 && not (isForAllTy k2)
...@@ -1790,9 +1790,9 @@ canCFunEqCan ev fn tys fsk ...@@ -1790,9 +1790,9 @@ canCFunEqCan ev fn tys fsk
vcat [ text "Kind co:" <+> ppr kind_co vcat [ text "Kind co:" <+> ppr kind_co
, text "RHS:" <+> ppr fsk <+> dcolon <+> ppr (tyVarKind fsk) , text "RHS:" <+> ppr fsk <+> dcolon <+> ppr (tyVarKind fsk)
, text "LHS:" <+> hang (ppr (mkTyConApp fn tys)) , 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) , text "New LHS" <+> hang (ppr new_lhs)
2 (dcolon <+> ppr (typeKind new_lhs)) ] 2 (dcolon <+> ppr (tcTypeKind new_lhs)) ]
; (ev', new_co, new_fsk) ; (ev', new_co, new_fsk)
<- newFlattenSkolem flav (ctEvLoc ev) fn tys' <- newFlattenSkolem flav (ctEvLoc ev) fn tys'
; let xi = mkTyVarTy new_fsk `mkCastTy` kind_co ; let xi = mkTyVarTy new_fsk `mkCastTy` kind_co
...@@ -1882,7 +1882,7 @@ canEqTyVar ev eq_rel swapped tv1 ps_ty1 xi2 ps_xi2 ...@@ -1882,7 +1882,7 @@ canEqTyVar ev eq_rel swapped tv1 ps_ty1 xi2 ps_xi2
xi1 = mkTyVarTy tv1 xi1 = mkTyVarTy tv1
k1 = tyVarKind tv1 k1 = tyVarKind tv1
k2 = typeKind xi2 k2 = tcTypeKind xi2
loc = ctEvLoc ev loc = ctEvLoc ev
flav = ctEvFlavour ev flav = ctEvFlavour ev
...@@ -1936,7 +1936,7 @@ canEqTyVarHetero ev eq_rel tv1 co1 ki1 ps_tv1 xi2 ki2 ps_xi2 ...@@ -1936,7 +1936,7 @@ canEqTyVarHetero ev eq_rel tv1 co1 ki1 ps_tv1 xi2 ki2 ps_xi2
loc = ctev_loc ev loc = ctev_loc ev
role = eqRelRole eq_rel role = eqRelRole eq_rel
-- guaranteed that typeKind lhs == typeKind rhs -- guaranteed that tcTypeKind lhs == tcTypeKind rhs
canEqTyVarHomo :: CtEvidence canEqTyVarHomo :: CtEvidence
-> EqRel -> SwapFlag -> EqRel -> SwapFlag
-> TcTyVar -- lhs: tv1 -> TcTyVar -- lhs: tv1
...@@ -2288,7 +2288,7 @@ rewriteEqEvidence :: CtEvidence -- Old evidence :: olhs ~ orhs (not swap ...@@ -2288,7 +2288,7 @@ rewriteEqEvidence :: CtEvidence -- Old evidence :: olhs ~ orhs (not swap
-- or orhs ~ olhs (swapped) -- or orhs ~ olhs (swapped)
-> SwapFlag -> SwapFlag
-> TcType -> TcType -- New predicate nlhs ~ nrhs -> 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 -- lhs_co, of type :: nlhs ~ olhs
-> TcCoercion -- rhs_co, of type :: nrhs ~ orhs -> TcCoercion -- rhs_co, of type :: nrhs ~ orhs
-> TcS CtEvidence -- Of type nlhs ~ nrhs -> TcS CtEvidence -- Of type nlhs ~ nrhs
...@@ -2364,7 +2364,7 @@ unifyWanted :: CtLoc -> Role ...@@ -2364,7 +2364,7 @@ unifyWanted :: CtLoc -> Role
-- See Note [unifyWanted and unifyDerived] -- See Note [unifyWanted and unifyDerived]
-- The returned coercion's role matches the input parameter -- The returned coercion's role matches the input parameter
unifyWanted loc Phantom ty1 ty2 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) } ; return (mkPhantomCo kind_co ty1 ty2) }
unifyWanted loc role orig_ty1 orig_ty2 unifyWanted loc role orig_ty1 orig_ty2
......
...@@ -629,8 +629,8 @@ deriveStandalone (L loc (DerivDecl _ deriv_ty mbl_deriv_strat overlap_mode)) ...@@ -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` -- Perform an additional unification with the kind of the `via`
-- type and the result of the previous kind unification. -- type and the result of the previous kind unification.
Just (ViaStrategy via_ty) -> do Just (ViaStrategy via_ty) -> do
let via_kind = typeKind via_ty let via_kind = tcTypeKind via_ty
inst_ty_kind = typeKind inst_ty' inst_ty_kind = tcTypeKind inst_ty'
mb_match = tcUnifyTy inst_ty_kind via_kind mb_match = tcUnifyTy inst_ty_kind via_kind
checkTc (isJust mb_match) checkTc (isJust mb_match)
...@@ -788,7 +788,7 @@ deriveTyData tvs tc tc_args mb_deriv_strat deriv_pred ...@@ -788,7 +788,7 @@ deriveTyData tvs tc tc_args mb_deriv_strat deriv_pred
-- See Note [tc_args and tycon arity] -- See Note [tc_args and tycon arity]
(tc_args_to_keep, args_to_drop) (tc_args_to_keep, args_to_drop)
= splitAt n_args_to_keep tc_args = 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 -- Match up the kinds, and apply the resulting kind substitution
-- to the types. See Note [Unify kinds in deriving] -- to the types. See Note [Unify kinds in deriving]
...@@ -828,9 +828,9 @@ deriveTyData tvs tc tc_args mb_deriv_strat deriv_pred ...@@ -828,9 +828,9 @@ deriveTyData tvs tc tc_args mb_deriv_strat deriv_pred
-- type and the result of the previous kind unification. -- type and the result of the previous kind unification.
Just (ViaStrategy via_ty) -> do Just (ViaStrategy via_ty) -> do
let final_via_ty = via_ty let final_via_ty = via_ty
final_via_kind = typeKind final_via_ty final_via_kind = tcTypeKind final_via_ty
final_inst_ty_kind 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 via_match = tcUnifyTy final_inst_ty_kind final_via_kind
checkTc (isJust via_match) checkTc (isJust via_match)
......
...@@ -157,7 +157,7 @@ inferConstraintsDataConArgs inst_ty inst_tys ...@@ -157,7 +157,7 @@ inferConstraintsDataConArgs inst_ty inst_tys
is_generic = main_cls `hasKey` genClassKey is_generic = main_cls `hasKey` genClassKey
is_generic1 = main_cls `hasKey` gen1ClassKey is_generic1 = main_cls `hasKey` gen1ClassKey
-- is_functor_like: see Note [Inferring the instance context] -- 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 || is_generic1
get_gen1_constraints :: Class -> CtOrigin -> TypeOrKind -> Type get_gen1_constraints :: Class -> CtOrigin -> TypeOrKind -> Type
...@@ -191,7 +191,7 @@ inferConstraintsDataConArgs inst_ty inst_tys ...@@ -191,7 +191,7 @@ inferConstraintsDataConArgs inst_ty inst_tys
-- message which points out the kind mismatch. -- message which points out the kind mismatch.
-- See Note [Inferring the instance context] -- See Note [Inferring the instance context]
mk_functor_like_constraints orig t_or_k cls 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 ( [ mk_cls_pred orig t_or_k cls ty
, mkPredOrigin orig KindLevel , mkPredOrigin orig KindLevel
(mkPrimEqPred ki typeToTypeKind) ] (mkPrimEqPred ki typeToTypeKind) ]
...@@ -232,7 +232,7 @@ inferConstraintsDataConArgs inst_ty inst_tys ...@@ -232,7 +232,7 @@ inferConstraintsDataConArgs inst_ty inst_tys
where where
constrs constrs
| main_cls `hasKey` dataClassKey | 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 = [ mk_cls_pred deriv_origin t_or_k main_cls ty
| (t_or_k, ty) <- zip t_or_ks rep_tc_args] | (t_or_k, ty) <- zip t_or_ks rep_tc_args]
| otherwise | otherwise
......
...@@ -38,7 +38,7 @@ import HsBinds ( PatSynBind(..) ) ...@@ -38,7 +38,7 @@ import HsBinds ( PatSynBind(..) )
import Name import Name
import RdrName ( lookupGlobalRdrEnv, lookupGRE_Name, GlobalRdrEnv import RdrName ( lookupGlobalRdrEnv, lookupGRE_Name, GlobalRdrEnv
, mkRdrUnqual, isLocalGRE, greSrcSpan ) , mkRdrUnqual, isLocalGRE, greSrcSpan )
import PrelNames ( typeableClassName, hasKey, liftedRepDataConKey, tYPETyConKey ) import PrelNames ( typeableClassName )
import Id import Id
import Var import Var
import VarSet import VarSet
...@@ -603,7 +603,7 @@ reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_impl = implics }) ...@@ -603,7 +603,7 @@ reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_impl = implics })
is_user_type_error ct _ = isUserTypeErrorCt ct 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_homo_equality _ _ = False
is_equality _ (EqPred {}) = True is_equality _ (EqPred {}) = True
...@@ -1177,7 +1177,7 @@ mkHoleError tidy_simples ctxt ct@(CHoleCan { cc_hole = hole }) ...@@ -1177,7 +1177,7 @@ mkHoleError tidy_simples ctxt ct@(CHoleCan { cc_hole = hole })
where where
occ = holeOcc hole occ = holeOcc hole
hole_ty = ctEvPred (ctEvidence ct) hole_ty = ctEvPred (ctEvidence ct)
hole_kind = typeKind hole_ty hole_kind = tcTypeKind hole_ty
tyvars = tyCoVarsOfTypeList hole_ty tyvars = tyCoVarsOfTypeList hole_ty
hole_msg = case hole of hole_msg = case hole of
...@@ -1500,9 +1500,9 @@ mkEqErr1 ctxt ct -- Wanted or derived; ...@@ -1500,9 +1500,9 @@ mkEqErr1 ctxt ct -- Wanted or derived;
|| not (cty1 `pickyEqType` cty2) || not (cty1 `pickyEqType` cty2)
-> hang (text "When matching" <+> sub_what) -> hang (text "When matching" <+> sub_what)
2 (vcat [ ppr cty1 <+> dcolon <+> 2 (vcat [ ppr cty1 <+> dcolon <+>
ppr (typeKind cty1) ppr (tcTypeKind cty1)
, ppr cty2 <+> dcolon <+> , ppr cty2 <+> dcolon <+>
ppr (typeKind cty2) ]) ppr (tcTypeKind cty2) ])
_ -> text "When matching the kind of" <+> quotes (ppr cty1) _ -> text "When matching the kind of" <+> quotes (ppr cty1)
msg2 = case sub_o of msg2 = case sub_o of
TypeEqOrigin {} TypeEqOrigin {}
...@@ -1750,7 +1750,7 @@ mkTyVarEqErr' dflags ctxt report ct oriented tv1 co1 ty2 ...@@ -1750,7 +1750,7 @@ mkTyVarEqErr' dflags ctxt report ct oriented tv1 co1 ty2
-- Not an occurs check, because F is a type function. -- Not an occurs check, because F is a type function.
where where
Pair _ k1 = tcCoercionKind co1 Pair _ k1 = tcCoercionKind co1
k2 = typeKind ty2 k2 = tcTypeKind ty2
ty1 = mkTyVarTy tv1 ty1 = mkTyVarTy tv1
occ_check_expand = occCheckForErrors dflags tv1 ty2 occ_check_expand = occCheckForErrors dflags tv1 ty2
...@@ -1919,12 +1919,10 @@ misMatchMsg ct oriented ty1 ty2 ...@@ -1919,12 +1919,10 @@ misMatchMsg ct oriented ty1 ty2
-- These next two cases are when we're about to report, e.g., that -- These next two cases are when we're about to report, e.g., that
-- 'LiftedRep doesn't match 'VoidRep. Much better just to say -- 'LiftedRep doesn't match 'VoidRep. Much better just to say
-- lifted vs. unlifted -- lifted vs. unlifted
| Just (tc1, []) <- splitTyConApp_maybe ty1 | isLiftedRuntimeRep ty1
, tc1 `hasKey` liftedRepDataConKey
= lifted_vs_unlifted = lifted_vs_unlifted
| Just (tc2, []) <- splitTyConApp_maybe ty2 | isLiftedRuntimeRep ty2
, tc2 `hasKey` liftedRepDataConKey
= lifted_vs_unlifted = lifted_vs_unlifted
| otherwise -- So now we have Nothing or (Just IsSwapped) | otherwise -- So now we have Nothing or (Just IsSwapped)
...@@ -2060,14 +2058,13 @@ mkExpectedActualMsg ty1 ty2 ct@(TypeEqOrigin { uo_actual = act ...@@ -2060,14 +2058,13 @@ mkExpectedActualMsg ty1 ty2 ct@(TypeEqOrigin { uo_actual = act
kind_desc | tcIsConstraintKind exp = text "a constraint" kind_desc | tcIsConstraintKind exp = text "a constraint"
-- TYPE t0 -- TYPE t0
| Just (tc, [arg]) <- tcSplitTyConApp_maybe exp | Just arg <- kindRep_maybe exp
, tc `hasKey` tYPETyConKey , tcIsTyVarTy arg = sdocWithDynFlags $ \dflags ->
, tcIsTyVarTy arg = sdocWithDynFlags $ \dflags -> if gopt Opt_PrintExplicitRuntimeReps dflags
if gopt Opt_PrintExplicitRuntimeReps dflags then text "kind" <+> quotes (ppr exp)
then text "kind" <+> quotes (ppr exp) else text "a type"
else text "a type"
| otherwise = text "kind" <+> quotes (ppr exp) | otherwise = text "kind" <+> quotes (ppr exp)
num_args_msg = case level of num_args_msg = case level of
KindLevel KindLevel
...@@ -2520,7 +2517,7 @@ mk_dict_err ctxt@(CEC {cec_encl = implics}) (ct, (matches, unifiers, unsafe_over ...@@ -2520,7 +2517,7 @@ mk_dict_err ctxt@(CEC {cec_encl = implics}) (ct, (matches, unifiers, unsafe_over
, not (isTypeFamilyTyCon tc) , not (isTypeFamilyTyCon tc)
= hang (text "GHC can't yet do polykinded") = hang (text "GHC can't yet do polykinded")
2 (text "Typeable" <+> 2 (text "Typeable" <+>
parens (ppr ty <+> dcolon <+> ppr (typeKind ty))) parens (ppr ty <+> dcolon <+> ppr (tcTypeKind ty)))
| otherwise | otherwise
= empty = empty
......
...@@ -388,7 +388,7 @@ tcExpr expr@(OpApp fix arg1 op arg2) res_ty ...@@ -388,7 +388,7 @@ tcExpr expr@(OpApp fix arg1 op arg2) res_ty
-- The *result* type can have any kind (Trac #8739), -- The *result* type can have any kind (Trac #8739),
-- so we don't need to check anything for that -- so we don't need to check anything for that
; _ <- unifyKind (Just (XHsType $ NHsCoreTy arg2_sigma)) ; _ <- unifyKind (Just (XHsType $ NHsCoreTy arg2_sigma))
(typeKind arg2_sigma) liftedTypeKind (tcTypeKind arg2_sigma) liftedTypeKind
-- ignore the evidence. arg2_sigma must have type * or #, -- ignore the evidence. arg2_sigma must have type * or #,
-- because we know arg2_sigma -> or_res_ty is well-kinded -- because we know arg2_sigma -> or_res_ty is well-kinded
-- (because otherwise matchActualFunTys would fail) -- (because otherwise matchActualFunTys would fail)
...@@ -1347,7 +1347,7 @@ tcArgs fun orig_fun_ty fun_orig orig_args herald ...@@ -1347,7 +1347,7 @@ tcArgs fun orig_fun_ty fun_orig orig_args herald
-- substitution is kind-respecting -- substitution is kind-respecting
; traceTc "VTA" (vcat [ppr tv, debugPprType kind ; traceTc "VTA" (vcat [ppr tv, debugPprType kind
, debugPprType ty_arg , debugPprType ty_arg
, debugPprType (typeKind ty_arg) , debugPprType (tcTypeKind ty_arg)
, debugPprType inner_ty , debugPprType inner_ty
, debugPprType insted_ty ]) , debugPprType insted_ty ])
......
...@@ -771,7 +771,7 @@ flattenArgsNom :: CtEvidence -> TyCon -> [TcType] -> TcS ([Xi], [TcCoercion], Tc ...@@ -771,7 +771,7 @@ flattenArgsNom :: CtEvidence -> TyCon -> [TcType] -> TcS ([Xi], [TcCoercion], Tc
-- ctEvFlavour ev = Nominal -- ctEvFlavour ev = Nominal
-- and we want to flatten all at nominal role -- 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 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 -- For Derived constraints the returned coercion may be undefined
-- because flattening may use a Derived equality ([D] a ~ ty) -- because flattening may use a Derived equality ([D] a ~ ty)
...@@ -800,8 +800,8 @@ flattenArgsNom ev tc tys ...@@ -800,8 +800,8 @@ flattenArgsNom ev tc tys
Key invariants: Key invariants:
(F0) co :: xi ~ zonk(ty) (F0) co :: xi ~ zonk(ty)
(F1) typeKind(xi) succeeds and returns a fully zonked kind (F1) tcTypeKind(xi) succeeds and returns a fully zonked kind
(F2) typeKind(xi) `eqType` zonk(typeKind(ty)) (F2) tcTypeKind(xi) `eqType` zonk(tcTypeKind(ty))
Note that it is flatten's job to flatten *every type function it sees*. 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. 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 ...@@ -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, zonked, it's possible that (co :: xi ~ ty) isn't quite true. So, instead,
we can rely on this fact: 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 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, 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 ...@@ -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 even before we zonk the whole program. For example, see the FTRNotFollowed
case in flattenTyVar. 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 during canonicalisation, and we want this kind to be zonked (e.g., see
TcCanonical.canEqTyVar). TcCanonical.canEqTyVar).
Flattening is always homogeneous. That is, the kind of the result of flattening is 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: 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. 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 ...@@ -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 -> [Role] -> [Type] -- these are in 1-to-1 correspondence
-> FlatM ([Xi], [Coercion], CoercionN) -> FlatM ([Xi], [Coercion], CoercionN)
-- Coercions :: Xi ~ Type, at roles given -- 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 -- 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 -- passed as the first parameter) instantiated at xis to the kind of that
-- function instantiated at the tys. This is useful in keeping flattening -- 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 ...@@ -1294,7 +1294,7 @@ flatten_args_slow orig_binders orig_inner_ki orig_fvs orig_roles orig_tys
; return (ty, mkReflCo Phantom ty) } ; return (ty, mkReflCo Phantom ty) }
-- By Note [Flattening] invariant (F2), -- 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 -- used as an argument to a function whose kind is different, if
-- earlier arguments have been flattened to new types. We thus -- earlier arguments have been flattened to new types. We thus
-- need a coercion (kind_co :: old_kind ~ new_kind). -- need a coercion (kind_co :: old_kind ~ new_kind).
...@@ -1475,7 +1475,7 @@ flatten_app_ty_args fun_xi fun_co arg_tys ...@@ -1475,7 +1475,7 @@ flatten_app_ty_args fun_xi fun_co arg_tys
do { let tc_roles = tyConRolesRepresentational tc do { let tc_roles = tyConRolesRepresentational tc
arg_roles = dropList xis tc_roles arg_roles = dropList xis tc_roles
; (arg_xis, arg_cos, kind_co) ; (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 -- Here, we have fun_co :: T xi1 xi2 ~ ty
-- and we need to apply fun_co to the arg_cos. The problem is -- 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 ...@@ -1494,7 +1494,7 @@ flatten_app_ty_args fun_xi fun_co arg_tys
; return (app_xi, app_co, kind_co) } ; return (app_xi, app_co, kind_co) }
Nothing -> Nothing ->
do { (arg_xis, arg_cos, kind_co) 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 ; let arg_xi = mkAppTys fun_xi arg_xis
arg_co = mkAppCos fun_co arg_cos arg_co = mkAppCos fun_co arg_cos
; return (arg_xi, arg_co, kind_co) } ; return (arg_xi, arg_co, kind_co) }
...@@ -1514,7 +1514,7 @@ flatten_ty_con_app tc tys ...@@ -1514,7 +1514,7 @@ flatten_ty_con_app tc tys
homogenise_result :: Xi -- a flattened type homogenise_result :: Xi -- a flattened type
-> Coercion -- :: xi ~r original ty -> Coercion -- :: xi ~r original ty
-> Role -- r -> 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) -> (Xi, Coercion) -- (xi |> kind_co, (xi |> kind_co)
-- ~r original ty) -- ~r original ty)
homogenise_result xi co r kind_co homogenise_result xi co r kind_co
...@@ -1624,9 +1624,9 @@ flatten_fam_app tc tys -- Can be over-saturated ...@@ -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 :: TyCon -> [TcType] -> FlatM (Xi, Coercion)
flatten_exact_fam_app_fully tc tys flatten_exact_fam_app_fully tc tys
-- See Note [Reduce type family applications eagerly] -- 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 -- 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 ; mOut <- try_to_reduce_nocache tc tys reduce_co id
; case mOut of ; case mOut of
Just out -> pure out Just out -> pure out
...@@ -1636,7 +1636,7 @@ flatten_exact_fam_app_fully tc tys ...@@ -1636,7 +1636,7 @@ flatten_exact_fam_app_fully tc tys
<- setEqRel NomEq $ -- just do this once, instead of for <- setEqRel NomEq $ -- just do this once, instead of for
-- each arg -- each arg
flatten_args_tc tc (repeat Nominal) tys 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 ; eq_rel <- getEqRel
; cur_flav <- getFlavour ; cur_flav <- getFlavour
; let role = eqRelRole eq_rel ; let role = eqRelRole eq_rel
...@@ -1711,8 +1711,8 @@ flatten_exact_fam_app_fully tc tys ...@@ -1711,8 +1711,8 @@ flatten_exact_fam_app_fully tc tys
try_to_reduce :: TyCon -- F, family tycon try_to_reduce :: TyCon -- F, family tycon
-> [Type] -- args, not necessarily flattened -> [Type] -- args, not necessarily flattened
-> CoercionN -- kind_co :: typeKind(F args) ~N -> CoercionN -- kind_co :: tcTypeKind(F args) ~N
-- typeKind(F orig_args) -- tcTypeKind(F orig_args)
-- where -- where
-- orig_args is what was passed to the outer -- orig_args is what was passed to the outer
-- function -- function
...@@ -1749,8 +1749,8 @@ flatten_exact_fam_app_fully tc tys ...@@ -1749,8 +1749,8 @@ flatten_exact_fam_app_fully tc tys
try_to_reduce_nocache :: TyCon -- F, family tycon try_to_reduce_nocache :: TyCon -- F, family tycon
-> [Type] -- args, not necessarily flattened -> [Type] -- args, not necessarily flattened
-> CoercionN -- kind_co :: typeKind(F args) -> CoercionN -- kind_co :: tcTypeKind(F args)
-- ~N typeKind(F orig_args) -- ~N tcTypeKind(F orig_args)
-- where -- where
-- orig_args is what was passed to the -- orig_args is what was passed to the
-- outer function -- outer function
...@@ -2060,7 +2060,7 @@ unflattenWanteds tv_eqs funeqs ...@@ -2060,7 +2060,7 @@ unflattenWanteds tv_eqs funeqs
-- NB: unlike unflattenFmv, filling a fmv here /does/ -- NB: unlike unflattenFmv, filling a fmv here /does/
-- bump the unification count; it is "improvement" -- bump the unification count; it is "improvement"
-- Note [Unflattening can force the solver to iterate] -- 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 -- CTyEqCan invariant should ensure this is true
do { is_filled <- isFilledMetaTyVar tv do { is_filled <- isFilledMetaTyVar tv
; elim <- case is_filled of ; elim <- case is_filled of
......
...@@ -1039,7 +1039,7 @@ zonk_cmd_top env (HsCmdTop (CmdTopTc stack_tys ty ids) cmd) ...@@ -1039,7 +1039,7 @@ zonk_cmd_top env (HsCmdTop (CmdTopTc stack_tys ty ids) cmd)
new_ty <- zonkTcTypeToTypeX env ty new_ty <- zonkTcTypeToTypeX env ty
new_ids <- mapSndM (zonkExpr env) ids 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... -- desugarer assumes that this is not levity polymorphic...
-- but indeed it should always be lifted due to the typing -- but indeed it should always be lifted due to the typing
-- rules for arrows -- rules for arrows
......
...@@ -507,7 +507,7 @@ missing any patterns. ...@@ -507,7 +507,7 @@ missing any patterns.
Note [The tcType invariant] Note [The tcType invariant]
~~~~~~~~~~~~~~~~~~~~~~~~~~~ ~~~~~~~~~~~~~~~~~~~~~~~~~~~
(IT1) If tc_ty = tc_hs_type hs_ty exp_kind (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 without any zonking needed. The reason for this is that in
tcInferApps we see (F ty), and we kind-check 'ty' with an tcInferApps we see (F ty), and we kind-check 'ty' with an
expected-kind coming from F. Then, to make the resulting application expected-kind coming from F. Then, to make the resulting application
...@@ -520,17 +520,17 @@ The tcType invariant also applies to checkExpectedKind: ...@@ -520,17 +520,17 @@ The tcType invariant also applies to checkExpectedKind:
(IT2) if (IT2) if
(tc_ty, _, _) = checkExpectedKind ty act_ki exp_ki (tc_ty, _, _) = checkExpectedKind ty act_ki exp_ki
then then
typeKind tc_ty = exp_ki tcTypeKind tc_ty = exp_ki
These other invariants are all necessary, too, as these functions These other invariants are all necessary, too, as these functions
are used within tc_hs_type: 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. (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.) (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. (IT6) If (ty, ki) <- tcTyVar ..., then zonk ki == ki.
(In other words, the result kind of tcTyVar is zonked.) (In other words, the result kind of tcTyVar is zonked.)
...@@ -587,7 +587,7 @@ tc_infer_hs_type mode (HsSpliceTy _ (HsSpliced _ _ (HsSplicedTy ty))) ...@@ -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 mode (HsDocTy _ ty _) = tc_infer_lhs_type mode ty
tc_infer_hs_type _ (XHsType (NHsCoreTy ty)) tc_infer_hs_type _ (XHsType (NHsCoreTy ty))
= do { ty <- zonkTcType ty -- (IT3) and (IT4) of Note [The tcType invariant] = 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 tc_infer_hs_type mode other_ty
= do { kv <- newMetaKindVar = do { kv <- newMetaKindVar
; ty' <- tc_hs_type mode other_ty kv ; ty' <- tc_hs_type mode other_ty kv
...@@ -745,7 +745,7 @@ tc_hs_type mode rn_ty@(HsSumTy _ hs_tys) exp_kind ...@@ -745,7 +745,7 @@ tc_hs_type mode rn_ty@(HsSumTy _ hs_tys) exp_kind
= do { let arity = length hs_tys = do { let arity = length hs_tys
; arg_kinds <- mapM (\_ -> newOpenTypeKind) hs_tys ; arg_kinds <- mapM (\_ -> newOpenTypeKind) hs_tys
; tau_tys <- zipWithM (tc_lhs_type<