Fix the interaction of operator sections and deep subsumption

Fixes DeepSubsumption08

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/.