diff options
| -rw-r--r-- | compiler/typecheck/TcHsType.hs | 118 | ||||
| -rw-r--r-- | compiler/typecheck/TcTyClsDecls.hs | 6 | ||||
| -rw-r--r-- | compiler/typecheck/TcValidity.hs | 4 | ||||
| -rw-r--r-- | compiler/types/Coercion.hs | 19 | ||||
| -rw-r--r-- | compiler/types/Coercion.hs-boot | 2 | ||||
| -rw-r--r-- | compiler/types/TyCoRep.hs | 26 | ||||
| -rw-r--r-- | compiler/types/Type.hs | 76 | ||||
| -rw-r--r-- | testsuite/tests/typecheck/should_fail/T16627.stderr | 4 |
8 files changed, 122 insertions, 133 deletions
diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs index 9a5d745dea..c9bb390f9e 100644 --- a/compiler/typecheck/TcHsType.hs +++ b/compiler/typecheck/TcHsType.hs @@ -1098,7 +1098,7 @@ tcInferApps_nosat mode orig_hs_ty fun orig_hs_args Named (Bndr _ Inferred) -> instantiate ki_binder inner_ki Anon InvisArg _ -> instantiate ki_binder inner_ki - Named (Bndr _ Specified) -> -- Visible kind application + Named (Bndr tv Specified) -> -- Visible kind application do { traceTc "tcInferApps (vis kind app)" (vcat [ ppr ki_binder, ppr hs_ki_arg , ppr (tyBinderType ki_binder) @@ -1114,7 +1114,9 @@ tcInferApps_nosat mode orig_hs_ty fun orig_hs_args tc_lhs_type (kindLevel mode) hs_ki_arg exp_kind ; traceTc "tcInferApps (vis kind app)" (ppr exp_kind) - ; (subst', fun') <- mkAppTyM subst fun ki_binder ki_arg + + ; let subst' = extendTvSubstAndInScope subst tv ki_arg + fun' = mk_app_ty fun ki_arg ; go (n+1) fun' subst' inner_ki hs_args } -- Attempted visible kind application (fun @ki), but fun_ki is @@ -1144,7 +1146,8 @@ tcInferApps_nosat mode orig_hs_ty fun orig_hs_args ; arg' <- addErrCtxt (funAppCtxt orig_hs_ty arg n) $ tc_lhs_type mode arg exp_kind ; traceTc "tcInferApps (vis normal app) 2" (ppr exp_kind) - ; (subst', fun') <- mkAppTyM subst fun ki_binder arg' + ; let subst' = extendTvSubstBinderAndInScope subst ki_binder arg' + fun' = mk_app_ty fun arg' ; go (n+1) fun' subst' inner_ki args } -- no binder; try applying the substitution, or infer another arrow in fun kind @@ -1170,9 +1173,6 @@ tcInferApps_nosat mode orig_hs_ty fun orig_hs_args (vcat [ ppr ki_binder, ppr subst]) ; (subst', arg') <- tcInstInvisibleTyBinder subst ki_binder ; go n (mkAppTy fun arg') subst' inner_ki all_args } - -- Because tcInvisibleTyBinder instantiate ki_binder, - -- the kind of arg' will have the same shape as the kind - -- of ki_binder. So we don't need mkAppTyM here. try_again_after_substing_or fallthrough | not (isEmptyTCvSubst subst) @@ -1194,65 +1194,15 @@ tcInferApps_nosat mode orig_hs_ty fun orig_hs_args = failWith $ text "Cannot apply function of kind" <+> quotes (ppr ty) $$ text "to visible kind argument" <+> quotes (ppr arg) - -mkAppTyM :: TCvSubst - -> TcType -> TyCoBinder -- fun, plus its top-level binder - -> TcType -- arg - -> TcM (TCvSubst, TcType) -- Extended subst, plus (fun arg) --- Precondition: the application (fun arg) is well-kinded after zonking --- That is, the application makes sense --- --- Precondition: for (mkAppTyM subst fun bndr arg) --- tcTypeKind fun = Pi bndr. body --- That is, fun always has a ForAllTy or FunTy at the top --- and 'bndr' is fun's pi-binder --- --- Postcondition: if fun and arg satisfy (PKTI), the purely-kinded type --- invariant, then so does the result type (fun arg) --- --- We do not require that --- tcTypeKind arg = tyVarKind (binderVar bndr) --- This must be true after zonking (precondition 1), but it's not --- required for the (PKTI). -mkAppTyM subst fun ki_binder arg - | -- See Note [mkAppTyM]: Nasty case 2 - TyConApp tc args <- fun - , isTypeSynonymTyCon tc - , args `lengthIs` (tyConArity tc - 1) - , any isTrickyTvBinder (tyConTyVars tc) -- We could cache this in the synonym - = do { arg' <- zonkTcType arg - ; args' <- zonkTcTypes args - ; let subst' = case ki_binder of - Anon {} -> subst - Named (Bndr tv _) -> extendTvSubstAndInScope subst tv arg' - ; return (subst', mkTyConApp tc (args' ++ [arg'])) } - - -mkAppTyM subst fun (Anon {}) arg - = return (subst, mk_app_ty fun arg) - -mkAppTyM subst fun (Named (Bndr tv _)) arg - = do { arg' <- if isTrickyTvBinder tv - then -- See Note [mkAppTyM]: Nasty case 1 - zonkTcType arg - else return arg - ; return ( extendTvSubstAndInScope subst tv arg' - , mk_app_ty fun arg' ) } - mk_app_ty :: TcType -> TcType -> TcType -- This function just adds an ASSERT for mkAppTyM's precondition mk_app_ty fun arg = ASSERT2( isPiTy fun_kind - , ppr fun <+> dcolon <+> ppr fun_kind $$ ppr arg ) + , ppr fun <+> dcolon <+> ppr fun_kind $$ ppr arg ) mkAppTy fun arg where fun_kind = tcTypeKind fun -isTrickyTvBinder :: TcTyVar -> Bool --- NB: isTrickyTvBinder is just an optimisation --- It would be absolutely sound to return True always -isTrickyTvBinder tv = isPiTy (tyVarKind tv) - {- Note [The Purely Kinded Type Invariant (PKTI)] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ During type inference, we maintain this invariant @@ -1274,48 +1224,28 @@ For example, suppose kappa is a unification variable We have already unified kappa := Type yielding co :: Refl (Type -> Type) - a :: kappa + We have a type variable a :: kappa then consider the type (a Int) If we call tcTypeKind on that, we'll crash, because the (un-zonked) -kind of 'a' is just kappa, not an arrow kind. So we must zonk first. - -So the type inference engine is very careful when building applications. -This happens in tcInferApps. Suppose we are kind-checking the type (a Int), -where (a :: kappa). Then in tcInferApps we'll run out of binders on -a's kind, so we'll call matchExpectedFunKind, and unify - kappa := kappa1 -> kappa2, with evidence co :: kappa ~ (kappa1 ~ kappa2) -At this point we must zonk the function type to expose the arrrow, so -that (a Int) will satisfy (PKTI). +kind of 'a' is just kappa, not an arrow kind. So we instead use + ((a |> co) Int) + +For this reason, mkCastTy is very careful about discarding reflexive +coercions. Suppose we have + (mkCastTy ty co) +and + ty :: k1 + co :: k2 ~ k3 +After type inference k1=k2 always. But /during/ type inference we +might have k1 /= k2. Specifically, + * zonk(k1) = zonk(k2) + * k2 may be more zonked than k1, but never the other way around + +So mkCastTy can discard the coercion when (and only when) + kind( ty ) = resultKind( co ) The absence of this caused #14174 and #14520. - -The calls to mkAppTyM is the other place we are very careful. - -Note [mkAppTyM] -~~~~~~~~~~~~~~~ -mkAppTyM is trying to guarantee the Purely Kinded Type Invariant -(PKTI) for its result type (fun arg). There are two ways it can go wrong: - -* Nasty case 1: forall types (polykinds/T14174a) - T :: forall (p :: *->*). p Int -> p Bool - Now kind-check (T x), where x::kappa. - Well, T and x both satisfy the PKTI, but - T x :: x Int -> x Bool - and (x Int) does /not/ satisfy the PKTI. - -* Nasty case 2: type synonyms - type S f a = f a - Even though (S ff aa) would satisfy the (PKTI) if S was a data type - (i.e. nasty case 1 is dealt with), it might still not satisfy (PKTI) - if S is a type synonym, because the /expansion/ of (S ff aa) is - (ff aa), and /that/ does not satisfy (PKTI). E.g. perhaps - (ff :: kappa), where 'kappa' has already been unified with (*->*). - - We check for nasty case 2 on the final argument of a type synonym. - -Notice that in both cases the trickiness only happens if the -bound variable has a pi-type. Hence isTrickyTvBinder. -} diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs index 545f001f00..495305a274 100644 --- a/compiler/typecheck/TcTyClsDecls.hs +++ b/compiler/typecheck/TcTyClsDecls.hs @@ -2962,7 +2962,7 @@ rejigConRes :: [KnotTied TyConBinder] -> KnotTied Type -- Template for result -- the same as the parent tycon, because checkValidDataCon will do it -- NB: All arguments may potentially be knot-tied rejigConRes tmpl_bndrs res_tmpl dc_inferred_tvs dc_specified_tvs res_ty - -- E.g. data T [a] b c where + -- E.g. data instance T [a] b c where -- MkT :: forall x y z. T [(x,y)] z z -- The {a,b,c} are the tmpl_tvs, and the {x,y,z} are the dc_tvs -- (NB: unlike the H98 case, the dc_tvs are not all existential) @@ -2994,8 +2994,8 @@ rejigConRes tmpl_bndrs res_tmpl dc_inferred_tvs dc_specified_tvs res_ty substed_eqs = map (substEqSpec arg_subst) raw_eqs in - (univ_tvs, substed_ex_tvs, substed_inferred_tvs, substed_specified_tvs, - substed_eqs, arg_subst) + ( univ_tvs, substed_ex_tvs, substed_inferred_tvs + , substed_specified_tvs, substed_eqs, arg_subst) | otherwise -- If the return type of the data constructor doesn't match the parent diff --git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs index 3f780fe546..0d10add09a 100644 --- a/compiler/typecheck/TcValidity.hs +++ b/compiler/typecheck/TcValidity.hs @@ -206,7 +206,7 @@ so we can take their type variables into account as part of the checkAmbiguity :: UserTypeCtxt -> Type -> TcM () checkAmbiguity ctxt ty | wantAmbiguityCheck ctxt - = do { traceTc "Ambiguity check for" (ppr ty) + = do { traceTc "Ambiguity check for {" (ppr ty) -- Solve the constraints eagerly because an ambiguous type -- can cause a cascade of further errors. Since the free -- tyvars are skolemised, we can safely use tcSimplifyTop @@ -216,7 +216,7 @@ checkAmbiguity ctxt ty tcSubType_NC ctxt ty ty ; simplifyAmbiguityCheck ty wanted - ; traceTc "Done ambiguity check for" (ppr ty) } + ; traceTc "} Done ambiguity check for" (ppr ty) } | otherwise = return () diff --git a/compiler/types/Coercion.hs b/compiler/types/Coercion.hs index b338bfbf9e..cfb1b1ecd1 100644 --- a/compiler/types/Coercion.hs +++ b/compiler/types/Coercion.hs @@ -352,11 +352,19 @@ Notes: -} decomposePiCos :: HasDebugCallStack - => CoercionN -> Pair Type -- Coercion and its kind - -> [Type] + => Kind -- k1 + -> CoercionN -- co + -> Kind -- k2 + -> [Type] -- t1 .. tn -> ([CoercionN], CoercionN) +-- We have ((ty :: k1) |> (co :: kx ~ k2)) t1 .. tn +-- and k1, k2 are the two kinds above +-- NB: usually k1=kx, but perhaps not during type inference +-- See Note [The Purely Kinded Type Invariant (PKTI)] in TcHsType +-- +-- We don't pass in 'ty' at all -- See Note [Pushing a coercion into a pi-type] -decomposePiCos orig_co (Pair orig_k1 orig_k2) orig_args +decomposePiCos orig_k1 orig_co orig_k2 orig_args = go [] (orig_subst,orig_k1) orig_co (orig_subst,orig_k2) orig_args where orig_subst = mkEmptyTCvSubst $ mkInScopeSet $ @@ -2876,9 +2884,9 @@ simplifyArgsWorker orig_ki_binders orig_inner_ki orig_fvs -- See Note [Last case in simplifyArgsWorker] go acc_xis acc_cos lc [] inner_ki roles args = let co1 = liftCoSubst Nominal lc inner_ki - co1_kind = coercionKind co1 + Pair flattened_kind orig_kind = coercionKind co1 unflattened_tys = map (coercionRKind . snd) args - (arg_cos, res_co) = decomposePiCos co1 co1_kind unflattened_tys + (arg_cos, res_co) = decomposePiCos flattened_kind co1 orig_kind unflattened_tys casted_args = ASSERT2( equalLength args arg_cos , ppr args $$ ppr arg_cos ) [ (casted_xi, casted_co) @@ -2892,7 +2900,6 @@ simplifyArgsWorker orig_ki_binders orig_inner_ki orig_fvs -- ... -> k, that k will be substituted to perhaps reveal more -- binders. zapped_lc = zapLiftingContext lc - Pair flattened_kind _ = co1_kind (bndrs, new_inner) = splitPiTys flattened_kind (xis_out, cos_out, res_co_out) diff --git a/compiler/types/Coercion.hs-boot b/compiler/types/Coercion.hs-boot index eb5e81b819..42d09c120a 100644 --- a/compiler/types/Coercion.hs-boot +++ b/compiler/types/Coercion.hs-boot @@ -38,7 +38,7 @@ mkAxiomRuleCo :: CoAxiomRule -> [Coercion] -> Coercion isGReflCo :: Coercion -> Bool isReflCo :: Coercion -> Bool isReflexiveCo :: Coercion -> Bool -decomposePiCos :: HasDebugCallStack => Coercion -> Pair Type -> [Type] -> ([Coercion], Coercion) +decomposePiCos :: HasDebugCallStack => Kind -> Coercion -> Kind -> [Type] -> ([Coercion], Coercion) coVarKindsTypesRole :: HasDebugCallStack => CoVar -> (Kind, Kind, Type, Type, Role) coVarRole :: CoVar -> Role diff --git a/compiler/types/TyCoRep.hs b/compiler/types/TyCoRep.hs index be2f74c731..f9a439b0b1 100644 --- a/compiler/types/TyCoRep.hs +++ b/compiler/types/TyCoRep.hs @@ -545,7 +545,7 @@ Accordingly, by eliminating reflexive casts, splitTyConApp need not worry about outermost casts to uphold (EQ). Eliminating reflexive casts is done in mkCastTy. -Unforunately, that's not the end of the story. Consider comparing +Unfortunately, that's not the end of the story. Consider comparing (T a b c) =? (T a b |> (co -> <Type>)) (c |> co) These two types have the same kind (Type), but the left type is a TyConApp while the right type is not. To handle this case, we say that the right-hand @@ -567,15 +567,27 @@ our (EQ) property. Lastly, in order to detect reflexive casts reliably, we must make sure not to have nested casts: we update (t |> co1 |> co2) to (t |> (co1 `TransCo` co2)). -In sum, in order to uphold (EQ), we need the following three invariants: +In sum, in order to uphold (EQ), we need the following four invariants: + + (EQ1) No ((fun_ty |> co) arg_ty) + where kind(fun_ty) = k1 -> k2 and resultKind(co) = k3 -> k4 + or kind(fun_ty) = forall a.k1 and resultKind(co) = forall a.k2 + In these cases we can push the coercion to give + (fun_ty (arg_ty |> co1)) |> co2 + where co1, co2 are gotten from co + Upheld by Type.mkAppTy + + (EQ2) No (ty |> co) where kind(ty) = resultKind(co) + In this case we can discard the coercion altogether + Upheld by Type.mCastTy + + (EQ3) No nested CastTys, (ty |> co1 |> co2) + In this case we can combine the coercions + Upheld by Type.mCastTy - (EQ1) No decomposable CastTy to the left of an AppTy, where a decomposable - cast is one that relates either a FunTy to a FunTy or a - ForAllTy to a ForAllTy. - (EQ2) No reflexive casts in CastTy. - (EQ3) No nested CastTys. (EQ4) No CastTy over (ForAllTy (Bndr tyvar vis) body). See Note [Weird typing rule for ForAllTy] in Type. + Upheld by Type.mCastTy These invariants are all documented above, in the declaration for Type. diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs index 749578d78f..bb85b29b36 100644 --- a/compiler/types/Type.hs +++ b/compiler/types/Type.hs @@ -248,7 +248,7 @@ import {-# SOURCE #-} Coercion( mkNomReflCo, mkGReflCo, mkReflCo , mkKindCo, mkSubCo, mkFunCo, mkAxiomInstCo , decomposePiCos, coercionKind, coercionLKind , coercionRKind, coercionType - , isReflexiveCo, seqCo ) + , seqCo ) -- others import Util @@ -764,13 +764,24 @@ the test in repSplitAppTy_maybe, which applies throughout, because the other calls to splitAppTy are in Unify, which is also used by the type checker (e.g. when matching type-function equations). +Note [mkAppTy subtleties] +~~~~~~~~~~~~~~~~~~~~~~~~~ +Very important: mkAppTy is responsible for upholding (EQ1) in +Note [Respecting definitional equality] in TyCoRep. + +Specifically, to uphold (EQ1) we have work to do when doing + mkAppTy (fun_ty |>co) arg_ty +Note, crucially, that we pass (typeKind fun_ty) to decomposePiCos +rather than inputKind( co ); the two may differ during type inference +See Note [The Purely Kinded Type Invariant (PKTI)] in TcHsType. -} -- | Applies a type to another, as in e.g. @k a@ mkAppTy :: Type -> Type -> Type - -- See Note [Respecting definitional equality], invariant (EQ1). +-- See Note [mkAppTy subtleties] mkAppTy (CastTy fun_ty co) arg_ty - | ([arg_co], res_co) <- decomposePiCos co (coercionKind co) [arg_ty] + | ([arg_co], res_co) <- decomposePiCos (typeKind fun_ty) co + (pSnd $ coercionKind co) [arg_ty] = (fun_ty `mkAppTy` (arg_ty `mkCastTy` arg_co)) `mkCastTy` res_co mkAppTy (TyConApp tc tys) ty2 = mkTyConApp tc (tys ++ [ty2]) @@ -789,16 +800,18 @@ mkAppTy ty1 ty2 = AppTy ty1 ty2 -- (T t1), (T t1 t2), etc mkAppTys :: Type -> [Type] -> Type -mkAppTys ty1 [] = ty1 -mkAppTys (CastTy fun_ty co) arg_tys -- much more efficient then nested mkAppTy - -- Why do this? See (EQ1) of - -- Note [Respecting definitional equality] - -- in TyCoRep - = foldl' AppTy ((mkAppTys fun_ty casted_arg_tys) `mkCastTy` res_co) leftovers +mkAppTys ty1 [] = ty1 + +mkAppTys (CastTy fun_ty co) arg_tys + = -- Much more efficient then nested mkAppTy + -- But see Note [mkAppTy subtleties] + foldl' AppTy ((mkAppTys fun_ty casted_arg_tys) `mkCastTy` res_co) leftovers where - (arg_cos, res_co) = decomposePiCos co (coercionKind co) arg_tys + (arg_cos, res_co) = decomposePiCos (typeKind fun_ty) co + (pSnd $ coercionKind co) arg_tys (args_to_cast, leftovers) = splitAtList arg_cos arg_tys casted_arg_tys = zipWith mkCastTy args_to_cast arg_cos + mkAppTys (TyConApp tc tys1) tys2 = mkTyConApp tc (tys1 ++ tys2) mkAppTys ty1 tys2 = foldl' AppTy ty1 tys2 @@ -1316,16 +1329,41 @@ splitCastTy_maybe ty | Just ty' <- coreView ty = splitCastTy_maybe ty' splitCastTy_maybe (CastTy ty co) = Just (ty, co) splitCastTy_maybe _ = Nothing --- | Make a 'CastTy'. The Coercion must be nominal. Checks the --- Coercion for reflexivity, dropping it if it's reflexive. --- See Note [Respecting definitional equality] in TyCoRep + +{- Note [mkCastTy subtleties] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Super important: mkCastTy is responsible for maintaining invariants +(EQ2-4) in Note [Respecting definitional equality] in TyCoRep. +See also Note [mkAppTy subtleties]. + +Specifically + +* EQ2: we must to a full `eqType` check her. This is important to keep + the splitXXX functions working properly. Otherwise we may end up + with something like + (((->) |> something_reflexive_but_not_obviously_so) biz baz) + which fails under splitFunTy_maybe. This happened with the cheaper check + in test dependent/should_compile/dynamic-paper. + See Note [Respecting definitional equality] in TyCoRep + +* EQ2: crucially, note that we do /not/ use isReflexiveCo, + because during type inference the kind of 'ty' may be less + zonked than the input kind of the coercion. See + Note [The Purely Kinded Type Invariant (PKTI)] in TcHsType + +* EQ3 (cast of cast) is easy + +* EQ3 (cast of forall) is reasonably easy +-} + +-- | Make a 'CastTy'. The Coercion must be nominal. +-- Some very important subtleties here: see Note [mkCastTy] mkCastTy :: Type -> Coercion -> Type -mkCastTy ty co | isReflexiveCo co = ty -- (EQ2) from the Note --- NB: Do the slow check here. This is important to keep the splitXXX --- functions working properly. Otherwise, we may end up with something --- like (((->) |> something_reflexive_but_not_obviously_so) biz baz) --- fails under splitFunTy_maybe. This happened with the cheaper check --- in test dependent/should_compile/dynamic-paper. +mkCastTy ty co + | let co_res_kind = pSnd (coercionKind co) + , typeKind ty `eqType` co_res_kind -- (EQ2) from the Note + -- Not isReflexiveCo! See Note [mkCastTy subtleties] + = ty mkCastTy (CastTy ty co1) co2 -- (EQ3) from the Note diff --git a/testsuite/tests/typecheck/should_fail/T16627.stderr b/testsuite/tests/typecheck/should_fail/T16627.stderr index 108e99f44a..d66122f342 100644 --- a/testsuite/tests/typecheck/should_fail/T16627.stderr +++ b/testsuite/tests/typecheck/should_fail/T16627.stderr @@ -1,6 +1,8 @@ T16627.hs:11:15: error: - • No instance for (Typeable r1) arising from a use of ‘typeRep’ + • No instance for (Typeable (->)) arising from a use of ‘typeRep’ + GHC can't yet do polykinded + Typeable ((->) :: TYPE r1 -> TYPE r2 -> *) • In the first argument of ‘mkTrApp’, namely ‘typeRep’ In the first argument of ‘mkTrApp’, namely ‘typeRep `mkTrApp` a’ In the expression: typeRep `mkTrApp` a `mkTrApp` b |