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)
(cherry picked from commit 71f740097af92b0ba441154736a21484fce5d0bb)
(cherry picked from commit dc27e15a76486b1ebd27a77f8515044c2671e22d)

30 files changed, 788 insertions, 191 deletions

diff --git a/compiler/GHC/Core/FVs.hs b/compiler/GHC/Core/FVs.hs
index 1fbf119172..17097bc0ef 100644
--- a/compiler/GHC/Core/FVs.hs
+++ b/compiler/GHC/Core/FVs.hs
@@ -625,7 +625,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/Data/IOEnv.hs b/compiler/GHC/Data/IOEnv.hs
index 5a3c56db3f..6a8d9635ae 100644
--- a/compiler/GHC/Data/IOEnv.hs
+++ b/compiler/GHC/Data/IOEnv.hs
@@ -60,7 +60,7 @@ import Control.Concurrent (forkIO, killThread)
 
 
 newtype IOEnv env a = IOEnv' (env -> IO a)
-  deriving (MonadThrow, MonadCatch, MonadMask) via (ReaderT env IO)
+  deriving (MonadThrow, MonadCatch, MonadMask, MonadFix) via (ReaderT env IO)
 
 -- See Note [The one-shot state monad trick] in GHC.Utils.Monad
 instance Functor (IOEnv env) where
diff --git a/compiler/GHC/Driver/Session.hs b/compiler/GHC/Driver/Session.hs
index 2abff1ad1f..b3d53c4953 100644
--- a/compiler/GHC/Driver/Session.hs
+++ b/compiler/GHC/Driver/Session.hs
@@ -1393,7 +1393,8 @@ languageExtensions (Just Haskell2010)
        LangExt.PatternGuards,
        LangExt.DoAndIfThenElse,
        LangExt.FieldSelectors,
-       LangExt.RelaxedPolyRec]
+       LangExt.RelaxedPolyRec,
+       LangExt.DeepSubsumption ]
 
 languageExtensions (Just GHC2021)
     = [LangExt.ImplicitPrelude,
@@ -3611,6 +3612,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/Errors/Hole.hs b/compiler/GHC/Tc/Errors/Hole.hs
index 6b6de5c576..0940a4cae3 100644
--- a/compiler/GHC/Tc/Errors/Hole.hs
+++ b/compiler/GHC/Tc/Errors/Hole.hs
@@ -958,7 +958,7 @@ tcCheckHoleFit (TypedHole {..}) hole_ty ty = discardErrs $
                           -- imp is the innermost implication
                           (imp:_) -> return (ic_tclvl imp)
      ; (wrap, wanted) <- setTcLevel innermost_lvl $ captureConstraints $
-                         tcSubTypeSigma ExprSigCtxt ty hole_ty
+                         tcSubTypeSigma orig ExprSigCtxt ty hole_ty
      ; traceTc "Checking hole fit {" empty
      ; traceTc "wanteds are: " $ ppr wanted
      ; if isEmptyWC wanted && isEmptyBag th_relevant_cts
@@ -985,6 +985,7 @@ tcCheckHoleFit (TypedHole {..}) hole_ty ty = discardErrs $
                ; traceTc "}" empty
                ; return (isSolvedWC rem, wrap) } }
      where
+       orig = ExprHoleOrigin (hole_occ <$> th_hole)
        setWCAndBinds :: EvBindsVar         -- Fresh ev binds var.
                      -> Implication        -- The implication to put WC in.
                      -> WantedConstraints  -- The WC constraints to put implic.
