Implement DeepSubsumption

This MR adds the language extension -XDeepSubsumption, implementing
GHC proposal #511.  This change mitigates the impact of GHC proposal

The changes are highly localised, by design.  See Note [Deep subsumption]
in GHC.Tc.Utils.Unify.

The main changes are:

* Add -XDeepSubsumption, which is on by default in Haskell98 and Haskell2010,
  but off in Haskell2021.

  -XDeepSubsumption largely restores the behaviour before the "simple subsumption" change.
  -XDeepSubsumpition has a similar flavour as -XNoMonoLocalBinds:
  it makes type inference more complicated and less predictable, but it
  may be convenient in practice.

* The main changes are in:
  * GHC.Tc.Utils.Unify.tcSubType, which does deep susumption and eta-expanansion
  * GHC.Tc.Utils.Unify.tcSkolemiseET, which does deep skolemisation
  * In GHC.Tc.Gen.App.tcApp we call tcSubTypeNC to match the result
    type. Without deep subsumption, unifyExpectedType would be sufficent.

  See Note [Deep subsumption] in GHC.Tc.Utils.Unify.

* There are no changes to Quick Look at all.

* The type of `withDict` becomes ambiguous; so add -XAllowAmbiguousTypes to
  GHC.Magic.Dict

* I fixed a small but egregious bug in GHC.Core.FVs.varTypeTyCoFVs, where
  we'd forgotten to take the free vars of the multiplicity of an Id.

(cherry picked from commit 7b9be6c8b94b3c2eb3441febb4a8005a03fa34a5)

24 files changed, 756 insertions, 177 deletions

diff --git a/compiler/GHC/Core/FVs.hs b/compiler/GHC/Core/FVs.hs
index e4663ad075..1565af9f56 100644
--- a/compiler/GHC/Core/FVs.hs
+++ b/compiler/GHC/Core/FVs.hs
@@ -622,7 +622,14 @@ dVarTypeTyCoVars :: Var -> DTyCoVarSet
 dVarTypeTyCoVars var = fvDVarSet $ varTypeTyCoFVs var
 
 varTypeTyCoFVs :: Var -> FV
-varTypeTyCoFVs var = tyCoFVsOfType (varType var)
+-- Find the free variables of a binder.
+-- In the case of ids, don't forget the multiplicity field!
+varTypeTyCoFVs var
+  = tyCoFVsOfType (varType var) `unionFV` mult_fvs
+  where
+    mult_fvs = case varMultMaybe var of
+                 Just mult -> tyCoFVsOfType mult
+                 Nothing   -> emptyFV
 
 idFreeVars :: Id -> VarSet
 idFreeVars id = assert (isId id) $ fvVarSet $ idFVs id
diff --git a/compiler/GHC/Driver/Session.hs b/compiler/GHC/Driver/Session.hs
index d7d9a62ee2..f4902df612 100644
--- a/compiler/GHC/Driver/Session.hs
+++ b/compiler/GHC/Driver/Session.hs
@@ -1380,7 +1380,8 @@ languageExtensions (Just Haskell2010)
        LangExt.PatternGuards,
        LangExt.DoAndIfThenElse,
        LangExt.FieldSelectors,
