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.

* I also had to fix tcSplitNestedSigmaTys

  When I did the shallow-subsumption patch
    commit 2b792facab46f7cdd09d12e79499f4e0dcd4293f
    Date:   Sun Feb 2 18:23:11 2020 +0000
    Simple subsumption

  I changed tcSplitNestedSigmaTys to not look through function arrows
  any more.  But that was actually an un-forced change.  This function
  is used only in

  * Improving error messages in GHC.Tc.Gen.Head.addFunResCtxt
  * Validity checking for default methods: GHC.Tc.TyCl.checkValidClass
  * A couple of calls in the GHCi debugger: GHC.Runtime.Heap.Inspect

  All to do with validity checking and error messages. Acutally its
  fine to look under function arrows here, and quite useful a test
  DeepSubsumption05 (a test motivated by a build failure in the
  `lens` package) shows.

  The fix is easy.  I added Note [tcSplitNestedSigmaTys].

29 files changed, 841 insertions, 202 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 ef7a7bdd08..ffcad74cae 100644
--- a/compiler/GHC/Driver/Session.hs
+++ b/compiler/GHC/Driver/Session.hs
@@ -1360,7 +1360,8 @@ languageExtensions (Just Haskell2010)
        LangExt.PatternGuards,
        LangExt.DoAndIfThenElse,
        LangExt.FieldSelectors,
-       LangExt.RelaxedPolyRec]
+       LangExt.RelaxedPolyRec,
+       LangExt.DeepSubsumption ]
 
 languageExtensions (Just GHC2021)
     = [LangExt.ImplicitPrelude,
@@ -3677,6 +3678,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 f037d7f9d7..69a077c15b 100644
--- a/compiler/GHC/Tc/Gen/App.hs
+++ b/compiler/GHC/Tc/Gen/App.hs
@@ -352,8 +352,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
 
        -- Typecheck the value arguments
        ; tc_args <- tcValArgs do_ql inst_args
@@ -380,7 +384,7 @@ tcApp rn_expr exp_res_ty
                                       , text "tc_expr:"     <+> ppr tc_expr ]) }
 
        -- Wrap the result
-       ; return (mkHsWrapCo res_co tc_expr) }
+       ; return (mkHsWrap res_wrap tc_expr) }
 
 --------------------
 wantQuickLook :: HsExpr GhcRn -> TcM Bool
diff --git a/compiler/GHC/Tc/Gen/Bind.hs b/compiler/GHC/Tc/Gen/Bind.hs
index 21d1424317..6d960adddf 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 cb7f5cfb56..204114bb5b 100644
--- a/compiler/GHC/Tc/Gen/Expr.hs
+++ b/compiler/GHC/Tc/Gen/Expr.hs
@@ -176,7 +176,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' }
 
@@ -732,7 +732,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/Head.hs b/compiler/GHC/Tc/Gen/Head.hs
index a56b9c833e..1c72c877ab 100644
--- a/compiler/GHC/Tc/Gen/Head.hs
+++ b/compiler/GHC/Tc/Gen/Head.hs
@@ -1402,9 +1402,9 @@ addFunResCtxt fun args fun_res_ty env_ty thing_inside
            ; let -- See Note [Splitting nested sigma types in mismatched
                  --           function types]
                  (_, _, fun_tau) = tcSplitNestedSigmaTys fun_res'
-                 -- No need to call tcSplitNestedSigmaTys here, since env_ty is
-                 -- an ExpRhoTy, i.e., it's already instantiated.
-                 (_, _, env_tau) = tcSplitSigmaTy env'
+                 (_, _, env_tau) = tcSplitNestedSigmaTys env'
+                     -- env_ty is an ExpRhoTy, but with simple subsumption it
+                     -- is not deeply skolemised, so still use tcSplitNestedSigmaTys
                  (args_fun, res_fun) = tcSplitFunTys fun_tau
                  (args_env, res_env) = tcSplitFunTys env_tau
                  n_fun = length args_fun
@@ -1451,7 +1451,7 @@ Previously, GHC computed the number of argument types through tcSplitSigmaTy.
 This is incorrect in the face of nested foralls, however!
 This caused Ticket #13311, for instance:
 
-  f :: forall a. (Monoid a) => forall b. (Monoid b) => Maybe a -> Maybe b
+  f :: forall a. (Monoid a) => Int -> forall b. (Monoid b) => Maybe a -> Maybe b
 
 If one uses `f` like so:
 
@@ -1462,7 +1462,7 @@ Then tcSplitSigmaTy will decompose the type of `f` into:
   Tyvars: [a]
   Context: (Monoid a)
   Argument types: []