diff --git a/compiler/GHC/Tc/Gen/App.hs b/compiler/GHC/Tc/Gen/App.hs
index a63a058660..4182f1c0de 100644
--- a/compiler/GHC/Tc/Gen/App.hs
+++ b/compiler/GHC/Tc/Gen/App.hs
@@ -349,8 +349,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 $ ppr rn_expr)
+                                 app_res_rho exp_res_ty
+                     -- Need tcSubType because of the possiblity of deep subsumption.
+                     -- app_res_rho and exp_res_ty are both rho-types, so without
+                     -- deep subsumption unifyExpectedType would be sufficient
 
        ; whenDOptM Opt_D_dump_tc_trace $
          do { inst_args <- mapM zonkArg inst_args  -- Only when tracing
@@ -372,7 +376,7 @@ tcApp rn_expr exp_res_ty
                     else return (rebuildHsApps tc_fun fun_ctxt tc_args)
 
        -- 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 20c87f930d..0046e9384f 100644
--- a/compiler/GHC/Tc/Gen/Bind.hs
+++ b/compiler/GHC/Tc/Gen/Bind.hs
@@ -624,7 +624,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
@@ -802,7 +802,7 @@ mkExport prag_fn insoluble qtvs theta
                                            -- an ambiguous type and have AllowAmbiguousType
                                            -- e..g infer  x :: forall a. F a -> Int
                   else addErrCtxtM (mk_impedance_match_msg mono_info sel_poly_ty poly_ty) $
-                       tcSubTypeSigma sig_ctxt sel_poly_ty poly_ty
+                       tcSubTypeSigma GhcBug20076 sig_ctxt sel_poly_ty poly_ty
 
         ; warn_missing_sigs <- woptM Opt_WarnMissingLocalSignatures
         ; when warn_missing_sigs $
diff --git a/compiler/GHC/Tc/Gen/Expr.hs b/compiler/GHC/Tc/Gen/Expr.hs
index 597b9ca9cf..85dc666840 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' }
 
@@ -1010,8 +1010,8 @@ tcSynArgE :: CtOrigin
            -- ^ returns a wrapper :: (type of right shape) "->" (type passed in)
 tcSynArgE orig sigma_ty syn_ty thing_inside
   = do { (skol_wrap, (result, ty_wrapper))
-           <- tcSkolemise GenSigCtxt sigma_ty $ \ rho_ty ->
-              go rho_ty syn_ty
+           <- tcTopSkolemise GenSigCtxt sigma_ty
+                (\ rho_ty -> go rho_ty syn_ty)
        ; return (result, skol_wrap <.> ty_wrapper) }
     where
     go rho_ty SynAny
diff --git a/compiler/GHC/Tc/Gen/Head.hs b/compiler/GHC/Tc/Gen/Head.hs
index 2310de3ee5..7e569a8b24 100644
--- a/compiler/GHC/Tc/Gen/Head.hs
+++ b/compiler/GHC/Tc/Gen/Head.hs
@@ -763,7 +763,7 @@ tcExprSig expr sig@(PartialSig { psig_name = name, sig_loc = loc })
                  then return idHsWrapper  -- Fast path; also avoids complaint when we infer
                                           -- an ambiguous type and have AllowAmbiguousType
                                           -- e..g infer  x :: forall a. F a -> Int
-                 else tcSubTypeSigma ExprSigCtxt inferred_sigma my_sigma
+                 else tcSubTypeSigma ExprSigOrigin ExprSigCtxt inferred_sigma my_sigma
 
        ; traceTc "tcExpSig" (ppr qtvs $$ ppr givens $$ ppr inferred_sigma $$ ppr my_sigma)
        ; let poly_wrap = wrap
diff --git a/compiler/GHC/Tc/Gen/Sig.hs b/compiler/GHC/Tc/Gen/Sig.hs
index e1c1381e21..1a06dac4bb 100644
--- a/compiler/GHC/Tc/Gen/Sig.hs
+++ b/compiler/GHC/Tc/Gen/Sig.hs
@@ -38,7 +38,7 @@ import GHC.Tc.Types.Origin
 import GHC.Tc.Utils.TcType
 import GHC.Tc.Utils.TcMType
 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, (<.>) )
