From 51ae3ba02a5d241a4c64f7c7e4808fbd8b814e31 Mon Sep 17 00:00:00 2001 From: Simon Peyton Jones Date: Thu, 21 Jul 2022 23:56:32 +0100 Subject: Fix the interaction of operator sections and deep subsumption Fixes DeepSubsumption08 --- compiler/GHC/Rename/Expr.hs | 10 ++++++++++ compiler/GHC/Tc/Gen/App.hs | 26 ++++++++++++++++++++------ compiler/GHC/Tc/Utils/Unify.hs | 22 ++++++++++++++++++++-- 3 files changed, 50 insertions(+), 8 deletions(-) diff --git a/compiler/GHC/Rename/Expr.hs b/compiler/GHC/Rename/Expr.hs index 6316ecea63..b0f13dfc12 100644 --- a/compiler/GHC/Rename/Expr.hs +++ b/compiler/GHC/Rename/Expr.hs @@ -695,6 +695,16 @@ Note the wrinkles: (e `op`) ==> op e with no auxiliary function at all. Simple! +* leftSection and rightSection switch on ImpredicativeTypes locally, + during Quick Look; see GHC.Tc.Gen.App.wantQuickLook. Consider + test DeepSubsumption08: + type Setter st t a b = forall f. Identical f => blah + (.~) :: Setter s t a b -> b -> s -> t + clear :: Setter a a' b (Maybe b') -> a -> a' + clear = (.~ Nothing) + The expansion look like (rightSection (.~) Nothing). So we must + instantiate `rightSection` first type argument to a polytype! + Hence the special magic in App.wantQuickLook. Historical Note [Desugaring operator sections] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/compiler/GHC/Tc/Gen/App.hs b/compiler/GHC/Tc/Gen/App.hs index 69a077c15b..4f04e82cf2 100644 --- a/compiler/GHC/Tc/Gen/App.hs +++ b/compiler/GHC/Tc/Gen/App.hs @@ -289,6 +289,7 @@ particular Ids: the renamer (Note [Handling overloaded and rebindable constructs] in GHC.Rename.Expr), and we want them to be instantiated impredicatively so that (f `op`), say, will work OK even if `f` is higher rank. + See Note [Left and right sections] in GHC.Rename.Expr. Note [Unify with expected type before typechecking arguments] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -352,12 +353,26 @@ tcApp rn_expr exp_res_ty = addFunResCtxt rn_fun rn_args app_res_rho exp_res_ty $ thing_inside + -- Match up app_res_rho: the result type of rn_expr + -- with exp_res_ty: the expected result type + ; do_ds <- xoptM LangExt.DeepSubsumption ; res_wrap <- perhaps_add_res_ty_ctxt $ - tcSubTypeNC (exprCtOrigin rn_expr) GenSigCtxt (Just $ HsExprRnThing rn_expr) - app_res_rho exp_res_ty - -- Need tcSubType because of the possiblity of deep subsumption. - -- app_res_rho and exp_res_ty are both rho-types, so without - -- deep subsumption unifyExpectedType would be sufficient + if not do_ds + then -- No deep subsumption + -- app_res_rho and exp_res_ty are both rho-types, + -- so with simple subsumption we can just unify them + -- No need to zonk; the unifier does that + do { co <- unifyExpectedType rn_expr app_res_rho exp_res_ty + ; return (mkWpCastN co) } + + else -- Deep subsumption + -- Even though both app_res_rho and exp_res_ty are rho-types, + -- they may have nested polymorphism, so if deep subsumption + -- is on we must call tcSubType. + -- Zonk app_res_rho first, becuase QL may have instantiated some + -- delta variables to polytypes, and tcSubType doesn't expect that + do { app_res_rho <- zonkQuickLook do_ql app_res_rho + ; tcSubTypeDS rn_expr app_res_rho exp_res_ty } -- Typecheck the value arguments ; tc_args <- tcValArgs do_ql inst_args @@ -388,7 +403,6 @@ tcApp rn_expr exp_res_ty -------------------- wantQuickLook :: HsExpr GhcRn -> TcM Bool --- GHC switches on impredicativity all the time for ($) wantQuickLook (HsVar _ (L _ f)) | getUnique f `elem` quickLookKeys = return True wantQuickLook _ = xoptM LangExt.ImpredicativeTypes diff --git a/compiler/GHC/Tc/Utils/Unify.hs b/compiler/GHC/Tc/Utils/Unify.hs index 9f85e04244..91b0d5015e 100644 --- a/compiler/GHC/Tc/Utils/Unify.hs +++ b/compiler/GHC/Tc/Utils/Unify.hs @@ -15,7 +15,7 @@ module GHC.Tc.Utils.Unify ( -- Full-blown subsumption tcWrapResult, tcWrapResultO, tcWrapResultMono, tcTopSkolemise, tcSkolemiseScoped, tcSkolemiseExpType, - tcSubType, tcSubTypeNC, tcSubTypeSigma, tcSubTypePat, + tcSubType, tcSubTypeSigma, tcSubTypePat, tcSubTypeDS, tcSubTypeAmbiguity, tcSubMult, checkConstraints, checkTvConstraints, buildImplicationFor, buildTvImplication, emitResidualTvConstraint, @@ -853,6 +853,24 @@ tcSubType orig ctxt ty_actual ty_expected do { traceTc "tcSubType" (vcat [pprUserTypeCtxt ctxt, ppr ty_actual, ppr ty_expected]) ; tcSubTypeNC orig ctxt Nothing ty_actual ty_expected } +--------------- +tcSubTypeDS :: HsExpr GhcRn + -> TcRhoType -- Actual -- a rho-type not a sigma-type + -> ExpRhoType -- Expected + -> TcM HsWrapper +-- Similar signature to unifyExpectedType; does deep subsumption +-- Only one call site, in GHC.Tc.Gen.App.tcApp +tcSubTypeDS rn_expr act_rho res_ty + = case res_ty of + Check exp_rho -> tc_sub_type_deep (unifyType m_thing) orig + GenSigCtxt act_rho exp_rho + + Infer inf_res -> do { co <- fillInferResult act_rho inf_res + ; return (mkWpCastN co) } + where + orig = exprCtOrigin rn_expr + m_thing = Just (HsExprRnThing rn_expr) + --------------- tcSubTypeNC :: CtOrigin -- ^ Used when instantiating -> UserTypeCtxt -- ^ Used when skolemising @@ -1154,7 +1172,7 @@ The effects are in these main places: signatures (e.g. f :: ty; f = e), we must deeply skolemise the type; see the call to tcDeeplySkolemise in tcSkolemiseScoped. -4. In GHC.Tc.Gen.App.tcApp we call tcSubTypeNC to match the result +4. In GHC.Tc.Gen.App.tcApp we call tcSubTypeDS to match the result type. Without deep subsumption, unifyExpectedType would be sufficent. In all these cases note that the deep skolemisation must be done /first/. -- cgit v1.2.1