-  Return type: forall b. Monoid b => Maybe a -> Maybe b
+  Return type: Int -> forall b. Monoid b => Maybe a -> Maybe b
 
 That is, it will conclude that there are *no* argument types, and since `f`
 was given no arguments, it won't print a helpful error message. On the other
@@ -1470,11 +1470,15 @@ hand, tcSplitNestedSigmaTys correctly decomposes `f`'s type down to:
 
   Tyvars: [a, b]
   Context: (Monoid a, Monoid b)
-  Argument types: [Maybe a]
+  Argument types: [Int, Maybe a]
   Return type: Maybe b
 
 So now GHC recognizes that `f` has one more argument type than it was actually
 provided.
+
+Notice that tcSplitNestedSigmaTys looks through function arrows too, regardless
+of simple/deep subsumption.  Here we are concerned only whether there is a
+mis-match in the number of value arguments.
 -}
 
 
diff --git a/compiler/GHC/Tc/Gen/Sig.hs b/compiler/GHC/Tc/Gen/Sig.hs
index ce5e3bd394..4bb9a8038d 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, (<.>) )
@@ -819,7 +819,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.hs b/compiler/GHC/Tc/TyCl.hs
index 52473f3d93..87580c1865 100644
--- a/compiler/GHC/Tc/TyCl.hs
+++ b/compiler/GHC/Tc/TyCl.hs
@@ -4903,6 +4903,31 @@ Note that when checking whether two type signatures match, we must take care to
 split as many foralls as it takes to retrieve the tau types we which to check.
 See Note [Splitting nested sigma types in class type signatures].
 