@@ -791,7 +791,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/Module.hs b/compiler/GHC/Tc/Module.hs
index 60e23f7e7a..a4fb1ec524 100644
--- a/compiler/GHC/Tc/Module.hs
+++ b/compiler/GHC/Tc/Module.hs
@@ -1785,9 +1785,14 @@ checkMainType tcg_env
              ctxt      = FunSigCtxt main_name False
        ; main_id   <- tcLookupId main_name
        ; (io_ty,_) <- getIOType
+       ; let main_ty   = idType main_id
+             eq_orig   = TypeEqOrigin { uo_actual   = main_ty
+                                      , uo_expected = io_ty
+                                      , uo_thing    = Nothing
+                                      , uo_visible  = True }
        ; (_, lie)  <- captureTopConstraints       $
                       setMainCtxt main_name io_ty $
-                      tcSubTypeSigma ctxt (idType main_id) io_ty
+                      tcSubTypeSigma eq_orig ctxt main_ty io_ty
        ; return lie } } } }
 
 checkMain :: Bool  -- False => no 'module M(..) where' header at all
diff --git a/compiler/GHC/Tc/TyCl/Instance.hs b/compiler/GHC/Tc/TyCl/Instance.hs
index 6fdce38825..b7ac2c2078 100644
--- a/compiler/GHC/Tc/TyCl/Instance.hs
+++ b/compiler/GHC/Tc/TyCl/Instance.hs
@@ -966,7 +966,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]
@@ -1901,8 +1901,9 @@ tcMethodBodyHelp hs_sig_fn sel_id local_meth_id meth_bind
                                 --           checking instance-sig <= class-meth-sig
                                 -- The instance-sig is the focus here; the class-meth-sig
                                 -- is fixed (#18036)
+                   ; let orig = InstanceSigOrigin sel_name sig_ty local_meth_ty
                    ; hs_wrap <- addErrCtxtM (methSigCtxt sel_name sig_ty local_meth_ty) $
-                                tcSubTypeSigma ctxt sig_ty local_meth_ty
+                                tcSubTypeSigma orig ctxt sig_ty local_meth_ty
                    ; return (sig_ty, hs_wrap) }
 
        ; inner_meth_name <- newName (nameOccName sel_name)
