diff options
author | Simon Peyton Jones <simon.peytonjones@gmail.com> | 2022-07-21 23:56:32 +0100 |
---|---|---|
committer | Zubin Duggal <zubin.duggal@gmail.com> | 2022-07-26 16:28:48 +0530 |
commit | c1e9dc7c75c3f596fe6dde3c2d8631ef67856126 (patch) | |
tree | 2af604ae2968d74348013338cc8de9753e594890 | |
parent | a989d1a2a3110eb7614828320a3877c774de2227 (diff) | |
download | haskell-c1e9dc7c75c3f596fe6dde3c2d8631ef67856126.tar.gz |
Fix the interaction of operator sections and deep subsumption
Fixes DeepSubsumption08
(cherry picked from commit 5e93a9521fc2220ee6f4f150c6681f84f33a2134)
-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 | 25 |
3 files changed, 53 insertions, 8 deletions
diff --git a/compiler/GHC/Rename/Expr.hs b/compiler/GHC/Rename/Expr.hs index 0a2289bdc4..7aa57929c6 100644 --- a/compiler/GHC/Rename/Expr.hs +++ b/compiler/GHC/Rename/Expr.hs @@ -649,6 +649,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 4182f1c0de..6d081b288b 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] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -349,12 +350,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 $ ppr 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 } ; whenDOptM Opt_D_dump_tc_trace $ do { inst_args <- mapM zonkArg inst_args -- Only when tracing @@ -380,7 +395,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 f1426389e3..5b0bdac84e 100644 --- a/compiler/GHC/Tc/Utils/Unify.hs +++ b/compiler/GHC/Tc/Utils/Unify.hs @@ -17,7 +17,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, @@ -611,6 +611,27 @@ 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 -> do { dflags <- getDynFlags + ; tc_sub_type_deep dflags (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 (ppr rn_expr) + +--------------- tcSubTypeNC :: CtOrigin -- ^ Used when instantiating -> UserTypeCtxt -- ^ Used when skolemising -> Maybe SDoc -- ^ The expression that has type 'actual' (if known) @@ -914,7 +935,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/. |