+Extra note: July 22.  If we have
+   class C a b where
+      op :: op_ty
+      default op :: def_ty
+      op = blah
+
+then we'll generate something like
+   $gdm_op :: C a b => def_ty
+   $gdm_op = blah
+
+We expect to write an instance that looks (in effect) like this:
+   instance G => C t1 t2 where
+      op = $gdm_op  -- Added when you leave out binding for 'op'
+
+So we need that
+  assuming constraints G, and C t1 t2,
+  we have (def_ty[t1/a,t2/b] <= op_ty[t1/a,t2/b]
+
+In the validity check, we want to check that there is such a G.
+E.g. if we check  def_ty <= op_ty, and get an insoluble constraint
+(Int~Bool), we know there will never be such a G, and can complain.
+
+This seems to be a more general way of thinking about the problem.
+But no one is complaining, so it'll have to wait for another day
+
 Note [Splitting nested sigma types in class type signatures]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Consider this type synonym and class definition:
diff --git a/compiler/GHC/Tc/TyCl/Instance.hs b/compiler/GHC/Tc/TyCl/Instance.hs
index 3067861431..cc7dc750d5 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/TcType.hs b/compiler/GHC/Tc/Utils/TcType.hs
index e9c643fe71..82924e9115 100644
--- a/compiler/GHC/Tc/Utils/TcType.hs
+++ b/compiler/GHC/Tc/Utils/TcType.hs
@@ -1443,35 +1443,51 @@ tcSplitSigmaTy ty = case tcSplitForAllInvisTyVars ty of
                         (tvs, rho) -> case tcSplitPhiTy rho of
                                         (theta, tau) -> (tvs, theta, tau)
 
--- | Split a sigma type into its parts, going underneath as many @ForAllTy@s
--- as possible. For example, given this type synonym:
---
--- @
--- type Traversal s t a b = forall f. Applicative f => (a -> f b) -> s -> f t
--- @
---
--- if you called @tcSplitSigmaTy@ on this type:
---
--- @
--- forall s t a b. Each s t a b => Traversal s t a b
--- @
---
--- then it would return @([s,t,a,b], [Each s t a b], Traversal s t a b)@. But
--- if you instead called @tcSplitNestedSigmaTys@ on the type, it would return
--- @([s,t,a,b,f], [Each s t a b, Applicative f], (a -> f b) -> s -> f t)@.
+-- | Split a sigma type into its parts, going underneath as many arrows
+-- and foralls as possible. See Note [tcSplitNestedSigmaTys]
 tcSplitNestedSigmaTys :: Type -> ([TyVar], ThetaType, Type)
--- NB: This is basically a pure version of topInstantiate (from Inst) that
--- doesn't compute an HsWrapper.
+-- See Note [tcSplitNestedSigmaTys]
+-- NB: This is basically a pure version of deeplyInstantiate (from Unify) that
+--     doesn't compute an HsWrapper.
 tcSplitNestedSigmaTys ty
     -- If there's a forall, split it apart and try splitting the rho type
     -- underneath it.
-  | (tvs1, theta1, rho1) <- tcSplitSigmaTy ty
+  | (arg_tys, body_ty)   <- tcSplitFunTys ty
+  , (tvs1, theta1, rho1) <- tcSplitSigmaTy body_ty
   , not (null tvs1 && null theta1)
   = let (tvs2, theta2, rho2) = tcSplitNestedSigmaTys rho1
-    in (tvs1 ++ tvs2, theta1 ++ theta2, rho2)
+    in (tvs1 ++ tvs2, theta1 ++ theta2, mkVisFunTys arg_tys rho2)
+
     -- If there's no forall, we're done.
   | otherwise = ([], [], ty)
 
+{- Note [tcSplitNestedSigmaTys]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+tcSplitNestedSigmaTys splits out all the /nested/ foralls and constraints,
+including under function arrows.  E.g. given this type synonym:
+  type Traversal s t a b = forall f. Applicative f => (a -> f b) -> s -> f t
+
+then
+  tcSplitNestedSigmaTys (forall s t a b. C s t a b => Int -> Traversal s t a b)
+
+will return
+  ( [s,t,a,b,f]
+  , [C s t a b, Applicative f]
+  , Int -> (a -> f b) -> s -> f t)@.
+
+This function is used in these places:
+* Improving error messages in GHC.Tc.Gen.Head.addFunResCtxt
+* Validity checking for default methods: GHC.Tc.TyCl.checkValidClass
+* A couple of calls in the GHCi debugger: GHC.Runtime.Heap.Inspect
+
+In other words, just in validity checking and error messages; hence
+no wrappers or evidence generation.
+
+Notice that tcSplitNestedSigmaTys even looks under function arrows;
+doing so is the Right Thing even with simple subsumption, not just
+with deep subsumption.
+-}
+
 -----------------------
 tcTyConAppTyCon :: Type -> TyCon
 tcTyConAppTyCon ty
diff --git a/compiler/GHC/Tc/Utils/Unify.hs b/compiler/GHC/Tc/Utils/Unify.hs
index 8ffbfb959b..9f85e04244 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,10 +55,12 @@ 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.Types.Name( Name, isSystemName )
 
 import GHC.Core.TyCon
 import GHC.Builtin.Types
@@ -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 5cbf84d330..0fd00b2c40 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 6b75ee2997..a841a73218 100644
--- a/testsuite/tests/driver/T4437.hs
+++ b/testsuite/tests/driver/T4437.hs
@@ -41,6 +41,7 @@ expectedGhcOnlyExtensions =
     , "AlternativeLayoutRule"
     , "AlternativeLayoutRuleTransitional"
     , "OverloadedRecordUpdate"
+    , "DeepSubsumption"
     ]
 
 expectedCabalOnlyExtensions :: [String]
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/showIface/LanguageExts.stdout b/testsuite/tests/showIface/LanguageExts.stdout
index c155327230..1e0a2a89be 100644
--- a/testsuite/tests/showIface/LanguageExts.stdout
+++ b/testsuite/tests/showIface/LanguageExts.stdout
@@ -12,6 +12,7 @@ docs:
          Just Haskell98
        language extensions:
          MonomorphismRestriction
+         DeepSubsumption
          ImplicitPrelude
          NPlusKPatterns
          PatternGuards
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/DeepSubsumption05.hs b/testsuite/tests/typecheck/should_compile/DeepSubsumption05.hs
new file mode 100644
index 0000000000..a6d9db3cb9
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/DeepSubsumption05.hs
@@ -0,0 +1,13 @@
+{-# LANGUAGE DefaultSignatures #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE DeepSubsumption #-}
+module DeepSubsumption06 where
+
+type Traversal' s a = forall f . Applicative f => (a -> a) -> f s -> f s
+type LensLike f m a = (a -> a) -> f m -> f m
+
+class Ixed m where
+  ix :: () -> Traversal' m ()
+
+  default ix :: (Applicative f) => () -> LensLike f m ()
+  ix = undefined
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 62edaf99e6..3410ad68bb 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -843,3 +843,9 @@ test('T18802', normal, compile, [''])
 test('T18802b', normal, compile, [''])
 test('T21289', normal, compile, [''])
 test('HardRecordUpdate', normal, compile, [''])
+test('T21548a', normal, compile, [''])
+test('DeepSubsumption01', normal, compile, [''])
+test('DeepSubsumption02', normal, compile, [''])
+test('DeepSubsumption03', normal, compile, [''])
+test('DeepSubsumption04', normal, compile, [''])
+test('DeepSubsumption05', 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