-       LangExt.RelaxedPolyRec]
+       LangExt.RelaxedPolyRec,
+       LangExt.DeepSubsumption ]
 
 languageExtensions (Just GHC2021)
     = [LangExt.ImplicitPrelude,
@@ -3715,6 +3716,7 @@ xFlagsDeps = [
   flagSpec "MagicHash"                        LangExt.MagicHash,
   flagSpec "MonadComprehensions"              LangExt.MonadComprehensions,
   flagSpec "MonoLocalBinds"                   LangExt.MonoLocalBinds,
+  flagSpec "DeepSubsumption"                  LangExt.DeepSubsumption,
   flagSpec "MonomorphismRestriction"          LangExt.MonomorphismRestriction,
   flagSpec "MultiParamTypeClasses"            LangExt.MultiParamTypeClasses,
   flagSpec "MultiWayIf"                       LangExt.MultiWayIf,
diff --git a/compiler/GHC/Tc/Gen/App.hs b/compiler/GHC/Tc/Gen/App.hs
index e72e3ed194..f594a12eca 100644
--- a/compiler/GHC/Tc/Gen/App.hs
+++ b/compiler/GHC/Tc/Gen/App.hs
@@ -372,8 +372,12 @@ tcApp rn_expr exp_res_ty
                  = addFunResCtxt rn_fun rn_args app_res_rho exp_res_ty $
                    thing_inside
 
-       ; res_co <- perhaps_add_res_ty_ctxt $
-                   unifyExpectedType rn_expr app_res_rho exp_res_ty
+       ; 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
 
        ; whenDOptM Opt_D_dump_tc_trace $
          do { inst_args <- mapM zonkArg inst_args  -- Only when tracing
@@ -396,7 +400,7 @@ tcApp rn_expr exp_res_ty
           else do return (rebuildHsApps tc_fun fun_ctxt tc_args)
 
        -- Wrap the result
-       ; return (mkHsWrapCo res_co tc_expr) }
+       ; return (mkHsWrap res_wrap tc_expr) }
 
 {-
 Note [Checking for representation-polymorphic built-ins]
diff --git a/compiler/GHC/Tc/Gen/Bind.hs b/compiler/GHC/Tc/Gen/Bind.hs
index 5a8718ea70..c75c51545f 100644
--- a/compiler/GHC/Tc/Gen/Bind.hs
+++ b/compiler/GHC/Tc/Gen/Bind.hs
@@ -606,7 +606,7 @@ tcPolyCheck prag_fn
                 tcSkolemiseScoped ctxt (idType poly_id) $ \rho_ty ->
                 -- Unwraps multiple layers; e.g
                 --    f :: forall a. Eq a => forall b. Ord b => blah
-                -- NB: tcSkolemise makes fresh type variables
+                -- NB: tcSkolemiseScoped makes fresh type variables
                 -- See Note [Instantiate sig with fresh variables]
 
                 let mono_id = mkLocalId mono_name (varMult poly_id) rho_ty in
diff --git a/compiler/GHC/Tc/Gen/Expr.hs b/compiler/GHC/Tc/Gen/Expr.hs
index f85cf4ade5..4548d66495 100644
--- a/compiler/GHC/Tc/Gen/Expr.hs
+++ b/compiler/GHC/Tc/Gen/Expr.hs
@@ -172,7 +172,7 @@ tcInferRhoNC (L loc expr)
 tcPolyExpr :: HsExpr GhcRn -> ExpSigmaType -> TcM (HsExpr GhcTc)
 tcPolyExpr expr res_ty
   = do { traceTc "tcPolyExpr" (ppr res_ty)
-       ; (wrap, expr') <- tcSkolemiseET GenSigCtxt res_ty $ \ res_ty ->
+       ; (wrap, expr') <- tcSkolemiseExpType GenSigCtxt res_ty $ \ res_ty ->
                           tcExpr expr res_ty
        ; return $ mkHsWrap wrap expr' }
 
@@ -1016,7 +1016,7 @@ tcSynArgE :: CtOrigin
            -- ^ returns a wrapper :: (type of right shape) "->" (type passed in)
 tcSynArgE orig op sigma_ty syn_ty thing_inside
   = do { (skol_wrap, (result, ty_wrapper))
-           <- tcSkolemise GenSigCtxt sigma_ty
+           <- tcTopSkolemise GenSigCtxt sigma_ty
                 (\ rho_ty -> go rho_ty syn_ty)
        ; return (result, skol_wrap <.> ty_wrapper) }
     where
diff --git a/compiler/GHC/Tc/Gen/Sig.hs b/compiler/GHC/Tc/Gen/Sig.hs
index 874870765f..2b57291dca 100644
--- a/compiler/GHC/Tc/Gen/Sig.hs
+++ b/compiler/GHC/Tc/Gen/Sig.hs
@@ -43,7 +43,7 @@ import GHC.Tc.Utils.Zonk
 import GHC.Tc.Types.Origin
 import GHC.Tc.Utils.TcType
 import GHC.Tc.Validity ( checkValidType )
-import GHC.Tc.Utils.Unify( tcSkolemise, unifyType )
+import GHC.Tc.Utils.Unify( tcTopSkolemise, unifyType )
 import GHC.Tc.Utils.Instantiate( topInstantiate, tcInstTypeBndrs )
 import GHC.Tc.Utils.Env( tcLookupId )
 import GHC.Tc.Types.Evidence( HsWrapper, (<.>) )
@@ -828,7 +828,7 @@ tcSpecWrapper :: UserTypeCtxt -> TcType -> TcType -> TcM HsWrapper
 -- See Note [Handling SPECIALISE pragmas], wrinkle 1
 tcSpecWrapper ctxt poly_ty spec_ty
   = do { (sk_wrap, inst_wrap)
-               <- tcSkolemise ctxt spec_ty $ \ spec_tau ->
+               <- tcTopSkolemise ctxt spec_ty $ \ spec_tau ->
                   do { (inst_wrap, tau) <- topInstantiate orig poly_ty
                      ; _ <- unifyType Nothing spec_tau tau
                             -- Deliberately ignore the evidence
diff --git a/compiler/GHC/Tc/TyCl/Instance.hs b/compiler/GHC/Tc/TyCl/Instance.hs
index 24802a65ea..c4b0cae497 100644
--- a/compiler/GHC/Tc/TyCl/Instance.hs
+++ b/compiler/GHC/Tc/TyCl/Instance.hs
@@ -997,7 +997,7 @@ The expected type might have a forall at the type. Normally, we
 can't skolemise in kinds because we don't have type-level lambda.
 But here, we're at the top-level of an instance declaration, so
 we actually have a place to put the regeneralised variables.
-Thus: skolemise away. cf. GHC.Tc.Utils.Unify.tcSkolemise
+Thus: skolemise away. cf. GHC.Tc.Utils.Unify.tcTopSkolemise
 Examples in indexed-types/should_compile/T12369
 
 Note [Implementing eta reduction for data families]
diff --git a/compiler/GHC/Tc/Utils/Unify.hs b/compiler/GHC/Tc/Utils/Unify.hs
index 8ffbfb959b..b18f03656a 100644
--- a/compiler/GHC/Tc/Utils/Unify.hs
+++ b/compiler/GHC/Tc/Utils/Unify.hs
@@ -14,9 +14,9 @@
 module GHC.Tc.Utils.Unify (
   -- Full-blown subsumption
   tcWrapResult, tcWrapResultO, tcWrapResultMono,
-  tcSkolemise, tcSkolemiseScoped, tcSkolemiseET,
-  tcSubType, tcSubTypeSigma, tcSubTypePat,
-  tcSubMult,
+  tcTopSkolemise, tcSkolemiseScoped, tcSkolemiseExpType,
+  tcSubType, tcSubTypeNC, tcSubTypeSigma, tcSubTypePat,
+  tcSubTypeAmbiguity, tcSubMult,
   checkConstraints, checkTvConstraints,
   buildImplicationFor, buildTvImplication, emitResidualTvConstraint,
 
@@ -55,13 +55,15 @@ import GHC.Core.Type
 import GHC.Core.Coercion
 import GHC.Core.Multiplicity
 
+import qualified GHC.LanguageExtensions as LangExt
+
 import GHC.Tc.Types.Evidence
 import GHC.Tc.Types.Constraint
 import GHC.Tc.Types.Origin
-import GHC.Types.Name( isSystemName )
 
 import GHC.Core.TyCon
 import GHC.Builtin.Types
+import GHC.Types.Name( Name, isSystemName )
 import GHC.Types.Var as Var
 import GHC.Types.Var.Set
 import GHC.Types.Var.Env
@@ -69,6 +71,7 @@ import GHC.Utils.Error
 import GHC.Driver.Session
 import GHC.Types.Basic
 import GHC.Data.Bag
+import GHC.Data.FastString( fsLit )
 import GHC.Utils.Misc
 import GHC.Utils.Outputable as Outputable
 import GHC.Utils.Panic
@@ -76,7 +79,6 @@ import GHC.Utils.Panic.Plain
 
 import GHC.Exts      ( inline )
 import Control.Monad
-import Control.Arrow ( second )
 import qualified Data.Semigroup as S ( (<>) )
 
 {- *********************************************************************
@@ -381,7 +383,7 @@ matchExpectedFunTys herald ctx arity orig_ty thing_inside
     go acc_arg_tys n ty
       | (tvs, theta, _) <- tcSplitSigmaTy ty
       , not (null tvs && null theta)
-      = do { (wrap_gen, (wrap_res, result)) <- tcSkolemise ctx ty $ \ty' ->
+      = do { (wrap_gen, (wrap_res, result)) <- tcTopSkolemise ctx ty $ \ty' ->
                                                go acc_arg_tys n ty'
            ; return (wrap_gen <.> wrap_res, result) }
 
@@ -758,9 +760,36 @@ It returns a wrapper function
         co_fn :: actual_ty ~ expected_ty
 which takes an HsExpr of type actual_ty into one of type
 expected_ty.
+
+Note [Ambiguity check and deep subsumption]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+   f :: (forall b. Eq b => a -> a) -> Int
+
+Does `f` have an ambiguous type?   The ambiguity check usually checks
+that this definition of f' would typecheck, where f' has the exact same
+type as f:
+   f' :: (forall b. Eq b => a -> a) -> Intp
+   f' = f
+
+This will be /rejected/ with DeepSubsumption but /accepted/ with
+ShallowSubsumption.  On the other hand, this eta-expanded version f''
+would be rejected both ways:
+   f'' :: (forall b. Eq b => a -> a) -> Intp
+   f'' x = f x
+
+This is squishy in the same way as other examples in GHC.Tc.Validity
+Note [The squishiness of the ambiguity check]
+
+The situation in June 2022.  Since we have SimpleSubsumption at the moment,
+we don't want introduce new breakage if you add -XDeepSubsumption, by
+rejecting types as ambiguous that weren't ambiguous before.  So, as a
+holding decision, we /always/ use SimpleSubsumption for the ambiguity check
+(erring on the side accepting more programs). Hence tcSubTypeAmbiguity.
 -}
 
 
+
 -----------------
 -- tcWrapResult needs both un-type-checked (for origins and error messages)
 -- and type-checked (for wrapping) expressions
@@ -824,6 +853,7 @@ 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 }
 
+---------------
 tcSubTypeNC :: CtOrigin          -- ^ Used when instantiating
             -> UserTypeCtxt      -- ^ Used when skolemising
             -> Maybe TypedThing -- ^ The expression that has type 'actual' (if known)
@@ -840,6 +870,47 @@ tcSubTypeNC inst_orig ctxt m_thing ty_actual res_ty
                           ; co <- fillInferResult rho inf_res
                           ; return (mkWpCastN co <.> wrap) }
 
+---------------
+tcSubTypeSigma :: CtOrigin       -- where did the actual type arise / why are we
+                                 -- doing this subtype check?
+               -> UserTypeCtxt   -- where did the expected type arise?
+               -> TcSigmaType -> TcSigmaType -> TcM HsWrapper
+-- External entry point, but no ExpTypes on either side
+-- Checks that actual <= expected
+-- Returns HsWrapper :: actual ~ expected
+tcSubTypeSigma orig ctxt ty_actual ty_expected
+  = tc_sub_type (unifyType Nothing) orig ctxt ty_actual ty_expected
+
+---------------
+tcSubTypeAmbiguity :: UserTypeCtxt   -- Where did this type arise
+                   -> TcSigmaType -> TcSigmaType -> TcM HsWrapper
+-- See Note [Ambiguity check and deep subsumption]
+tcSubTypeAmbiguity ctxt ty_actual ty_expected
+  = tc_sub_type_shallow (unifyType Nothing)
+                        (AmbiguityCheckOrigin ctxt)
+                        ctxt ty_actual ty_expected
+
+---------------
+addSubTypeCtxt :: TcType -> ExpType -> TcM a -> TcM a
+addSubTypeCtxt ty_actual ty_expected thing_inside
+ | isRhoTy ty_actual        -- If there is no polymorphism involved, the
+ , isRhoExpTy ty_expected   -- TypeEqOrigin stuff (added by the _NC functions)
+ = thing_inside             -- gives enough context by itself
+ | otherwise
+ = addErrCtxtM mk_msg thing_inside
+  where
+    mk_msg tidy_env
+      = do { (tidy_env, ty_actual)   <- zonkTidyTcType tidy_env ty_actual
+           ; ty_expected             <- readExpType ty_expected
+                   -- A worry: might not be filled if we're debugging. Ugh.
+           ; (tidy_env, ty_expected) <- zonkTidyTcType tidy_env ty_expected
+           ; let msg = vcat [ hang (text "When checking that:")
+                                 4 (ppr ty_actual)
+                            , nest 2 (hang (text "is more polymorphic than:")
+                                         2 (ppr ty_expected)) ]
+           ; return (tidy_env, msg) }
+
+
 {- Note [Instantiation of InferResult]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 We now always instantiate before filling in InferResult, so that
@@ -863,7 +934,7 @@ For example:
        f :: (?x :: Int) => a -> a
        g y = let ?x = 3::Int in f
    Here want to instantiate f's type so that the ?x::Int constraint
-   gets discharged by the enclosing implicit-parameter binding.
+  gets discharged by the enclosing implicit-parameter binding.
 
 3. Suppose one defines plus = (+). If we instantiate lazily, we will
    infer plus :: forall a. Num a => a -> a -> a. However, the monomorphism
@@ -878,29 +949,33 @@ command. See Note [Implementing :type] in GHC.Tc.Module.
 -}
 
 ---------------
-tcSubTypeSigma :: CtOrigin       -- where did the actual type arise / why are we
-                                 -- doing this subtype check?
-               -> UserTypeCtxt   -- where did the expected type arise?
-               -> TcSigmaType -> TcSigmaType -> TcM HsWrapper
--- External entry point, but no ExpTypes on either side
--- Checks that actual <= expected
--- Returns HsWrapper :: actual ~ expected
-tcSubTypeSigma orig ctxt ty_actual ty_expected
-  = tc_sub_type (unifyType Nothing) orig ctxt ty_actual ty_expected
-
----------------
-tc_sub_type :: (TcType -> TcType -> TcM TcCoercionN)  -- How to unify
-            -> CtOrigin       -- Used when instantiating
-            -> UserTypeCtxt   -- Used when skolemising
-            -> TcSigmaType    -- Actual; a sigma-type
-            -> TcSigmaType    -- Expected; also a sigma-type
-            -> TcM HsWrapper
+tc_sub_type, tc_sub_type_deep, tc_sub_type_shallow
+    :: (TcType -> TcType -> TcM TcCoercionN)  -- How to unify
+    -> CtOrigin       -- Used when instantiating
+    -> UserTypeCtxt   -- Used when skolemising
+    -> TcSigmaType    -- Actual; a sigma-type
+    -> TcSigmaType    -- Expected; also a sigma-type
+    -> TcM HsWrapper
 -- Checks that actual_ty is more polymorphic than expected_ty
 -- If wrap = tc_sub_type t1 t2
 --    => wrap :: t1 ~> t2
+--
+-- The "how to unify argument" is always a call to `uType TypeLevel orig`,
+-- but with different ways of constructing the CtOrigin `orig` from
+-- the argument types and context.
+
+----------------------
 tc_sub_type unify inst_orig ctxt ty_actual ty_expected
-  | definitely_poly ty_expected      -- See Note [Don't skolemise unnecessarily]
-  , not (possibly_poly ty_actual)
+  = do { deep_subsumption <- xoptM LangExt.DeepSubsumption
+       ; if deep_subsumption
+         then tc_sub_type_deep    unify inst_orig ctxt ty_actual ty_expected
+         else tc_sub_type_shallow unify inst_orig ctxt ty_actual ty_expected
+  }
+
+----------------------
+tc_sub_type_shallow unify inst_orig ctxt ty_actual ty_expected
+  | definitely_poly ty_expected   -- See Note [Don't skolemise unnecessarily]
+  , definitely_mono_shallow ty_actual
   = do { traceTc "tc_sub_type (drop to equality)" $
          vcat [ text "ty_actual   =" <+> ppr ty_actual
               , text "ty_expected =" <+> ppr ty_expected ]
@@ -913,52 +988,67 @@ tc_sub_type unify inst_orig ctxt ty_actual ty_expected
               , text "ty_expected =" <+> ppr ty_expected ]
 
        ; (sk_wrap, inner_wrap)
-           <- tcSkolemise ctxt ty_expected $ \ sk_rho ->
+           <- tcTopSkolemise ctxt ty_expected $ \ sk_rho ->
               do { (wrap, rho_a) <- topInstantiate inst_orig ty_actual
                  ; cow           <- unify rho_a sk_rho
                  ; return (mkWpCastN cow <.> wrap) }
 
        ; return (sk_wrap <.> inner_wrap) }
-  where
-    possibly_poly ty = not (isRhoTy ty)
 
-    definitely_poly ty
-      | (tvs, theta, tau) <- tcSplitSigmaTy ty
-      , (tv:_) <- tvs
-      , null theta
-      , checkTyVarEq tv tau `cterHasProblem` cteInsolubleOccurs
-      = True
-      | otherwise
-      = False
+----------------------
+tc_sub_type_deep unify inst_orig ctxt ty_actual ty_expected
+  | definitely_poly ty_expected      -- See Note [Don't skolemise unnecessarily]
+  , definitely_mono_deep ty_actual
+  = do { traceTc "tc_sub_type_deep (drop to equality)" $
+         vcat [ text "ty_actual   =" <+> ppr ty_actual
+              , text "ty_expected =" <+> ppr ty_expected ]
+       ; mkWpCastN <$>
+         unify ty_actual ty_expected }
 
-------------------------
-addSubTypeCtxt :: TcType -> ExpType -> TcM a -> TcM a
-addSubTypeCtxt ty_actual ty_expected thing_inside
- | isRhoTy ty_actual        -- If there is no polymorphism involved, the
- , isRhoExpTy ty_expected   -- TypeEqOrigin stuff (added by the _NC functions)
- = thing_inside             -- gives enough context by itself
- | otherwise
- = addErrCtxtM mk_msg thing_inside
-  where
-    mk_msg tidy_env
-      = do { (tidy_env, ty_actual)   <- zonkTidyTcType tidy_env ty_actual
-                   -- might not be filled if we're debugging. ugh.
-           ; mb_ty_expected          <- readExpType_maybe ty_expected
-           ; (tidy_env, ty_expected) <- case mb_ty_expected of
-                                          Just ty -> second mkCheckExpType <$>
-                                                     zonkTidyTcType tidy_env ty
-                                          Nothing -> return (tidy_env, ty_expected)
-           ; ty_expected             <- readExpType ty_expected
-           ; (tidy_env, ty_expected) <- zonkTidyTcType tidy_env ty_expected
-           ; let msg = vcat [ hang (text "When checking that:")
-                                 4 (ppr ty_actual)
-                            , nest 2 (hang (text "is more polymorphic than:")
-                                         2 (ppr ty_expected)) ]
-           ; return (tidy_env, msg) }
+  | otherwise   -- This is the general case
+  = do { traceTc "tc_sub_type_deep (general case)" $
+         vcat [ text "ty_actual   =" <+> ppr ty_actual
+              , text "ty_expected =" <+> ppr ty_expected ]
+
+       ; (sk_wrap, inner_wrap)
+           <- tcDeeplySkolemise ctxt ty_expected $ \ sk_rho ->
+              -- See Note [Deep subsumption]
+              tc_sub_type_ds unify inst_orig ctxt ty_actual sk_rho
+
+       ; return (sk_wrap <.> inner_wrap) }
+
+definitely_mono_shallow :: TcType -> Bool
+definitely_mono_shallow ty = isRhoTy ty
+    -- isRhoTy: no top level forall or (=>)
+
+definitely_mono_deep :: TcType -> Bool
+definitely_mono_deep ty
+  | not (definitely_mono_shallow ty)     = False
+    -- isRhoTy: False means top level forall or (=>)
+  | Just (_, res) <- tcSplitFunTy_maybe ty = definitely_mono_deep res
+    -- Top level (->)
+  | otherwise                              = True
+
+definitely_poly :: TcType -> Bool
+-- A very conservative test:
+-- see Note [Don't skolemise unnecessarily]
+definitely_poly ty
+  | (tvs, theta, tau) <- tcSplitSigmaTy ty
+  , (tv:_) <- tvs   -- At least one tyvar
+  , null theta      -- No constraints; see (DP1)
+  , checkTyVarEq tv tau `cterHasProblem` cteInsolubleOccurs
+       -- The tyvar actually occurs (DP2),
+       --     and occurs in an injective position (DP3).
+       -- Fortunately checkTyVarEq, used for the occur check,
+       -- is just what we need.
+  = True
+  | otherwise
+  = False
 
 {- Note [Don't skolemise unnecessarily]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Suppose we are trying to solve
+     ty_actual   <= ty_expected
     (Char->Char) <= (forall a. a->a)
 We could skolemise the 'forall a', and then complain
 that (Char ~ a) is insoluble; but that's a pretty obscure
@@ -966,54 +1056,25 @@ error.  It's better to say that
     (Char->Char) ~ (forall a. a->a)
 fails.
 
-So roughly:
- * if the ty_expected has an outermost forall
-      (i.e. skolemisation is the next thing we'd do)
- * and the ty_actual has no top-level polymorphism (but looking deeply)
-then we can revert to simple equality.  But we need to be careful.
-These examples are all fine:
-
- * (Char->Char) <= (forall a. Char -> Char)
-      ty_expected isn't really polymorphic
-
- * (Char->Char) <= (forall a. (a~Char) => a -> a)
-      ty_expected isn't really polymorphic
-
- * (Char->Char) <= (forall a. F [a] Char -> Char)
-                   where type instance F [x] t = t
-     ty_expected isn't really polymorphic
-
 If we prematurely go to equality we'll reject a program we should
-accept (e.g. #13752).  So the test (which is only to improve
-error message) is very conservative:
- * ty_actual is /definitely/ monomorphic
- * ty_expected is /definitely/ polymorphic
+accept (e.g. #13752).  So the test (which is only to improve error
+message) is very conservative:
 
-Note [Settting the argument context]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider we are doing the ambiguity check for the (bogus)
-  f :: (forall a b. C b => a -> a) -> Int
+ * ty_actual   is /definitely/ monomorphic: see `definitely_mono`
+   This definitely_mono test comes in "shallow" and "deep" variants
 
-We'll call
-   tcSubType ((forall a b. C b => a->a) -> Int )
-             ((forall a b. C b => a->a) -> Int )
+ * ty_expected is /definitely/ polymorphic: see `definitely_poly`
+   This definitely_poly test is more subtle than you might think.
+   Here are three cases where expected_ty looks polymorphic, but
+   isn't, and where it would be /wrong/ to switch to equality:
 
-with a UserTypeCtxt of (FunSigCtxt "f").  Then we'll do the co/contra thing
-on the argument type of the (->) -- and at that point we want to switch
-to a UserTypeCtxt of GenSigCtxt.  Why?
+   (DP1)  (Char->Char) <= (forall a. (a~Char) => a -> a)
 
-* Error messages.  If we stick with FunSigCtxt we get errors like
-     * Could not deduce: C b
-       from the context: C b0
-        bound by the type signature for:
-            f :: forall a b. C b => a->a
-  But of course f does not have that type signature!
-  Example tests: T10508, T7220a, Simple14
+   (DP2)  (Char->Char) <= (forall a. Char -> Char)
+
+   (DP3)  (Char->Char) <= (forall a. F [a] Char -> Char)
+                          where type instance F [x] t = t
 
-* Implications. We may decide to build an implication for the whole
-  ambiguity check, but we don't need one for each level within it,
-  and GHC.Tc.Utils.Unify.alwaysBuildImplication checks the UserTypeCtxt.
-  See Note [When to build an implication]
 
 Note [Wrapper returned from tcSubMult]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1066,13 +1127,304 @@ tcEqMult origin w_actual w_expected = do
 
 {- *********************************************************************
 *                                                                      *
+                    Deep subsumption
+*                                                                      *
+********************************************************************* -}
+
+{- Note [Deep subsumption]
+~~~~~~~~~~~~~~~~~~~~~~~~~~
+The DeepSubsumption extension, documented here
+
+    https://github.com/ghc-proposals/ghc-proposals/pull/511.
+
+makes a best-efforts attempt implement deep subsumption as it was
+prior to the the Simplify Subsumption proposal:
+
+    https://github.com/ghc-proposals/ghc-proposals/pull/287
+
+The effects are in these main places:
+
+1. In the subsumption check, tcSubType, we must do deep skolemisation:
+   see the call to tcDeeplySkolemise in tc_sub_type_deep
+
+2. In tcPolyExpr we must do deep skolemisation:
+   see the call to tcDeeplySkolemise in tcSkolemiseExpType
+
+3. for expression type signatures (e :: ty), and functions with type
+   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
+   type. Without deep subsumption, unifyExpectedType would be sufficent.
+
+In all these cases note that the deep skolemisation must be done /first/.
+Consider (1)
+     (forall a. Int -> a -> a)  <=  Int -> (forall b. b -> b)
+We must skolemise the `forall b` before instantiating the `forall a`.
+See also Note [Deep skolemisation].
+
+Note that we /always/ use shallow subsumption in the ambiguity check.
+See Note [Ambiguity check and deep subsumption].
+
+Note [Deep skolemisation]
+~~~~~~~~~~~~~~~~~~~~~~~~~
+deeplySkolemise decomposes and skolemises a type, returning a type
+with all its arrows visible (ie not buried under foralls)
+
+Examples:
+
+  deeplySkolemise (Int -> forall a. Ord a => blah)
+    =  ( wp, [a], [d:Ord a], Int -> blah )
+    where wp = \x:Int. /\a. \(d:Ord a). <hole> x
+
+  deeplySkolemise  (forall a. Ord a => Maybe a -> forall b. Eq b => blah)
+    =  ( wp, [a,b], [d1:Ord a,d2:Eq b], Maybe a -> blah )
+    where wp = /\a.\(d1:Ord a).\(x:Maybe a)./\b.\(d2:Ord b). <hole> x
+
+In general,
+  if      deeplySkolemise ty = (wrap, tvs, evs, rho)
+    and   e :: rho
+  then    wrap e :: ty
+    and   'wrap' binds tvs, evs
+
+ToDo: this eta-abstraction plays fast and loose with termination,
+      because it can introduce extra lambdas.  Maybe add a `seq` to
+      fix this
+
+Note [Setting the argument context]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider we are doing the ambiguity check for the (bogus)
+  f :: (forall a b. C b => a -> a) -> Int
+
+We'll call
+   tcSubType ((forall a b. C b => a->a) -> Int )
+             ((forall a b. C b => a->a) -> Int )
+
+with a UserTypeCtxt of (FunSigCtxt "f").  Then we'll do the co/contra thing
+on the argument type of the (->) -- and at that point we want to switch
+to a UserTypeCtxt of GenSigCtxt.  Why?
+
+* Error messages.  If we stick with FunSigCtxt we get errors like
+     * Could not deduce: C b
+       from the context: C b0
+        bound by the type signature for:
+            f :: forall a b. C b => a->a
+  But of course f does not have that type signature!
+  Example tests: T10508, T7220a, Simple14
+
+* Implications. We may decide to build an implication for the whole
+  ambiguity check, but we don't need one for each level within it,
+  and TcUnify.alwaysBuildImplication checks the UserTypeCtxt.
+  See Note [When to build an implication]
+
+Note [Multiplicity in deep subsumption]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+   t1 ->{mt} t2  <=   s1 ->{ms} s2
+
+At the moment we /unify/ ms~mt, via tcEqMult.
+
+Arguably we should use `tcSubMult`. But then if mt=m0 (a unification
+variable) and ms=Many, `tcSubMult` is a no-op (since anything is a
+sub-multiplicty of Many).  But then `m0` may never get unified with
+anything.  It is then skolemised by the zonker; see GHC.HsToCore.Binds
+Note [Free tyvars on rule LHS].  So we in RULE foldr/app in GHC.Base
+we get this
+
+ "foldr/app"     [1] forall ys m1 m2. foldr (\x{m1} \xs{m2}. (:) x xs) ys
+                                       = \xs -> xs ++ ys
+
+where we eta-expanded that (:).  But now foldr expects an argument
+with ->{Many} and gets an argument with ->{m1} or ->{m2}, and Lint
+complains.
+
+The easiest solution was to use tcEqMult in tc_sub_type_ds, and
+insist on equality. This is only in the DeepSubsumption code anyway.
+-}
+
+tc_sub_type_ds :: (TcType -> TcType -> TcM TcCoercionN)  -- How to unify
+               -> CtOrigin       -- Used when instantiating
+               -> UserTypeCtxt   -- Used when skolemising
+               -> TcSigmaType    -- Actual; a sigma-type
+               -> TcRhoType      -- Expected; deeply skolemised
+               -> TcM HsWrapper
+
+-- If wrap = tc_sub_type_ds t1 t2
+--    => wrap :: t1 ~> t2
+-- Here is where the work actually happens!
+-- Precondition: ty_expected is deeply skolemised
+
+tc_sub_type_ds unify inst_orig ctxt ty_actual ty_expected
+  = do { traceTc "tc_sub_type_ds" $
+         vcat [ text "ty_actual   =" <+> ppr ty_actual
+              , text "ty_expected =" <+> ppr ty_expected ]
+       ; go ty_actual ty_expected }
+  where
+    -- NB: 'go' is not recursive, except for doing tcView
+    go ty_a ty_e | Just ty_a' <- tcView ty_a = go ty_a' ty_e
+                 | Just ty_e' <- tcView ty_e = go ty_a  ty_e'
+
+    go (TyVarTy tv_a) ty_e
+      = do { lookup_res <- isFilledMetaTyVar_maybe tv_a
+           ; case lookup_res of
+               Just ty_a' ->
+                 do { traceTc "tc_sub_type_ds following filled meta-tyvar:"
+                        (ppr tv_a <+> text "-->" <+> ppr ty_a')
+                    ; tc_sub_type_ds unify inst_orig ctxt ty_a' ty_e }
+               Nothing -> just_unify ty_actual ty_expected }
+
+    go ty_a@(FunTy { ft_af = VisArg, ft_mult = act_mult, ft_arg = act_arg, ft_res = act_res })
+       ty_e@(FunTy { ft_af = VisArg, ft_mult = exp_mult, ft_arg = exp_arg, ft_res = exp_res })
+      | isTauTy ty_a, isTauTy ty_e         -- Short cut common case to avoid
+      = just_unify ty_actual ty_expected   -- unnecessary eta expansion
+
+      | otherwise
+      = -- This is where we do the co/contra thing, and generate a WpFun, which in turn
+        -- causes eta-expansion, which we don't like; hence encouraging NoDeepSubsumption
+        do { arg_wrap  <- tc_sub_type_deep unify given_orig GenSigCtxt exp_arg act_arg
+                          -- GenSigCtxt: See Note [Setting the argument context]
+           ; res_wrap  <- tc_sub_type_ds   unify inst_orig  ctxt       act_res exp_res
+           ; mult_wrap <- tcEqMult inst_orig act_mult exp_mult
+                          -- See Note [Multiplicity in deep subsumption]
+           ; return (mult_wrap <.>
+                     mkWpFun arg_wrap res_wrap (Scaled exp_mult exp_arg) exp_res) }
+                     -- arg_wrap :: exp_arg ~> act_arg
+                     -- res_wrap :: act-res ~> exp_res
+      where
+        given_orig = GivenOrigin (SigSkol GenSigCtxt exp_arg [])
+
+    go ty_a ty_e
+      | let (tvs, theta, _) = tcSplitSigmaTy ty_a
+      , not (null tvs && null theta)
+      = do { (in_wrap, in_rho) <- topInstantiate inst_orig ty_a
+           ; body_wrap <- tc_sub_type_ds unify inst_orig ctxt in_rho ty_e
+           ; return (body_wrap <.> in_wrap) }
+
+      | otherwise   -- Revert to unification
+      = do { -- It's still possible that ty_actual has nested foralls. Instantiate
+             -- these, as there's no way unification will succeed with them in.
+             -- See typecheck/should_compile/T11305 for an example of when this
+             -- is important. The problem is that we're checking something like
+             --  a -> forall b. b -> b     <=   alpha beta gamma
+             -- where we end up with alpha := (->)
+             (inst_wrap, rho_a) <- deeplyInstantiate inst_orig ty_actual
+           ; unify_wrap         <- just_unify rho_a ty_expected
+           ; return (unify_wrap <.> inst_wrap) }
+
+    just_unify ty_a ty_e = do { cow <- unify ty_a ty_e
+                              ; return (mkWpCastN cow) }
+
+tcDeeplySkolemise
+    :: UserTypeCtxt -> TcSigmaType
+    -> (TcType -> TcM result)
+    -> TcM (HsWrapper, result)
+        -- ^ The wrapper has type: spec_ty ~> expected_ty
+-- Just like tcTopSkolemise, but calls
+-- deeplySkolemise instead of topSkolemise
+-- See Note [Deep skolemisation]
+tcDeeplySkolemise ctxt expected_ty thing_inside
+  | isTauTy expected_ty  -- Short cut for common case
+  = do { res <- thing_inside expected_ty
+       ; return (idHsWrapper, res) }
+  | otherwise
+  = do  { -- This (unpleasant) rec block allows us to pass skol_info to deeplySkolemise;
+          -- but skol_info can't be built until we have tv_prs
+          rec { (wrap, tv_prs, given, rho_ty) <- deeplySkolemise skol_info expected_ty
+              ; skol_info <- mkSkolemInfo (SigSkol ctxt expected_ty tv_prs) }
+
+        ; traceTc "tcDeeplySkolemise" (ppr expected_ty $$ ppr rho_ty $$ ppr tv_prs)
+
+        ; let skol_tvs  = map snd tv_prs
+        ; (ev_binds, result)
+              <- checkConstraints (getSkolemInfo skol_info) skol_tvs given $
+                 thing_inside rho_ty
+
+        ; return (wrap <.> mkWpLet ev_binds, result) }
+          -- The ev_binds returned by checkConstraints is very
+          -- often empty, in which case mkWpLet is a no-op
+
+deeplySkolemise :: SkolemInfo -> TcSigmaType
+                -> TcM ( HsWrapper
+                       , [(Name,TyVar)]     -- All skolemised variables
+                       , [EvVar]            -- All "given"s
+                       , TcRhoType )
+-- See Note [Deep skolemisation]
+deeplySkolemise skol_info ty
+  = go init_subst ty
+  where
+    init_subst = mkEmptyTCvSubst (mkInScopeSet (tyCoVarsOfType ty))
+
+    go subst ty
+      | Just (arg_tys, tvs, theta, ty') <- tcDeepSplitSigmaTy_maybe ty
+      = do { let arg_tys' = substScaledTys subst arg_tys
+           ; ids1           <- newSysLocalIds (fsLit "dk") arg_tys'
+           ; (subst', tvs1) <- tcInstSkolTyVarsX skol_info subst tvs
+           ; ev_vars1       <- newEvVars (substTheta subst' theta)
+           ; (wrap, tvs_prs2, ev_vars2, rho) <- go subst' ty'
+           ; let tv_prs1 = map tyVarName tvs `zip` tvs1
+           ; return ( mkWpLams ids1
+                      <.> mkWpTyLams tvs1
+                      <.> mkWpLams ev_vars1
+                      <.> wrap
+                      <.> mkWpEvVarApps ids1
+                    , tv_prs1  ++ tvs_prs2
+                    , ev_vars1 ++ ev_vars2
+                    , mkVisFunTys arg_tys' rho ) }
+
+      | otherwise
+      = return (idHsWrapper, [], [], substTy subst ty)
+        -- substTy is a quick no-op on an empty substitution
+
+deeplyInstantiate :: CtOrigin -> TcType -> TcM (HsWrapper, Type)
+deeplyInstantiate orig ty
+  = go init_subst ty
+  where
+    init_subst = mkEmptyTCvSubst (mkInScopeSet (tyCoVarsOfType ty))
+
+    go subst ty
+      | Just (arg_tys, tvs, theta, rho) <- tcDeepSplitSigmaTy_maybe ty
+      = do { (subst', tvs') <- newMetaTyVarsX subst tvs
+           ; let arg_tys' = substScaledTys   subst' arg_tys
+                 theta'   = substTheta subst' theta
+           ; ids1  <- newSysLocalIds (fsLit "di") arg_tys'
+           ; wrap1 <- instCall orig (mkTyVarTys tvs') theta'
+           ; (wrap2, rho2) <- go subst' rho
+           ; return (mkWpLams ids1
+                        <.> wrap2
+                        <.> wrap1
+                        <.> mkWpEvVarApps ids1,
+                     mkVisFunTys arg_tys' rho2) }
+
+      | otherwise
+      = do { let ty' = substTy subst ty
+           ; return (idHsWrapper, ty') }
+
+tcDeepSplitSigmaTy_maybe
+  :: TcSigmaType -> Maybe ([Scaled TcType], [TyVar], ThetaType, TcSigmaType)
+-- Looks for a *non-trivial* quantified type, under zero or more function arrows
+-- By "non-trivial" we mean either tyvars or constraints are non-empty
+
+tcDeepSplitSigmaTy_maybe ty
+  | Just (arg_ty, res_ty)           <- tcSplitFunTy_maybe ty
+  , Just (arg_tys, tvs, theta, rho) <- tcDeepSplitSigmaTy_maybe res_ty
+  = Just (arg_ty:arg_tys, tvs, theta, rho)
+
+  | (tvs, theta, rho) <- tcSplitSigmaTy ty
+  , not (null tvs && null theta)
+  = Just ([], tvs, theta, rho)
+
+  | otherwise = Nothing
+
+
+{- *********************************************************************
+*                                                                      *
                     Generalisation
 *                                                                      *
 ********************************************************************* -}
 
 {- Note [Skolemisation]
 ~~~~~~~~~~~~~~~~~~~~~~~
-tcSkolemise takes "expected type" and strip off quantifiers to expose the
+tcTopSkolemise takes "expected type" and strip off quantifiers to expose the
 type underneath, binding the new skolems for the 'thing_inside'
 The returned 'HsWrapper' has type (specific_ty -> expected_ty).
 
@@ -1088,31 +1440,37 @@ tcSkolemiseScoped is very similar, but differs in two ways:
 
 * It deals specially with just the outer forall, bringing those type
   variables into lexical scope.  To my surprise, I found that doing
-  this unconditionally in tcSkolemise (i.e. doing it even if we don't
+  this unconditionally in tcTopSkolemise (i.e. doing it even if we don't
   need to bring the variables into lexical scope, which is harmless)
   caused a non-trivial (1%-ish) perf hit on the compiler.
 
+* It handles deep subumption, wheres tcTopSkolemise never looks under
+  function arrows.
+
 * It always calls checkConstraints, even if there are no skolem
   variables at all.  Reason: there might be nested deferred errors
   that must not be allowed to float to top level.
   See Note [When to build an implication] below.
 -}
 
-tcSkolemise, tcSkolemiseScoped
+tcTopSkolemise, tcSkolemiseScoped
     :: UserTypeCtxt -> TcSigmaType
     -> (TcType -> TcM result)
     -> TcM (HsWrapper, result)
         -- ^ The wrapper has type: spec_ty ~> expected_ty
 -- See Note [Skolemisation] for the differences between
--- tcSkolemiseScoped and tcSkolemise
+-- tcSkolemiseScoped and tcTopSkolemise
 
 tcSkolemiseScoped ctxt expected_ty thing_inside
-  = do {
-       ; rec { (wrap, tv_prs, given, rho_ty) <- topSkolemise skol_info expected_ty
-             ; let skol_tvs  = map snd tv_prs
-             ; skol_info <- mkSkolemInfo (SigSkol ctxt expected_ty tv_prs)
-       }
-
+  = do { deep_subsumption <- xoptM LangExt.DeepSubsumption
+       ; let skolemise | deep_subsumption = deeplySkolemise
+                       | otherwise        = topSkolemise
+       ; -- This (unpleasant) rec block allows us to pass skol_info to deeplySkolemise;
+         -- but skol_info can't be built until we have tv_prs
+         rec { (wrap, tv_prs, given, rho_ty) <- skolemise skol_info expected_ty
+             ; skol_info <- mkSkolemInfo (SigSkol ctxt expected_ty tv_prs) }
+
+       ; let skol_tvs = map snd tv_prs
        ; (ev_binds, res)
              <- checkConstraints (getSkolemInfo skol_info) skol_tvs given $
                 tcExtendNameTyVarEnv tv_prs               $
@@ -1120,35 +1478,35 @@ tcSkolemiseScoped ctxt expected_ty thing_inside
 
        ; return (wrap <.> mkWpLet ev_binds, res) }
 
-tcSkolemise ctxt expected_ty thing_inside
+tcTopSkolemise ctxt expected_ty thing_inside
   | isRhoTy expected_ty  -- Short cut for common case
   = do { res <- thing_inside expected_ty
        ; return (idHsWrapper, res) }
   | otherwise
-  = do  {
-        ; rec { (wrap, tv_prs, given, rho_ty) <- topSkolemise skol_info expected_ty
-
-              ; let skol_tvs  = map snd tv_prs
-              ; skol_info <- mkSkolemInfo (SigSkol ctxt expected_ty tv_prs)
-        }
+  = do { rec { (wrap, tv_prs, given, rho_ty) <- topSkolemise skol_info expected_ty
+             ; skol_info <- mkSkolemInfo (SigSkol ctxt expected_ty tv_prs) }
 
-        ; (ev_binds, result)
-              <- checkConstraints (getSkolemInfo skol_info) skol_tvs given $
-                 thing_inside rho_ty
+       ; let skol_tvs = map snd tv_prs
+       ; (ev_binds, result)
+             <- checkConstraints (getSkolemInfo skol_info) skol_tvs given $
+                thing_inside rho_ty
 
-        ; return (wrap <.> mkWpLet ev_binds, result) }
-          -- The ev_binds returned by checkConstraints is very
-          -- often empty, in which case mkWpLet is a no-op
+       ; return (wrap <.> mkWpLet ev_binds, result) }
+         -- The ev_binds returned by checkConstraints is very
+        -- often empty, in which case mkWpLet is a no-op
 
--- | Variant of 'tcSkolemise' that takes an ExpType
-tcSkolemiseET :: UserTypeCtxt -> ExpSigmaType
-              -> (ExpRhoType -> TcM result)
-              -> TcM (HsWrapper, result)
-tcSkolemiseET _ et@(Infer {}) thing_inside
+-- | Variant of 'tcTopSkolemise' that takes an ExpType
+tcSkolemiseExpType :: UserTypeCtxt -> ExpSigmaType
+                   -> (ExpRhoType -> TcM result)
+                   -> TcM (HsWrapper, result)
+tcSkolemiseExpType _ et@(Infer {}) thing_inside
   = (idHsWrapper, ) <$> thing_inside et
-tcSkolemiseET ctxt (Check ty) thing_inside
-  = tcSkolemise ctxt ty $ \rho_ty ->
-    thing_inside (mkCheckExpType rho_ty)
+tcSkolemiseExpType ctxt (Check ty) thing_inside
+  = do { deep_subsumption <- xoptM LangExt.DeepSubsumption
+       ; let skolemise | deep_subsumption = tcDeeplySkolemise
+                       | otherwise        = tcTopSkolemise
+       ; skolemise ctxt ty $ \rho_ty ->
+         thing_inside (mkCheckExpType rho_ty) }
 
 checkConstraints :: SkolemInfoAnon
                  -> [TcTyVar]           -- Skolems
@@ -1167,7 +1525,7 @@ checkConstraints skol_info skol_tvs given thing_inside
                  ; return (ev_binds, result) }
 
          else -- Fast path.  We check every function argument with tcCheckPolyExpr,
-              -- which uses tcSkolemise and hence checkConstraints.
+              -- which uses tcTopSkolemise and hence checkConstraints.
               -- So this fast path is well-exercised
               do { res <- thing_inside
                  ; return (emptyTcEvBinds, res) } }
diff --git a/compiler/GHC/Tc/Validity.hs b/compiler/GHC/Tc/Validity.hs
index 22b627a36f..cd628b5622 100644
--- a/compiler/GHC/Tc/Validity.hs
+++ b/compiler/GHC/Tc/Validity.hs
@@ -26,7 +26,7 @@ import GHC.Prelude
 import GHC.Data.Maybe
 
 -- friends:
-import GHC.Tc.Utils.Unify    ( tcSubTypeSigma )
+import GHC.Tc.Utils.Unify    ( tcSubTypeAmbiguity )
 import GHC.Tc.Solver         ( simplifyAmbiguityCheck )
 import GHC.Tc.Instance.Class ( matchGlobalInst, ClsInstResult(..), InstanceWhat(..), AssocInstInfo(..) )
 import GHC.Core.TyCo.FVs
@@ -141,7 +141,9 @@ This neatly takes account of the functional dependency stuff above,
 and implicit parameter (see Note [Implicit parameters and ambiguity]).
 And this is what checkAmbiguity does.
 
-What about this, though?
+Note [The squishiness of the ambiguity check]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+What about this?
    g :: C [a] => Int
 Is every call to 'g' ambiguous?  After all, we might have
    instance C [a] where ...
@@ -152,6 +154,17 @@ with -XFlexibleInstances we could have
 and now a call could be legal after all!  Well, we'll reject this
 unless the instance is available *here*.
 
+But even that's not quite right. Even a function with an utterly-ambiguous
+type like f :: Eq a => Int -> Int
+is still callable if you are prepared to use visible type application,
+thus (f @Bool x).
+
+In short, the ambiguity check is a good-faith attempt to say "you are likely
+to have trouble if your function has this type"; it is NOT the case that
+"you can't call this function without giving a type error".
+
+See also Note [Ambiguity check and deep subsumption] in GHC.Tc.Utils.Unify.
+
 Note [When to call checkAmbiguity]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 We call checkAmbiguity
@@ -220,7 +233,9 @@ checkAmbiguity ctxt ty
        ; allow_ambiguous <- xoptM LangExt.AllowAmbiguousTypes
        ; (_wrap, wanted) <- addErrCtxt (mk_msg allow_ambiguous) $
                             captureConstraints $
-                            tcSubTypeSigma (AmbiguityCheckOrigin ctxt) ctxt ty ty
+                            tcSubTypeAmbiguity ctxt ty ty
+                            -- See Note [Ambiguity check and deep subsumption]
+                            -- in GHC.Tc.Utils.Unify
        ; simplifyAmbiguityCheck ty wanted
 
        ; traceTc "Done ambiguity check for" (ppr ty) }
diff --git a/docs/users_guide/exts/default_signatures.rst b/docs/users_guide/exts/default_signatures.rst
index 54e995e2ce..210bbea560 100644
--- a/docs/users_guide/exts/default_signatures.rst
+++ b/docs/users_guide/exts/default_signatures.rst
@@ -88,7 +88,7 @@ default type signatures.
 
 - Ignoring outermost contexts, a default type signature must match the original
   type signature according to
-  :ref:`GHC's subsumption rules <simple-subsumption>`. As a result, the order
+  :ref:`GHC's subsumption rules <subsumption>`. As a result, the order
   of type variables in the default signature is important. Recall the ``Foo``
   example from the previous section: ::
 
@@ -122,7 +122,7 @@ default type signatures.
 
       default bar :: forall b. (C', b ~ Int) => a -> b -> b
 
-- Because of :ref:`GHC's subsumption rules <simple-subsumption>` rules, there
+- Because of :ref:`GHC's subsumption rules <subsumption>` rules, there
   are relatively tight restrictions concerning nested or higher-rank
   ``forall``\ s (see :ref:`arbitrary-rank-polymorphism`). Consider this
   class: ::
diff --git a/docs/users_guide/exts/rank_polymorphism.rst b/docs/users_guide/exts/rank_polymorphism.rst
index d91c2fae6d..75066e8c7f 100644
--- a/docs/users_guide/exts/rank_polymorphism.rst
+++ b/docs/users_guide/exts/rank_polymorphism.rst
@@ -167,7 +167,7 @@ In the function ``h`` we use the record selectors ``return`` and
 ``MonadT`` data structure, rather than using pattern matching.
 
 
-.. _simple-subsumption:
+.. _subsumption:
 
 Subsumption
 -------------
@@ -209,13 +209,39 @@ A similar phenomenon occurs for operator sections. For example,
 ``(\`g3a\` "hello")`` is not well typed, but it can be made to typecheck by eta
 expanding it to ``\x -> x \`g3a\` "hello"``.
 
-Historical note.  Earlier versions of GHC allowed these now-rejected applications, by inserting
-automatic eta-expansions, as described in Section 4.6 of `Practical type inference for arbitrary-rank types <https://www.microsoft.com/en-us/research/publication/practical-type-inference-for-arbitrary-rank-types/>`__, where it is
-called "deep skolemisation".
-But these automatic eta-expansions may silently change the semantics of the user's program,
-and deep skolemisation was removed from the language by
-`GHC Proposal #287 <https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0287-simplify-subsumption.rst>`__.
-This proposal has many more examples.
+.. extension:: DeepSubsumption
+    :shortdesc: Enable deep subsumption
+
+    :since: 9.2.4
+
+    Relax the simple subsumption rules, implicitly inserting eta-expansions
+    when matching up function types with different quantification structures.
+
+The :extension:`DeepSubsumption` extension relaxes the aforementioned requirement that
+foralls must appear in the same place. GHC will instead automatically rewrite expressions
+like ``f x`` of type ``ty1 -> ty2`` to become ``(\ (y :: ty1) -> f x y)``; this is called eta-expansion.
+See Section 4.6 of
+`Practical type inference for arbitrary-rank types <https://www.microsoft.com/en-us/research/publication/practical-type-inference-for-arbitrary-rank-types/>`__,
+where this process is called "deep skolemisation".
+
+Note that these eta-expansions may silently change the semantics of the user's program: ::
+
+  h1 :: Int -> forall a. a -> a
+  h1 = undefined
+  h2 :: forall b. Int -> b -> b
+  h2 = h1
+
+With :extension:`DeepSubsumption`, GHC will accept these definitions,
+inserting an implicit eta-expansion: ::
+
+  h2 = \ i -> h1 i
+
+This means that ``h2 `seq` ()`` will not crash, even though ``h1 `seq` ()`` does crash.
+
+Historical note: Deep skolemisation was initially removed from the language by
+`GHC Proposal #287 <https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0287-simplify-subsumption.rst>`__,
+but was re-introduced as part of the :extension:`DeepSubsumption` extension following
+`GHC Proposal #511 <https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0511-deep-subsumption.rst>`__.
 
 .. _higher-rank-type-inference:
 
diff --git a/libraries/ghc-boot-th/GHC/LanguageExtensions/Type.hs b/libraries/ghc-boot-th/GHC/LanguageExtensions/Type.hs
index ce07116a1e..76b20bed35 100644
--- a/libraries/ghc-boot-th/GHC/LanguageExtensions/Type.hs
+++ b/libraries/ghc-boot-th/GHC/LanguageExtensions/Type.hs
@@ -30,6 +30,7 @@ data Extension
    | UndecidableSuperClasses
    | MonomorphismRestriction
    | MonoLocalBinds
+   | DeepSubsumption
    | RelaxedPolyRec           -- Deprecated
    | ExtendedDefaultRules     -- Use GHC's extended rules for defaulting
    | ForeignFunctionInterface
diff --git a/libraries/ghc-prim/GHC/Magic/Dict.hs b/libraries/ghc-prim/GHC/Magic/Dict.hs
index 560ab3956f..34886fee3b 100644
--- a/libraries/ghc-prim/GHC/Magic/Dict.hs
+++ b/libraries/ghc-prim/GHC/Magic/Dict.hs
@@ -5,6 +5,7 @@
 {-# LANGUAGE NoImplicitPrelude #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE AllowAmbiguousTypes #-}  -- See Note [withDict has an ambiguous type]
 {-# LANGUAGE Unsafe #-}
 
 -----------------------------------------------------------------------------
@@ -40,3 +41,20 @@ import GHC.Types (RuntimeRep, TYPE)
 -- @Note [withDict]@ in "GHC.Tc.Instance.Class" in GHC.
 class WithDict cls meth where
   withDict :: forall {rr :: RuntimeRep} (r :: TYPE rr). meth -> (cls => r) -> r
+
+{- Note [withDict has an ambiguous type]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The type of `withDict` is ambiguous.  Consider
+   foo :: forall cls meth. WithDict cls meth
+       => forall rr (r::rr). meth -> (cls => r) -> r
+   foo m k = withDict m k
+
+If we instantiate `withDict` with fresh unification variables, including cls0 for cls,
+there is nothing that forces the `cls` Wanted from the call to `k` to unify with the
+`cls0` Given from the call to `withDict`.  You have to give it a class argument:
+
+   foo m k = withDict @cls m k
+
+That's fine.  But it means we need -XAllowAmbiguousTypes for the withDict definition,
+at least with deep subsumption.
+-}
\ No newline at end of file
diff --git a/testsuite/tests/driver/T4437.hs b/testsuite/tests/driver/T4437.hs
index 02af5d8b63..c25c3b7f1c 100644
--- a/testsuite/tests/driver/T4437.hs
+++ b/testsuite/tests/driver/T4437.hs
@@ -37,7 +37,8 @@ check title expected got
 -- See Note [Adding a language extension] in compiler/GHC/Driver/Session.hs.
 expectedGhcOnlyExtensions :: [String]
 expectedGhcOnlyExtensions =
-    [ ]
+    [ "DeepSubsumption"
+    ]
 
 expectedCabalOnlyExtensions :: [String]
 expectedCabalOnlyExtensions = ["Generics",
diff --git a/testsuite/tests/indexed-types/should_compile/Simple14.hs b/testsuite/tests/indexed-types/should_compile/Simple14.hs
index bedf5bb3e7..a1b2e5eaca 100644
--- a/testsuite/tests/indexed-types/should_compile/Simple14.hs
+++ b/testsuite/tests/indexed-types/should_compile/Simple14.hs
@@ -1,5 +1,6 @@
 {-# LANGUAGE Haskell2010 #-}
 {-# LANGUAGE TypeFamilies, RankNTypes, FlexibleContexts, ScopedTypeVariables #-}
+{-# LANGUAGE AllowAmbiguousTypes #-}
 
 module Simple14 where
 
@@ -7,6 +8,7 @@ data EQ_ x y = EQ_
 
 -- Nov 2014: actually eqE has an ambiguous type
 -- Apr 2020: now it doesn't again
+-- Jun 2022: now it does again -- because of DeepSubsumption
 eqE :: EQ_ x y -> (x~y => EQ_ z z) -> p
 eqE x y = error "eqE"
 
diff --git a/testsuite/tests/indexed-types/should_compile/Simple14.stderr b/testsuite/tests/indexed-types/should_compile/Simple14.stderr
index 7489ffce5a..c9c83b6434 100644
--- a/testsuite/tests/indexed-types/should_compile/Simple14.stderr
+++ b/testsuite/tests/indexed-types/should_compile/Simple14.stderr
@@ -1,21 +1,21 @@
 
-Simple14.hs:20:27: error:
+Simple14.hs:22:27: error:
     • Couldn't match type ‘z0’ with ‘n’
       Expected: EQ_ z0 z0
         Actual: EQ_ m n
-        ‘z0’ is untouchable
-          inside the constraints: Maybe m ~ Maybe n
-          bound by a type expected by the context:
-                     (Maybe m ~ Maybe n) => EQ_ z0 z0
-          at Simple14.hs:20:26-41
+    • ‘z0’ is untouchable
+        inside the constraints: Maybe m ~ Maybe n
+        bound by a type expected by the context:
+                   (Maybe m ~ Maybe n) => EQ_ z0 z0
+        at Simple14.hs:22:26-41
       ‘n’ is a rigid type variable bound by
         the type signature for:
           foo :: forall m n. EQ_ (Maybe m) (Maybe n)
-        at Simple14.hs:19:1-42
+        at Simple14.hs:21:1-42
     • In the second argument of ‘eqE’, namely ‘(eqI :: EQ_ m n)’
       In the expression: x `eqE` (eqI :: EQ_ m n)
       In the first argument of ‘ntI’, namely
         ‘(\ x -> x `eqE` (eqI :: EQ_ m n))’
     • Relevant bindings include
-        x :: EQ_ (Maybe m) (Maybe n) (bound at Simple14.hs:20:13)
-        foo :: EQ_ (Maybe m) (Maybe n) (bound at Simple14.hs:20:1)
+        x :: EQ_ (Maybe m) (Maybe n) (bound at Simple14.hs:22:13)
+        foo :: EQ_ (Maybe m) (Maybe n) (bound at Simple14.hs:22:1)
diff --git a/testsuite/tests/simplCore/should_compile/rule2.stderr b/testsuite/tests/simplCore/should_compile/rule2.stderr
index 7a27514454..3c108d8e71 100644
--- a/testsuite/tests/simplCore/should_compile/rule2.stderr
+++ b/testsuite/tests/simplCore/should_compile/rule2.stderr
@@ -10,19 +10,22 @@
 
 
 ==================== Grand total simplifier statistics ====================
-Total ticks:     10
+Total ticks:     12
 
-1 PreInlineUnconditionally 1 f
+2 PreInlineUnconditionally
+  1 f
+  1 ds
 1 UnfoldingDone 1 Roman.bar
 1 RuleFired 1 foo/bar
 1 LetFloatFromLet 1
-6 BetaReduction
+7 BetaReduction
   1 f
   1 a
   1 m
   1 m
   1 b
   1 m
+  1 ds
 8 SimplifierDone 8
 
 
diff --git a/testsuite/tests/typecheck/should_compile/DeepSubsumption01.hs b/testsuite/tests/typecheck/should_compile/DeepSubsumption01.hs
new file mode 100644
index 0000000000..d07525b7eb
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/DeepSubsumption01.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE DeriveAnyClass #-}
+{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE DeepSubsumption #-}
+module Repro where
+
+import GHC.Generics
+import Data.Binary
+
+data FFIType
+  = FFIVoid
+  deriving (Show, Generic, Binary)
diff --git a/testsuite/tests/typecheck/should_compile/DeepSubsumption02.hs b/testsuite/tests/typecheck/should_compile/DeepSubsumption02.hs
new file mode 100644
index 0000000000..fe8be78f38
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/DeepSubsumption02.hs
@@ -0,0 +1,73 @@
+{-# LANGUAGE BangPatterns, Rank2Types, FlexibleContexts, LambdaCase, DeepSubsumption #-}
+module DeepSubsumption02 where
+
+import Data.Semigroup
+
+-- | Finite source
+type Source r s = Tap r (Maybe s)
+
+newtype Sink t m a = Sink
+  { unSink :: forall r. t m -> (a -> t m -> m r) -> m r }
+
+-- | Mono in/out
+type Converter p q r s m = Source r s (Sink (Source p q) m)
+
+type Pipe a b m = forall r. (Monoid r, Semigroup r) => Converter r a r b m
+
+newtype Tap r s m = Tap { unTap :: r -> m (s, Tap r s m) }
+
+type Distiller tap r s m = Tap r s (Sink tap m)
+
+filter :: Monad m => (a -> Bool) -> Pipe a a m
+--filter f = filtering $ maybe True f
+filter = filtering . maybe True
+{-# INLINE filter #-}
+
+mapAccum :: Monad m => (s -> a -> (s, b)) -> s -> Pipe a b m
+--mapAccum f x = go x where
+mapAccum f = go where
+  go s = reservingTap $ \case
+    Just a -> let (s', b) = f s a in return (Just b, go s')
+    Nothing -> return (Nothing, go s)
+{-# INLINE mapAccum #-}
+
+traverse :: (Monad m) => (a -> m b) -> Pipe a b m
+-- traverse f = traversing $ Prelude.traverse f
+traverse = traversing . Prelude.traverse
+{-# INLINE traverse #-}
+
+-- | Get one element preserving a request
+reservingTap :: Monad m => (a -> Sink (Tap r a) m (b, Distiller (Tap r a) r b m)) -> Distiller (Tap r a) r b m
+reservingTap k = Tap $ \r -> Sink $ \t cont -> do
+  (a, t') <- unTap t r
+  unSink (k a) t' cont
+{-# INLINE reservingTap #-}
+
+traversing :: (Monad m) => (a -> m b) -> Distiller (Tap r a) r b m
+traversing f = go where
+  go = reservingTap $ \a -> do
+    b <- undefined $ f a
+    return (b, go)
+{-# INLINE traversing #-}
+
+filtering :: (Monoid r, Monad m) => (a -> Bool) -> Distiller (Tap r a) r a m
+filtering f = go where
+  go = reservingTap $ \a -> if f a
+    then return (a, go)
+    else unTap go mempty
+{-# INLINE filtering #-}
+
+instance Functor (Sink s m) where
+  fmap f m = Sink $ \s k -> unSink m s (k . f)
+
+instance Applicative (Sink s m) where
+  pure a = Sink $ \s k -> k a s
+  Sink mf <*> Sink mx = Sink
+    $ \s k -> mf s $ \f s' -> mx s' $ k . f
+  m *> k = m >>= \_ -> k
+
+instance Monad (Sink s m) where
+  return = pure
+  {-# INLINE return #-}
+  m >>= k = Sink $ \s cont -> unSink m s $ \a s' -> unSink (k a) s' cont
+
diff --git a/testsuite/tests/typecheck/should_compile/DeepSubsumption03.hs b/testsuite/tests/typecheck/should_compile/DeepSubsumption03.hs
new file mode 100644
index 0000000000..8f8c465047
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/DeepSubsumption03.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE DeepSubsumption #-}
+{-# LANGUAGE NoPolyKinds #-}
+module DeepSubsumption03 where
+
+class Profunctor p where
+  dimap :: (s -> a) -> (b -> t) -> p i a b -> p i s t
+
+type Iso s t a b = forall p i . Profunctor p => p i a b -> p i s t
+
+iso :: (s -> a) -> (b -> t) -> Iso s t a b
+-- iso f g = dimap f g
+iso = dimap
diff --git a/testsuite/tests/typecheck/should_compile/DeepSubsumption04.hs b/testsuite/tests/typecheck/should_compile/DeepSubsumption04.hs
new file mode 100644
index 0000000000..abaf8d569b
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/DeepSubsumption04.hs
@@ -0,0 +1,29 @@
+{-# LANGUAGE DeepSubsumption #-}
+{-# LANGUAGE KindSignatures #-}
+module DeepSubsumption04 where
+
+import Data.Kind
+
+data TermOutput = TermOutput
+
+type TermAction = () -> TermOutput
+
+type ActionT = WriterT TermAction
+
+class MonadReader r m  where
+  ask :: m r
+
+data WriterT w (m :: Type -> Type) a = WriterT
+
+type ActionM a = forall m . (MonadReader () m) => ActionT m a
+
+output :: TermAction -> ActionM ()
+output t = undefined
+
+termText :: String -> TermOutput
+termText = undefined
+
+outputText :: String -> ActionM ()
+outputText = output . const . termText
+--outputText x = output . const . termText $ x
+
diff --git a/testsuite/tests/typecheck/should_compile/T21548a.hs b/testsuite/tests/typecheck/should_compile/T21548a.hs
new file mode 100644
index 0000000000..399f3e5386
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T21548a.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE RankNTypes, DeepSubsumption #-}
+
+module T21548a where
+
+f1 :: (forall a. a -> forall b. b -> b) -> Int
+f1 = f1
+
+g1 :: forall p q. p -> q -> q
+g1 = g1
+
+foo1 = f1 g1
+
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index d252f2216f..641133efb1 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -831,3 +831,8 @@ test('T21328', normal, compile, [''])
 test('T21516', normal, compile, [''])
 test('T21519', normal, compile, [''])
 test('T21519a', normal, compile, [''])
+test('T21548a', normal, compile, [''])
+test('DeepSubsumption01', normal, compile, [''])
+test('DeepSubsumption02', normal, compile, [''])
+test('DeepSubsumption03', normal, compile, [''])
+test('DeepSubsumption04', normal, compile, [''])
diff --git a/testsuite/tests/typecheck/should_fail/T14618.stderr b/testsuite/tests/typecheck/should_fail/T14618.stderr
index 05a763048e..6cf768bbce 100644
--- a/testsuite/tests/typecheck/should_fail/T14618.stderr
+++ b/testsuite/tests/typecheck/should_fail/T14618.stderr
@@ -1,10 +1,10 @@
 
 T14618.hs:7:14: error:
-    • Couldn't match type ‘b’ with ‘forall c. a’
-      Expected: a -> b
-        Actual: a -> forall c. a
-      Cannot equate type variable ‘b’
-      with a type involving polytypes: forall c. a
+    • Couldn't match expected type ‘b’ with actual type ‘a’
+      ‘a’ is a rigid type variable bound by
+        the type signature for:
+          safeCoerce :: forall a b. a -> b
+        at T14618.hs:6:1-20
       ‘b’ is a rigid type variable bound by
         the type signature for:
           safeCoerce :: forall a b. a -> b