diff options
author | Simon Peyton Jones <simon.peytonjones@gmail.com> | 2022-07-21 23:56:32 +0100 |
---|---|---|
committer | Marge Bot <ben+marge-bot@smart-cactus.org> | 2022-07-25 09:42:01 -0400 |
commit | 5e93a9521fc2220ee6f4f150c6681f84f33a2134 (patch) | |
tree | 7c8889a8bda1dd0ba974ade8f2c986a0456a28ad | |
parent | 671899858585376dcbbbdc3740dad4b8ec7b6a70 (diff) | |
download | haskell-5e93a9521fc2220ee6f4f150c6681f84f33a2134.tar.gz |
Fix the interaction of operator sections and deep subsumption
Fixes DeepSubsumption08
-rw-r--r-- | compiler/GHC/Rename/Expr.hs | 10 | ||||
-rw-r--r-- | compiler/GHC/Tc/Gen/App.hs | 26 | ||||
-rw-r--r-- | 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, @@ -854,6 +854,24 @@ tcSubType orig ctxt ty_actual 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 -> Maybe TypedThing -- ^ The expression that has type 'actual' (if known) @@ -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/. |