diff --git a/compiler/GHC/Tc/TyCl/PatSyn.hs b/compiler/GHC/Tc/TyCl/PatSyn.hs
index 111853d4d6..eedb8e9c9a 100644
--- a/compiler/GHC/Tc/TyCl/PatSyn.hs
+++ b/compiler/GHC/Tc/TyCl/PatSyn.hs
@@ -500,7 +500,8 @@ tcCheckPatSynDecl psb@PSB{ psb_id = lname@(L _ name), psb_args = details
            -- Else the error message location is wherever tcCheckPat finished,
            -- namely the right-hand corner of the pattern
         do { arg_id <- tcLookupId arg_name
-           ; wrap <- tcSubTypeSigma GenSigCtxt
+           ; wrap <- tcSubTypeSigma (OccurrenceOf (idName arg_id))
+                                    GenSigCtxt
                                     (idType arg_id)
                                     (substTy subst arg_ty)
                 -- Why do we need tcSubType here?
diff --git a/compiler/GHC/Tc/Types/Origin.hs b/compiler/GHC/Tc/Types/Origin.hs
index 5f233520b4..8b3b14324e 100644
--- a/compiler/GHC/Tc/Types/Origin.hs
+++ b/compiler/GHC/Tc/Types/Origin.hs
@@ -461,7 +461,7 @@ data CtOrigin
         -- We only need a CtOrigin on the first, because the location
         -- is pinned on the entire error message
 
-  | ExprHoleOrigin OccName   -- from an expression hole
+  | ExprHoleOrigin (Maybe OccName)   -- from an expression hole
   | TypeHoleOrigin OccName   -- from a type hole (partial type signature)
   | PatCheckOrigin      -- normalisation of a type during pattern-match checking
   | ListOrigin          -- An overloaded list
@@ -481,6 +481,13 @@ data CtOrigin
       CtOrigin   -- origin of the original constraint
       -- See Detail (7) of Note [Type equality cycles] in GHC.Tc.Solver.Canonical
 
+  | InstanceSigOrigin   -- from the sub-type check of an InstanceSig
+      Name   -- the method name
+      Type   -- the instance-sig type
+      Type   -- the instantiated type of the method
+  | AmbiguityCheckOrigin UserTypeCtxt
+  | GhcBug20076
+
 -- | The number of superclass selections needed to get this Given.
 -- If @d :: C ty@   has @ScDepth=2@, then the evidence @d@ will look
 -- like @sc_sel (sc_sel dg)@, where @dg@ is a Given.
@@ -660,6 +667,18 @@ pprCtOrigin (InstProvidedOrigin mod cls_inst)
 pprCtOrigin (CycleBreakerOrigin orig)
   = pprCtOrigin orig
 
+pprCtOrigin (InstanceSigOrigin method_name sig_type orig_method_type)
+  = vcat [ ctoHerald <+> text "the check that an instance signature is more general"
+         , text "than the type of the method (instantiated for this instance)"
+         , hang (text "instance signature:")
+              2 (ppr method_name <+> dcolon <+> ppr sig_type)
+         , hang (text "instantiated method type:")
+              2 (ppr orig_method_type) ]
+
+pprCtOrigin (AmbiguityCheckOrigin ctxt)
+  = ctoHerald <+> text "a type ambiguity check for" $$
+    pprUserTypeCtxt ctxt
+
 pprCtOrigin simple_origin
   = ctoHerald <+> pprCtO simple_origin
 
@@ -693,7 +712,8 @@ pprCtO DoOrigin              = text "a do statement"
 pprCtO MCompOrigin           = text "a statement in a monad comprehension"
 pprCtO ProcOrigin            = text "a proc expression"
 pprCtO AnnOrigin             = text "an annotation"
-pprCtO (ExprHoleOrigin occ)  = text "a use of" <+> quotes (ppr occ)
+pprCtO (ExprHoleOrigin Nothing)  = text "an expression hole"
+pprCtO (ExprHoleOrigin (Just occ))  = text "a use of" <+> quotes (ppr occ)
 pprCtO (TypeHoleOrigin occ)  = text "a use of wildcard" <+> quotes (ppr occ)
 pprCtO PatCheckOrigin        = text "a pattern-match completeness check"
 pprCtO ListOrigin            = text "an overloaded list"
@@ -701,4 +721,7 @@ pprCtO StaticOrigin          = text "a static form"
 pprCtO NonLinearPatternOrigin = text "a non-linear pattern"
 pprCtO (UsageEnvironmentOf x) = hsep [text "multiplicity of", quotes (ppr x)]
 pprCtO BracketOrigin         = text "a quotation bracket"
+pprCtO (InstanceSigOrigin {})  = text "a type signature in an instance"
+pprCtO (AmbiguityCheckOrigin {}) = text "a type ambiguity check"
+pprCtO GhcBug20076           = text "GHC Bug #20076"
 pprCtO _                     = panic "pprCtOrigin"
diff --git a/compiler/GHC/Tc/Utils/TcMType.hs b/compiler/GHC/Tc/Utils/TcMType.hs
index 2285818fab..d696ca4909 100644
--- a/compiler/GHC/Tc/Utils/TcMType.hs
+++ b/compiler/GHC/Tc/Utils/TcMType.hs
@@ -283,7 +283,7 @@ emitNewExprHole occ ty
        ; ref <- newTcRef (pprPanic "unfilled unbound-variable evidence" (ppr u))
        ; let her = HER ref ty u
 
-       ; loc <- getCtLocM (ExprHoleOrigin occ) (Just TypeLevel)
+       ; loc <- getCtLocM (ExprHoleOrigin (Just occ)) (Just TypeLevel)
 
        ; let hole = Hole { hole_sort = ExprHole her
                          , hole_occ  = occ
diff --git a/compiler/GHC/Tc/Utils/Unify.hs b/compiler/GHC/Tc/Utils/Unify.hs
index 2264c21413..f1426389e3 100644
--- a/compiler/GHC/Tc/Utils/Unify.hs
+++ b/compiler/GHC/Tc/Utils/Unify.hs
@@ -2,6 +2,7 @@
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TupleSections       #-}
 {-# LANGUAGE BlockArguments      #-}
+{-# LANGUAGE RecursiveDo         #-}
 
 {-# OPTIONS_GHC -Wno-incomplete-uni-patterns   #-}
 {-# OPTIONS_GHC -Wno-incomplete-record-updates #-}
@@ -15,9 +16,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,
 
@@ -54,13 +55,16 @@ import GHC.Tc.Utils.Env
 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.Tc.Utils.Instantiate
 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
@@ -68,13 +72,13 @@ 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
 
 import GHC.Exts      ( inline )
 import Control.Monad
-import Control.Arrow ( second )
 import qualified Data.Semigroup as S ( (<>) )
 
 {- *********************************************************************
@@ -306,7 +310,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) }
 
@@ -513,9 +517,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
@@ -580,11 +611,11 @@ 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 SDoc     -- The expression that has type 'actual' (if known)
-            -> TcSigmaType            -- Actual type
-            -> ExpRhoType             -- Expected type
+tcSubTypeNC :: CtOrigin          -- ^ Used when instantiating
+            -> UserTypeCtxt      -- ^ Used when skolemising
+            -> Maybe SDoc        -- ^ The expression that has type 'actual' (if known)
+            -> TcSigmaType       -- ^ Actual type
+            -> ExpRhoType        -- ^ Expected type
             -> TcM HsWrapper
 tcSubTypeNC inst_orig ctxt m_thing ty_actual res_ty
   = case res_ty of
@@ -597,6 +628,51 @@ 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
+  = do { dflags <- getDynFlags
+       ; tc_sub_type dflags (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
+  = do { dflags <- getDynFlags
+       ; tc_sub_type_shallow dflags (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
@@ -620,7 +696,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
@@ -635,33 +711,34 @@ command. See Note [Implementing :type] in GHC.Tc.Module.
 -}
 
 ---------------
-tcSubTypeSigma :: UserTypeCtxt -> TcSigmaType -> TcSigmaType -> TcM HsWrapper
--- External entry point, but no ExpTypes on either side
--- Checks that actual <= expected
--- Returns HsWrapper :: actual ~ expected
-tcSubTypeSigma ctxt ty_actual ty_expected
-  = do { dflags <- getDynFlags
-       ; tc_sub_type dflags (unifyType Nothing) eq_orig ctxt ty_actual ty_expected }
-  where
-    eq_orig = TypeEqOrigin { uo_actual   = ty_actual
-                           , uo_expected = ty_expected
-                           , uo_thing    = Nothing
-                           , uo_visible  = True }
-
----------------
-tc_sub_type :: DynFlags
-            -> (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
+    :: DynFlags
+    -> (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 dflags 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    dflags unify inst_orig ctxt ty_actual ty_expected
+         else tc_sub_type_shallow dflags unify inst_orig ctxt ty_actual ty_expected
+  }
+
+----------------------
+tc_sub_type_shallow dflags unify inst_orig ctxt ty_actual ty_expected
+  | definitely_poly dflags 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 ]
@@ -674,52 +751,67 @@ tc_sub_type dflags 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 dflags tv tau `cterHasProblem` cteInsolubleOccurs
-      = True
-      | otherwise
-      = False
+----------------------
+tc_sub_type_deep dflags unify inst_orig ctxt ty_actual ty_expected
+  | definitely_poly dflags 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 :: DynFlags -> TcType -> Bool
+-- A very conservative test:
+-- see Note [Don't skolemise unnecessarily]
+definitely_poly dflags ty
+  | (tvs, theta, tau) <- tcSplitSigmaTy ty
+  , (tv:_) <- tvs   -- At least one tyvar
+  , null theta      -- No constraints; see (DP1)
+  , checkTyVarEq dflags 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
@@ -727,54 +819,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]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -824,13 +887,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 { dflags <- getDynFlags
+           ; arg_wrap  <- tc_sub_type_deep dflags 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]
+           ; let doc = text "When checking that" <+> quotes (ppr ty_actual)
+                   <+> text "is more polymorphic than" <+> quotes (ppr ty_expected)
+           ; return (mult_wrap <.>
+                     mkWpFun arg_wrap res_wrap (Scaled exp_mult exp_arg) exp_res doc)}
+                     -- 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  { (wrap, tv_prs, given, rho_ty) <- deeplySkolemise expected_ty
+        ; let skol_info = 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 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 :: TcSigmaType
+                -> TcM ( HsWrapper
+                       , [(Name,TyVar)]     -- All skolemised variables
+                       , [EvVar]            -- All "given"s
+                       , TcRhoType )
+-- See Note [Deep skolemisation]
+deeplySkolemise 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 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).
 
@@ -846,29 +1200,35 @@ 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 { (wrap, tv_prs, given, rho_ty) <- topSkolemise expected_ty
-       ; let skol_tvs  = map snd tv_prs
-             skol_info = SigSkol ctxt expected_ty tv_prs
+  = do { deep_subsumption <- xoptM LangExt.DeepSubsumption
+       ; let skolemise | deep_subsumption = deeplySkolemise
+                       | otherwise        = topSkolemise
+       ; (wrap, tv_prs, given, rho_ty) <- skolemise expected_ty
 
+       ; let skol_tvs = map snd tv_prs
+             skol_info = SigSkol ctxt expected_ty tv_prs
        ; (ev_binds, res)
              <- checkConstraints skol_info skol_tvs given $
                 tcExtendNameTyVarEnv tv_prs               $
@@ -876,33 +1236,36 @@ 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  { (wrap, tv_prs, given, rho_ty) <- topSkolemise expected_ty
+  = do { rec { let skol_info = SigSkol ctxt expected_ty tv_prs
+             ; (wrap, tv_prs, given, rho_ty) <- topSkolemise expected_ty
+             }
 
-        ; let skol_tvs  = map snd tv_prs
-              skol_info = SigSkol ctxt expected_ty tv_prs
-
-        ; (ev_binds, result)
-              <- checkConstraints skol_info skol_tvs given $
-                 thing_inside rho_ty
+       ; let skol_tvs = map snd tv_prs
+       ; (ev_binds, result)
+             <- checkConstraints 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 :: SkolemInfo
                  -> [TcTyVar]           -- Skolems
@@ -921,7 +1284,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 9a43e69c67..5ad18a52eb 100644
--- a/compiler/GHC/Tc/Validity.hs
+++ b/compiler/GHC/Tc/Validity.hs
@@ -27,7 +27,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
@@ -139,7 +139,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 ...
@@ -150,6 +152,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
@@ -218,7 +231,9 @@ checkAmbiguity ctxt ty
        ; allow_ambiguous <- xoptM LangExt.AllowAmbiguousTypes
        ; (_wrap, wanted) <- addErrCtxt (mk_msg allow_ambiguous) $
                             captureConstraints $
-                            tcSubTypeSigma 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 92c6c8ffd6..5604ce7cd1 100644
--- a/docs/users_guide/exts/rank_polymorphism.rst
+++ b/docs/users_guide/exts/rank_polymorphism.rst
@@ -157,7 +157,7 @@ In the function ``h`` we use the record selectors ``return`` and
 ``MonadT`` data structure, rather than using pattern matching.
 
 
-.. _simple-subsumption:
+.. _subsumption:
 
 Subsumption
 -------------
@@ -199,13 +199,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-aank 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 8dc2b67a36..153ed8fe62 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/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/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 a2a3606c09..fd18df7707 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -794,3 +794,8 @@ test('T21558', normal, compile, ['-w'])
 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