Commit 634c07dc authored by Richard Eisenberg's avatar Richard Eisenberg Committed by Ben Gamari
Browse files

Expand and implement Note [The tcType invariant]

Read that note -- it's necessary to make sure that we can
always call typeKind without panicking. As discussed on #14873,
there were more checks and zonking to do, implemented here.
There are no known bugs fixed by this patch, but there are likely
unknown ones.

(cherry picked from commit cf67e59a)
parent 31f7d21b
...@@ -537,9 +537,8 @@ missing any patterns. ...@@ -537,9 +537,8 @@ missing any patterns.
Note [The tcType invariant] Note [The tcType invariant]
~~~~~~~~~~~~~~~~~~~~~~~~~~~ ~~~~~~~~~~~~~~~~~~~~~~~~~~~
If tc_ty = tc_hs_type hs_ty exp_kind (IT1) If tc_ty = tc_hs_type hs_ty exp_kind
then then typeKind tc_ty = exp_kind
typeKind 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
...@@ -547,10 +546,26 @@ well kinded --- see Note [Ensure well-kinded types] in TcType --- we ...@@ -547,10 +546,26 @@ well kinded --- see Note [Ensure well-kinded types] in TcType --- we
need the kind-checked 'ty' to have exactly the kind that F expects, need the kind-checked 'ty' to have exactly the kind that F expects,
with no funny zonking nonsense in between. with no funny zonking nonsense in between.
The tcType invariant also applies to checkExpectedKind: if The tcType invariant also applies to checkExpectedKind:
(tc_ty, _, _) = checkExpectedKind ty act_ki exp_ki
then (IT2) if
typeKind tc_ty = exp_ki (tc_ty, _, _) = checkExpectedKind ty act_ki exp_ki
then
typeKind 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.
(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.
(IT6) If (ty, ki) <- tcTyVar ..., then zonk ki == ki.
(In other words, the result kind of tcTyVar is zonked.)
-} -}
------------------------------------------ ------------------------------------------
...@@ -572,17 +587,12 @@ tc_infer_hs_type mode (HsTyVar _ _ (L _ tv)) = tcTyVar mode tv ...@@ -572,17 +587,12 @@ tc_infer_hs_type mode (HsTyVar _ _ (L _ tv)) = tcTyVar mode tv
tc_infer_hs_type mode (HsAppTy _ ty1 ty2) tc_infer_hs_type mode (HsAppTy _ ty1 ty2)
= do { let (hs_fun_ty, hs_arg_tys) = splitHsAppTys ty1 [ty2] = do { let (hs_fun_ty, hs_arg_tys) = splitHsAppTys ty1 [ty2]
; (fun_ty, fun_kind) <- tc_infer_lhs_type mode hs_fun_ty ; (fun_ty, fun_kind) <- tc_infer_lhs_type mode hs_fun_ty
-- A worry: what if fun_kind needs zoonking? -- NB: (IT4) of Note [The tcType invariant] ensures that fun_kind is zonked
-- We used to zonk it here, but that got fun_ty and fun_kind
-- out of sync (see the precondition to tcTyApps), which caused
-- Trac #14873. So I'm now zonking in tcTyVar, and not here.
-- Is that enough? Seems so, but I can't see how to be certain.
; tcTyApps mode hs_fun_ty fun_ty fun_kind hs_arg_tys } ; tcTyApps mode hs_fun_ty fun_ty fun_kind hs_arg_tys }
tc_infer_hs_type mode (HsOpTy _ lhs lhs_op@(L _ hs_op) rhs) tc_infer_hs_type mode (HsOpTy _ lhs lhs_op@(L _ hs_op) rhs)
| not (hs_op `hasKey` funTyConKey) | not (hs_op `hasKey` funTyConKey)
= do { (op, op_kind) <- tcTyVar mode hs_op = do { (op, op_kind) <- tcTyVar mode hs_op
-- See "A worry" in the HsApp case
; tcTyApps mode (noLoc $ HsTyVar noExt NotPromoted lhs_op) op op_kind ; tcTyApps mode (noLoc $ HsTyVar noExt NotPromoted lhs_op) op op_kind
[lhs, rhs] } [lhs, rhs] }
...@@ -606,7 +616,9 @@ tc_infer_hs_type mode (HsSpliceTy _ (HsSpliced _ _ (HsSplicedTy ty))) ...@@ -606,7 +616,9 @@ tc_infer_hs_type mode (HsSpliceTy _ (HsSpliced _ _ (HsSplicedTy ty)))
= tc_infer_hs_type mode ty = tc_infer_hs_type mode 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)) = return (ty, typeKind ty) tc_infer_hs_type _ (XHsType (NHsCoreTy ty))
= do { ty <- zonkTcType ty -- (IT3) and (IT4) of Note [The tcType invariant]
; return (ty, typeKind 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
...@@ -702,7 +714,7 @@ tc_hs_type mode (HsQualTy { hst_ctxt = ctxt, hst_body = ty }) exp_kind ...@@ -702,7 +714,7 @@ tc_hs_type mode (HsQualTy { hst_ctxt = ctxt, hst_body = ty }) exp_kind
then tc_lhs_type mode ty constraintKind then tc_lhs_type mode ty constraintKind
else do { ek <- newOpenTypeKind else do { ek <- newOpenTypeKind
-- The body kind (result of the function) -- The body kind (result of the function)
-- can be * or #, hence newOpenTypeKind -- can be TYPE r, for any r, hence newOpenTypeKind
; ty' <- tc_lhs_type mode ty ek ; ty' <- tc_lhs_type mode ty ek
; checkExpectedKind (unLoc ty) ty' liftedTypeKind exp_kind } ; checkExpectedKind (unLoc ty) ty' liftedTypeKind exp_kind }
...@@ -914,11 +926,13 @@ tcInferApps :: TcTyMode ...@@ -914,11 +926,13 @@ tcInferApps :: TcTyMode
-- Reason: we will return a type application like (fun_ty arg1 ... argn), -- Reason: we will return a type application like (fun_ty arg1 ... argn),
-- and that type must be well-kinded -- and that type must be well-kinded
-- See Note [The tcType invariant] -- See Note [The tcType invariant]
-- Postcondition: Result kind is zonked.
tcInferApps mode mb_kind_info orig_hs_ty fun_ty fun_ki orig_hs_args tcInferApps mode mb_kind_info orig_hs_ty fun_ty fun_ki orig_hs_args
= do { traceTc "tcInferApps {" (ppr orig_hs_ty $$ ppr orig_hs_args $$ ppr fun_ki) = do { traceTc "tcInferApps {" (ppr orig_hs_ty $$ ppr orig_hs_args $$ ppr fun_ki)
; stuff <- go 1 [] empty_subst fun_ty orig_ki_binders orig_inner_ki orig_hs_args ; (f_args, args, res_k) <- go 1 [] empty_subst fun_ty orig_ki_binders orig_inner_ki orig_hs_args
; traceTc "tcInferApps }" empty ; traceTc "tcInferApps }" empty
; return stuff } ; res_k <- zonkTcType res_k -- nec'y to uphold (IT4) of Note [The tcType invariant]
; return (f_args, args, res_k) }
where where
empty_subst = mkEmptyTCvSubst $ mkInScopeSet $ empty_subst = mkEmptyTCvSubst $ mkInScopeSet $
tyCoVarsOfType fun_ki tyCoVarsOfType fun_ki
...@@ -992,11 +1006,12 @@ tcTyApps :: TcTyMode ...@@ -992,11 +1006,12 @@ tcTyApps :: TcTyMode
-> TcType -- ^ Function (could be knot-tied) -> TcType -- ^ Function (could be knot-tied)
-> TcKind -- ^ Function kind (zonked) -> TcKind -- ^ Function kind (zonked)
-> [LHsType GhcRn] -- ^ Args -> [LHsType GhcRn] -- ^ Args
-> TcM (TcType, TcKind) -- ^ (f args, result kind) -> TcM (TcType, TcKind) -- ^ (f args, result kind) result kind is zonked
-- Precondition: see precondition for tcInferApps -- Precondition: see precondition for tcInferApps
tcTyApps mode orig_hs_ty fun_ty fun_ki args tcTyApps mode orig_hs_ty fun_ty fun_ki args
= do { (ty', _args, ki') <- tcInferApps mode Nothing orig_hs_ty fun_ty fun_ki args = do { (ty', _args, ki') <- tcInferApps mode Nothing orig_hs_ty fun_ty fun_ki args
; return (ty', ki') } ; return (ty' `mkNakedCastTy` mkRepReflCo ki', ki') }
-- The mkNakedCastTy is for (IT3) of Note [The tcType invariant]
-------------------------- --------------------------
-- Like checkExpectedKindX, but returns only the final type; convenient wrapper -- Like checkExpectedKindX, but returns only the final type; convenient wrapper
...@@ -1054,11 +1069,12 @@ checkExpectedKindX mb_kind_env pp_hs_ty ty act_kind exp_kind ...@@ -1054,11 +1069,12 @@ checkExpectedKindX mb_kind_env pp_hs_ty ty act_kind exp_kind
-- | Instantiate @n@ invisible arguments to a type. If @n <= 0@, no instantiation -- | Instantiate @n@ invisible arguments to a type. If @n <= 0@, no instantiation
-- occurs. If @n@ is too big, then all available invisible arguments are instantiated. -- occurs. If @n@ is too big, then all available invisible arguments are instantiated.
-- (In other words, this function is very forgiving about bad values of @n@.) -- (In other words, this function is very forgiving about bad values of @n@.)
-- Why zonk the result? So that tcTyVar can obey (IT6) of Note [The tcType invariant]
instantiateTyN :: Maybe (VarEnv Kind) -- ^ Predetermined instantiations instantiateTyN :: Maybe (VarEnv Kind) -- ^ Predetermined instantiations
-- (for assoc. type patterns) -- (for assoc. type patterns)
-> Int -- ^ @n@ -> Int -- ^ @n@
-> [TyBinder] -> TcKind -- ^ its kind -> [TyBinder] -> TcKind -- ^ its kind (zonked)
-> TcM ([TcType], TcKind) -- ^ The inst'ed type, new args, kind -> TcM ([TcType], TcKind) -- ^ The inst'ed type, new args, kind (zonked)
instantiateTyN mb_kind_env n bndrs inner_ki instantiateTyN mb_kind_env n bndrs inner_ki
| n <= 0 | n <= 0
= return ([], ki) = return ([], ki)
...@@ -1066,7 +1082,7 @@ instantiateTyN mb_kind_env n bndrs inner_ki ...@@ -1066,7 +1082,7 @@ instantiateTyN mb_kind_env n bndrs inner_ki
| otherwise | otherwise
= do { (subst, inst_args) <- tcInstTyBinders empty_subst mb_kind_env inst_bndrs = do { (subst, inst_args) <- tcInstTyBinders empty_subst mb_kind_env inst_bndrs
; let rebuilt_ki = mkPiTys leftover_bndrs inner_ki ; let rebuilt_ki = mkPiTys leftover_bndrs inner_ki
ki' = substTy subst rebuilt_ki ; ki' <- zonkTcType (substTy subst rebuilt_ki)
; traceTc "instantiateTyN" (vcat [ ppr ki ; traceTc "instantiateTyN" (vcat [ ppr ki
, ppr n , ppr n
, ppr subst , ppr subst
...@@ -1173,22 +1189,24 @@ tcTyVar mode name -- Could be a tyvar, a tycon, or a datacon ...@@ -1173,22 +1189,24 @@ tcTyVar mode name -- Could be a tyvar, a tycon, or a datacon
handle_tyfams tc tc_tc handle_tyfams tc tc_tc
| mightBeUnsaturatedTyCon tc_tc || mode_unsat mode | mightBeUnsaturatedTyCon tc_tc || mode_unsat mode
-- This is where mode_unsat is used -- This is where mode_unsat is used
= do { traceTc "tcTyVar2a" (ppr tc_tc $$ ppr tc_kind) = do { tc_kind <- zonkTcType (tyConKind tc_tc) -- (IT6) of Note [The tcType invariant]
; return (mkNakedTyConApp tc [], tc_kind) } ; traceTc "tcTyVar2a" (ppr tc_tc $$ ppr tc_kind)
; return (mkNakedTyConApp tc [] `mkNakedCastTy` mkRepReflCo tc_kind, tc_kind) }
-- the mkNakedCastTy ensures (IT5) of Note [The tcType invariant]
| otherwise | otherwise
= do { (tc_args, kind) <- instantiateTyN Nothing (length (tyConBinders tc_tc)) = do { tc_kind <- zonkTcType (tyConKind tc_tc)
; let (tc_kind_bndrs, tc_inner_ki) = splitPiTysInvisible tc_kind
; (tc_args, kind) <- instantiateTyN Nothing (length (tyConBinders tc_tc))
tc_kind_bndrs tc_inner_ki tc_kind_bndrs tc_inner_ki
; let tc_ty = mkNakedTyConApp tc tc_args ; let tc_ty = mkNakedTyConApp tc tc_args `mkNakedCastTy` mkRepReflCo kind
-- mkNakedCastTy is for (IT5) of Note [The tcType invariant]
-- tc and tc_ty must not be traced here, because that would -- tc and tc_ty must not be traced here, because that would
-- force the evaluation of a potentially knot-tied variable (tc), -- force the evaluation of a potentially knot-tied variable (tc),
-- and the typechecker would hang, as per #11708 -- and the typechecker would hang, as per #11708
; traceTc "tcTyVar2b" (vcat [ ppr tc_tc <+> dcolon <+> ppr tc_kind ; traceTc "tcTyVar2b" (vcat [ ppr tc_tc <+> dcolon <+> ppr tc_kind
, ppr kind ]) , ppr kind ])
; return (tc_ty, kind) } ; return (tc_ty, kind) }
where
tc_kind = tyConKind tc_tc
(tc_kind_bndrs, tc_inner_ki) = splitPiTysInvisible tc_kind
get_loopy_tc :: Name -> TyCon -> TcM TyCon get_loopy_tc :: Name -> TyCon -> TcM TyCon
-- Return the knot-tied global TyCon if there is one -- Return the knot-tied global TyCon if there is one
...@@ -2726,6 +2744,7 @@ It does sort checking and desugaring at the same time, in one single pass. ...@@ -2726,6 +2744,7 @@ It does sort checking and desugaring at the same time, in one single pass.
tcLHsKindSig :: UserTypeCtxt -> LHsKind GhcRn -> TcM Kind tcLHsKindSig :: UserTypeCtxt -> LHsKind GhcRn -> TcM Kind
tcLHsKindSig ctxt hs_kind tcLHsKindSig ctxt hs_kind
-- See Note [Recipe for checking a signature] in TcHsType -- See Note [Recipe for checking a signature] in TcHsType
-- Result is zonked
= do { kind <- solveLocalEqualities $ = do { kind <- solveLocalEqualities $
tc_lhs_kind kindLevelMode hs_kind tc_lhs_kind kindLevelMode hs_kind
; kind <- zonkPromoteType kind ; kind <- zonkPromoteType kind
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment