GitLab

Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC

Commits:

56b32c5a

by sheaf at 2025-08-12T10:00:19-04:00

Improve deep subsumption

This commit improves the DeepSubsumption sub-typing implementation
in GHC.Tc.Utils.Unify.tc_sub_type_deep by being less eager to fall back
to unification.

For example, we now are properly able to prove the subtyping relationship

  ((∀ a. a->a) -> Int) -> Bool  <=  β[tau] Bool

for an unfilled metavariable β. In this case (with an AppTy on the right),
we used to fall back to unification. No longer: now, given that the LHS
is a FunTy and that the RHS is a deep rho type (does not need any instantiation),
we try to make the RHS into a FunTy, viz.

  β := (->) γ

We can then continue using covariance & contravariance of the function
arrow, which allows us to prove the subtyping relationship, instead of
trying to unify which would cause us to error out with:

  Couldn't match expected type ‘β’ with actual type ‘(->) ((∀ a. a -> a) -> Int)

See Note [FunTy vs non-FunTy case in tc_sub_type_deep] in GHC.Tc.Utils.Unify.

The other main improvement in this patch concerns type inference.
The main subsumption logic happens (before & after this patch) in
GHC.Tc.Gen.App.checkResultTy. However, before this patch, all of the
DeepSubsumption logic only kicked in in 'check' mode, not in 'infer' mode.

This patch adds deep instantiation in the 'infer' mode of checkResultTy
when we are doing deep subsumption, which allows us to accept programs
such as:

  f :: Int -> (forall a. a->a)
  g :: Int -> Bool -> Bool

  test1 b =
    case b of
      True  -> f
      False -> g
  test2 b =
    case b of
      True  -> g
      False -> f

See Note [Deeply instantiate in checkResultTy when inferring].

Finally, we add representation-polymorphism checks to ensure that the
lambda abstractions we introduce when doing subsumption obey the
representation polymorphism invariants of Note [Representation polymorphism invariants]
in GHC.Core. See Note [FunTy vs FunTy case in tc_sub_type_deep].
This is accompanied by a courtesy change to `(<.>) :: HsWrapper -> HsWrapper -> HsWrapper`,
adding the equation:

  WpCast c1 <.> WpCast c2 = WpCast (c1 `mkTransCo` c2)

This is useful because mkWpFun does not introduce an eta-expansion when
both of the argument & result wrappers are casts; so this change allows
us to avoid introducing lambda abstractions when casts suffice.

Fixes #26225

26 changed files:

compiler/GHC/Builtin/PrimOps/Ids.hs
compiler/GHC/HsToCore.hs
compiler/GHC/Tc/Gen/App.hs
compiler/GHC/Tc/Gen/Expr.hs
compiler/GHC/Tc/Gen/HsType.hs
compiler/GHC/Tc/Types/Evidence.hs
compiler/GHC/Tc/Types/Origin.hs
compiler/GHC/Tc/Utils/Concrete.hs
compiler/GHC/Tc/Utils/Unify.hs
compiler/GHC/Types/Id/Make.hs
testsuite/tests/corelint/LintEtaExpand.stderr
testsuite/tests/indexed-types/should_fail/T5439.stderr
testsuite/tests/partial-sigs/should_compile/T10403.stderr
testsuite/tests/partial-sigs/should_fail/T10615.stderr
+ testsuite/tests/rep-poly/NoEtaRequired.hs
testsuite/tests/rep-poly/T21906.stderr
testsuite/tests/rep-poly/all.T
+ testsuite/tests/typecheck/should_compile/T26225.hs
+ testsuite/tests/typecheck/should_compile/T26225b.hs
testsuite/tests/typecheck/should_compile/all.T
− testsuite/tests/typecheck/should_fail/T12563.stderr
testsuite/tests/typecheck/should_fail/T14618.stderr
testsuite/tests/typecheck/should_fail/T6022.stderr
testsuite/tests/typecheck/should_fail/T8883.stderr
testsuite/tests/typecheck/should_fail/all.T
testsuite/tests/typecheck/should_fail/tcfail140.stderr

Changes:

compiler/GHC/Builtin/PrimOps/Ids.hs

@@ -99,7 +99,7 @@ computePrimOpConcTyVarsFromType nm tyvars arg_tys _res_ty = mkNameEnv concs
        | tv `elem` [ runtimeRep1TyVar, runtimeRep2TyVar, runtimeRep3TyVar
                    , levity1TyVar, levity2TyVar ]
        = listToMaybe $
 -          mapMaybe (\ (i,arg) -> Argument i <$> positiveKindPos_maybe tv arg)
 +          mapMaybe (\ (i,arg) -> mkArgPos i <$> positiveKindPos_maybe tv arg)
              (zip [1..] arg_tys)
        | otherwise
        = Nothing
@@ -124,7 +124,7 @@ negativeKindPos_maybe tv ty
+       )
    where
      recur (pos, scaled_ty)
 -      = Argument pos <$> positiveKindPos_maybe tv (scaledThing scaled_ty)
 +      = mkArgPos pos <$> positiveKindPos_maybe tv (scaledThing scaled_ty)
      -- (assumes we don't have any function types nested inside other types)
  -- | Does this type variable appear in a kind in a positive position in the
@@ -145,7 +145,7 @@ positiveKindPos_maybe tv ty
+       )
    where
      recur (pos, scaled_ty)
 -      = Argument pos <$> negativeKindPos_maybe tv (scaledThing scaled_ty)
 +      = mkArgPos pos <$> negativeKindPos_maybe tv (scaledThing scaled_ty)
      -- (assumes we don't have any function types nested inside other types)
      finish ty
        | tv `elemVarSet` tyCoVarsOfType (typeKind ty)

compiler/GHC/HsToCore.hs

@@ -39,7 +39,7 @@ import GHC.HsToCore.Coverage
  import GHC.HsToCore.Docs
  import GHC.Tc.Types
 -import GHC.Tc.Types.Origin ( Position(..) )
 +import GHC.Tc.Types.Origin ( Position(..), mkArgPos )
  import GHC.Tc.Utils.Monad  ( finalSafeMode, fixSafeInstances )
  import GHC.Tc.Module ( runTcInteractive )
@@ -780,7 +780,7 @@ mkUnsafeCoercePrimPair _old_id old_expr
               arity = 1
               concs = mkRepPolyIdConcreteTyVars
 -                     [((mkTyVarTy openAlphaTyVar, Argument 1 Top), runtimeRep1TyVar)]
 +                     [((mkTyVarTy openAlphaTyVar, mkArgPos 1 Top), runtimeRep1TyVar)]
                       unsafeCoercePrimName
               id   = mkExportedLocalId (RepPolyId concs) unsafeCoercePrimName ty `setIdInfo` info

compiler/GHC/Tc/Gen/App.hs

@@ -430,7 +430,8 @@ tcApp rn_expr exp_res_ty
                           -- Step 5.2: typecheck the arguments, and monomorphise
                           --           any un-unified instantiation variables
                         ; tc_args <- tcValArgs DoQL inst_args
 -                         -- Step 5.3: typecheck the arguments
 +                         -- Step 5.3: zonk to expose the polymophism hidden under
 +                         --           QuickLook instantiation variables in `app_res_rho`
                         ; app_res_rho <- liftZonkM $ zonkTcType app_res_rho
                           -- Step 5.4: subsumption check against the expected type
                         ; res_wrap <- checkResultTy rn_expr tc_head inst_args
@@ -463,6 +464,8 @@ finishApp tc_head@(tc_fun,_) tc_args app_res_rho res_wrap
         ; traceTc "End tcApp }" (ppr tc_fun)
         ; return (mkHsWrap res_wrap res_expr) }
 +-- | Connect up the inferred type of an application with the expected type.
 +-- This is usually just a unification, but with deep subsumption there is more to do.
  checkResultTy :: HsExpr GhcRn
                -> (HsExpr GhcTc, AppCtxt)  -- Head
                -> [HsExprArg p]            -- Arguments, just error messages
@@ -470,11 +473,29 @@ checkResultTy :: HsExpr GhcRn
                              --   expose foralls, but maybe not deeply instantiated
                -> ExpRhoType -- Expected type; this is deeply skolemised
                -> TcM HsWrapper
 --- Connect up the inferred type of the application with the expected type
 --- This is usually just a unification, but with deep subsumption there is more to do
 -checkResultTy _ _ _ app_res_rho (Infer inf_res)
 -  = do { co <- fillInferResult app_res_rho inf_res
 -       ; return (mkWpCastN co) }
 +checkResultTy rn_expr _fun _inst_args app_res_rho (Infer inf_res)
 +  = fillInferResultDS (exprCtOrigin rn_expr) app_res_rho inf_res
 +  -- See Note [Deeply instantiate in checkResultTy when inferring]
++
 +{- Note [Deeply instantiate in checkResultTy when inferring]
 +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 +To accept the following program (T26225b) with -XDeepSubsumption, we need to
 +deeply instantiate when inferring in checkResultTy:
++
 +  f :: Int -> (forall a. a->a)
 +  g :: Int -> Bool -> Bool
++
 +  test b =
 +    case b of
 +      True  -> f
 +      False -> g
++
 +If we don't deeply instantiate in the branches of the case expression, we will
 +try to unify the type of 'f' with that of 'g', which fails. If we instead
 +deeply instantiate 'f', we will fill the 'InferResult' with 'Int -> alpha -> alpha'
 +which then successfully unifies with the type of 'g' when we come to fill the
 +'InferResult' hole a second time for the second case branch.
 +-}
  checkResultTy rn_expr (tc_fun, fun_ctxt) inst_args app_res_rho (Check res_ty)
  -- Unify with expected type from the context
@@ -502,8 +523,6 @@ checkResultTy rn_expr (tc_fun, fun_ctxt) inst_args app_res_rho (Check res_ty)
               -- Even though both app_res_rho and res_ty are rho-types,
               -- they may have nested polymorphism, so if deep subsumption
               -- is on we must call tcSubType.
 -             -- Zonk app_res_rho first, because QL may have instantiated some
 -             -- delta variables to polytypes, and tcSubType doesn't expect that
               do { wrap <- tcSubTypeDS rn_expr app_res_rho res_ty
                  ; traceTc "checkResultTy 2 }" (ppr app_res_rho $$ ppr res_ty)
                  ; return wrap } }

compiler/GHC/Tc/Gen/Expr.hs

@@ -1056,7 +1056,8 @@ tcSynArgA orig op sigma_ty arg_shapes res_shape thing_inside
      tc_syn_arg _ (SynFun {}) _
        = pprPanic "tcSynArgA hits a SynFun" (ppr orig)
      tc_syn_arg res_ty (SynType the_ty) thing_inside
 -      = do { wrap   <- tcSubType orig GenSigCtxt res_ty the_ty
 +      = do { wrap   <- addSubTypeCtxt res_ty the_ty $
 +                       tcSubType orig GenSigCtxt Nothing res_ty the_ty
             ; result <- thing_inside []
             ; return (result, wrap) }

compiler/GHC/Tc/Gen/HsType.hs

@@ -946,7 +946,7 @@ Terms are eagerly instantiated. This means that if you say
  then `id` gets instantiated to have type alpha -> alpha. The variable
  alpha is then unconstrained and regeneralized. So we may well end up with
 -  x = /\x. id @a
 +  x = /\a. id @a
  But we cannot do this in types, as we have no type-level lambda.
  So, we must be careful only to instantiate at the last possible moment, when
@@ -954,9 +954,15 @@ we're sure we're never going to want the lost polymorphism again. This is done
  in calls to `tcInstInvisibleTyBinders`; a particular case in point is in
  `checkExpectedKind`.
 +For example, suppose we have:
 +    Actual:  ∀ k2 k. k -> k2   -> k
 +  Expected:  ∀    k. k -> Type -> k
 +We must very delicately instantiate just k2 to kappa, and then unify
 +  (∀ k. k -> Type -> k) ~ (∀ k. k -> kappa -> k)
++
  Otherwise, we are careful /not/ to instantiate.  For example:
 -* at a variable  in `tcTyVar`
 -* in `tcInferLHsTypeUnsaturated`, which is used by :kind in GHCi.
 +  * at a variable  in `tcTyVar`
 +  * in `tcInferLHsTypeUnsaturated`, which is used by :kind in GHCi.
  ************************************************************************
  *                                                                      *
@@ -1977,6 +1983,8 @@ checkExpKind :: HsType GhcRn -> TcType -> TcKind -> ExpKind -> TcM TcType
  checkExpKind rn_ty ty ki (Check ki') =
    checkExpectedKind rn_ty ty ki ki'
  checkExpKind _rn_ty ty ki (Infer cell) = do
 +  -- NB: do not instantiate.
 +  -- See Note [Do not always instantiate eagerly in types]
    co <- fillInferResult ki cell
    pure (ty `mkCastTy` co)

compiler/GHC/Tc/Types/Evidence.hs

@@ -199,28 +199,44 @@ instance Monoid HsWrapper where
    mempty = WpHole
  (<.>) :: HsWrapper -> HsWrapper -> HsWrapper
 -WpHole <.> c = c
 -c <.> WpHole = c
 -c1 <.> c2    = c1 `WpCompose` c2
+-
 --- | Smart constructor to create a 'WpFun' 'HsWrapper'.
 +WpHole    <.> c         = c
 +c         <.> WpHole    = c
 +WpCast c1 <.> WpCast c2 = WpCast (c1 `mkTransCo` c2)
 +  -- If we can represent the HsWrapper as a cast, try to do so: this may avoid
 +  -- unnecessary eta-expansion (see 'mkWpFun').
 +c1        <.> c2        = c1 `WpCompose` c2
++
 +-- | Smart constructor to create a 'WpFun' 'HsWrapper', which avoids introducing
 +-- a lambda abstraction if the two supplied wrappers are either identities or
 +-- casts.
 +--
 +-- PRECONDITION: either:
  --
 --- PRECONDITION: the "from" type of the first wrapper must have a syntactically
 --- fixed RuntimeRep (see Note [Fixed RuntimeRep] in GHC.Tc.Utils.Concrete).
 +--  1. both of the 'HsWrapper's are identities or casts, or
 +--  2. both the "from" and "to" types of the first wrapper have a syntactically
 +--     fixed RuntimeRep (see Note [Fixed RuntimeRep] in GHC.Tc.Utils.Concrete).
  mkWpFun :: HsWrapper -> HsWrapper
          -> Scaled TcTypeFRR -- ^ the "from" type of the first wrapper
 -                            -- MUST have a fixed RuntimeRep
          -> TcType           -- ^ Either "from" type or "to" type of the second wrapper
                              --   (used only when the second wrapper is the identity)
          -> HsWrapper
 -  -- NB: we can't check that the argument type has a fixed RuntimeRep with an assertion,
 -  -- because of [Wrinkle: Typed Template Haskell] in Note [hasFixedRuntimeRep]
 -  -- in GHC.Tc.Utils.Concrete.
  mkWpFun WpHole       WpHole       _             _  = WpHole
  mkWpFun WpHole       (WpCast co2) (Scaled w t1) _  = WpCast (mk_wp_fun_co w (mkRepReflCo t1) co2)
  mkWpFun (WpCast co1) WpHole       (Scaled w _)  t2 = WpCast (mk_wp_fun_co w (mkSymCo co1)    (mkRepReflCo t2))
  mkWpFun (WpCast co1) (WpCast co2) (Scaled w _)  _  = WpCast (mk_wp_fun_co w (mkSymCo co1)    co2)
 -mkWpFun co1          co2          t1            _  = WpFun co1 co2 t1
 +mkWpFun w_arg        w_res        t1            _  =
 +  -- In this case, we will desugar to a lambda
 +  --
 +  --   \x. w_res[ e w_arg[x] ]
 +  --
 +  -- To satisfy Note [Representation polymorphism invariants] in GHC.Core,
 +  -- it must be the case that both the lambda bound variable x and the function
 +  -- argument w_arg[x] have a fixed runtime representation, i.e. that both the
 +  -- "from" and "to" types of the first wrapper "w_arg" have a fixed runtime representation.
 +  --
 +  -- Unfortunately, we can't check this with an assertion here, because of
 +  -- [Wrinkle: Typed Template Haskell] in Note [hasFixedRuntimeRep] in GHC.Tc.Utils.Concrete.
 +  WpFun w_arg w_res t1
  mkWpEta :: [Id] -> HsWrapper -> HsWrapper
  -- (mkWpEta [x1, x2] wrap) [e]

compiler/GHC/Tc/Types/Origin.hs

  {-# LANGUAGE DataKinds #-}
 +{-# LANGUAGE DerivingStrategies #-}
  {-# LANGUAGE FlexibleContexts #-}
  {-# LANGUAGE GADTs #-}
  {-# LANGUAGE PolyKinds #-}
  {-# LANGUAGE StandaloneKindSignatures #-}
 -{-# LANGUAGE TypeFamilies #-}
 +{-# LANGUAGE TypeFamilyDependencies #-}
  -- | Describes the provenance of types as they flow through the type-checker.
  -- The datatypes here are mainly used for error message generation.
@@ -39,7 +40,7 @@ module GHC.Tc.Types.Origin (
    mkFRRUnboxedTuple, mkFRRUnboxedSum,
    -- ** FixedRuntimeRep origin for rep-poly 'Id's
 -  RepPolyId(..), Polarity(..), Position(..),
 +  RepPolyId(..), Polarity(..), Position(..), mkArgPos,
    -- ** Arrow command FixedRuntimeRep origin
    FRRArrowContext(..), pprFRRArrowContext,
@@ -78,7 +79,7 @@ import GHC.Utils.Outputable
  import GHC.Utils.Panic
  import GHC.Stack
  import GHC.Utils.Monad
 -import GHC.Utils.Misc( HasDebugCallStack )
 +import GHC.Utils.Misc( HasDebugCallStack, nTimes )
  import GHC.Types.Unique
  import GHC.Types.Unique.Supply
@@ -1188,7 +1189,7 @@ data FixedRuntimeRepContext
    -- See 'FRRArrowContext' for more details.
    | FRRArrow !FRRArrowContext
 -  -- | A representation-polymorphic check arising from a call
 +  -- | A representation-polymorphism check arising from a call
    -- to 'matchExpectedFunTys' or 'matchActualFunTy'.
    --
    -- See 'ExpectedFunTyOrigin' for more details.
@@ -1197,6 +1198,13 @@ data FixedRuntimeRepContext
        !Int
          -- ^ argument position (1-indexed)
 +  -- | A representation-polymorphism check arising from eta-expansion
 +  -- performed as part of deep subsumption.
 +  | forall p. FRRDeepSubsumption
 +      { frrDSExpected :: Bool
 +      , frrDSPosition :: Position p
 +      }
++
  -- | The description of a representation-polymorphic 'Id'.
  data RepPolyId
    -- | A representation-polymorphic 'PrimOp'.
@@ -1234,8 +1242,8 @@ pprFixedRuntimeRepContext (FRRRecordUpdate lbl _arg)
  pprFixedRuntimeRepContext (FRRBinder binder)
    = sep [ text "The binder"
          , quotes (ppr binder) ]
 -pprFixedRuntimeRepContext (FRRRepPolyId nm id what)
 -  = pprFRRRepPolyId id nm what
 +pprFixedRuntimeRepContext (FRRRepPolyId nm id pos)
 +  = text "The" <+> ppr pos <+> text "of" <+> pprRepPolyId id nm
  pprFixedRuntimeRepContext FRRPatBind
    = text "The pattern binding"
  pprFixedRuntimeRepContext FRRPatSynArg
@@ -1277,6 +1285,13 @@ pprFixedRuntimeRepContext (FRRArrow arrowContext)
    = pprFRRArrowContext arrowContext
  pprFixedRuntimeRepContext (FRRExpectedFunTy funTyOrig arg_pos)
    = pprExpectedFunTyOrigin funTyOrig arg_pos
 +pprFixedRuntimeRepContext (FRRDeepSubsumption is_exp pos)
 +  = hsep [ text "The", what, text "type of the"
 +         , ppr (Argument pos)
 +         , text "of the eta-expansion"
 +         ]
 +  where
 +    what = if is_exp then text "expected" else text "actual"
  instance Outputable FixedRuntimeRepContext where
    ppr = pprFixedRuntimeRepContext
@@ -1305,34 +1320,117 @@ data ArgPos
  *                                                                      *
  ********************************************************************* -}
 +{- Note [Positional information in representation-polymorphism errors]
 +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 +Consider an invalid instantiation of the 'catch#' primop:
++
 +  catch#
 +    :: forall {q :: RuntimeRep} {k :: Levity} (a :: TYPE q)
 +              (b :: TYPE (BoxedRep k)).
 +       (State# RealWorld -> (# State# RealWorld, a #))
 +       -> (b -> State# RealWorld -> (# State# RealWorld, a #))
 +       -> State# RealWorld
 +       -> (# State# RealWorld, a #)
++
 +  boo :: forall r (a :: TYPE r). ...
 +  boo = catch# @a
++
 +The instantiation is invalid because we insist that the quantified RuntimeRep
 +type variable 'q' be instantiated to a concrete RuntimeRep, as per
 +Note [Representation-polymorphism checking built-ins] in GHC.Tc.Utils.Concrete.
++
 +We report this as the following error message:
++
 +  The result of the first argument of the primop ‘catch#’ does not have a fixed runtime representation.
 +  Its type is: (a :: TYPE r).
++
 +The positional information in this message, namely "The result of the first argument",
 +is produced by using the 'Position' datatype. In this case:
++
 +  pos :: Position Neg
 +  pos = Result (Argument Top)
 +  ppr pos = "result of the first argument"
++
 +Other examples:
++
 +  pos2 :: Position Neg
 +  pos2 = Argument (Result (Result Top))
 +  ppr pos2 = "3rd argument"
++
 +  pos3 :: Position Pos
 +  pos3 = Argument (Result (Argument (Result Top)))
 +  ppr pos3 = "2nd argument of the 2nd argument"
++
 +It's useful to keep track at the type-level whether we are in a positive or
 +negative position in the type, as for primops we can usually tolerate
 +representation-polymorphism in positive positions, but not in negative ones;
 +for example
++
 +  ($) :: forall {r} (a :: Type) (b :: TYPE r). (a -> b) -> a -> b
++
++
 +This positional information is (currently) used to report representation-polymorphism
 +errors in precisely the following two situations:
++
 +  1. Representation-polymorphic Ids with no binding, as described in
 +     Note [Representation-polymorphic Ids with no binding] in GHC.Tc.Utils.Concrete.
++
 +     This uses the 'FRRRepPolyId' constructor of 'FixedRuntimeRepContext'.
++
 +  2. When inserting eta-expansions for deep subsumption.
 +     See Wrinkle [Representation-polymorphism checking during subtyping] in
 +     Note [FunTy vs FunTy case in tc_sub_type_deep] in GHC.Tc.Utils.Unify.
++
 +     This uses the 'FRRDeepSubsumption' constructor of 'FixedRuntimeRepContext'.
 +-}
++
 +-- | Are we in a positive (covariant) or negative (contravariant) position?
 +--
 +-- See Note [Positional information in representation-polymorphism errors].
  data Polarity = Pos | Neg
 +-- | Flip the 'Polarity': turn positive into negative and vice-versa.
  type FlipPolarity :: Polarity -> Polarity
 -type family FlipPolarity p where
 +type family FlipPolarity p = r | r -> p where
    FlipPolarity Pos = Neg
    FlipPolarity Neg = Pos
  -- | A position in which a type variable appears in a type;
  -- in particular, whether it appears in a positive or a negative position.
 +--
 +-- See Note [Positional information in representation-polymorphism errors].
  type Position :: Polarity -> Hs.Type
  data Position p where
 -  -- | In the @i@-th argument of a function arrow
 -  Argument :: Int -> Position (FlipPolarity p) -> Position p
 +  -- | In the argument of a function arrow
 +  Argument :: Position p -> Position (FlipPolarity p)
    -- | In the result of a function arrow
    Result   :: Position p -> Position p
    -- | At the top level of a type
    Top      :: Position Pos
+-
 -pprFRRRepPolyId :: RepPolyId -> Name -> Position Neg -> SDoc
 -pprFRRRepPolyId id nm (Argument i pos) =
 -  text "The" <+> what <+> speakNth i <+> text "argument of" <+> pprRepPolyId id nm
 +deriving stock instance Show (Position p)
 +instance Outputable (Position p) where
 +  ppr = go 1
 +    where
 +      go :: Int -> Position q -> SDoc
 +      go i (Argument (Result pos)) = go (i+1) (Argument pos)
 +      go i (Argument pos) = speakNth i <+> text "argument" <+> aux 1 pos
 +      go i (Result (Result pos)) = go i (Result pos)
 +      go i (Result pos) = text "result" <+> aux i pos
 +      go _ Top = text "top-level"
++
 +      aux :: Int -> Position q -> SDoc
 +      aux i pos = case pos of { Top -> empty; _ -> text "of the" <+> go i pos }
++
 +-- | @'mkArgPos' i p@ makes the 'Position' @p@ relative to the @ith@ argument.
 +--
 +-- Example: @ppr (mkArgPos 3 (Result Top)) == "in the result of the 3rd argument"@.
 +mkArgPos :: Int -> Position p -> Position (FlipPolarity p)
 +mkArgPos i = go
    where
 -    what = case pos of
 -      Top       -> empty
 -      Result {} -> text "return type of the"
 -      _         -> text "nested return type inside the"
 -pprFRRRepPolyId id nm (Result {}) =
 -  text "The result of" <+> pprRepPolyId id nm
 +    go :: Position p -> Position (FlipPolarity p)
 +    go Top = Argument $ nTimes (i-1) Result Top
 +    go (Result p) = Result $ go p
 +    go (Argument p) = Argument $ go p
  pprRepPolyId :: RepPolyId -> Name -> SDoc
  pprRepPolyId id nm = id_desc <+> quotes (ppr nm)

compiler/GHC/Tc/Utils/Concrete.hs

@@ -803,7 +803,7 @@ idConcreteTvs id
    = mkNameEnv
      [(tyVarName a_rep, ConcreteFRR $ FixedRuntimeRepOrigin (mkTyVarTy a)
                                     $ FRRRepPolyId unsafeCoercePrimName RepPolyFunction
 -                                   $ Argument 1 Top)]
 +                                   $ mkArgPos 1 Top)]
    | otherwise
    = idDetailsConcreteTvs $ idDetails id

compiler/GHC/Tc/Utils/Unify.hs

 +{-# LANGUAGE DataKinds           #-}
  {-# LANGUAGE DeriveTraversable   #-}
  {-# LANGUAGE DerivingStrategies  #-}
  {-# LANGUAGE LambdaCase          #-}
@@ -18,6 +19,7 @@ module GHC.Tc.Utils.Unify (
    -- Full-blown subsumption
    tcWrapResult, tcWrapResultO, tcWrapResultMono,
    tcSubType, tcSubTypeSigma, tcSubTypePat, tcSubTypeDS,
 +  addSubTypeCtxt,
    tcSubTypeAmbiguity, tcSubMult,
    checkConstraints, checkTvConstraints,
    buildImplicationFor, buildTvImplication, emitResidualTvConstraint,
@@ -25,9 +27,10 @@ module GHC.Tc.Utils.Unify (
    -- Skolemisation
    DeepSubsumptionFlag(..), getDeepSubsumptionFlag, isRhoTyDS,
    tcSkolemise, tcSkolemiseCompleteSig, tcSkolemiseExpectedType,
 +  deeplyInstantiate,
    -- Various unifications
 -  unifyType, unifyKind, unifyInvisibleType, unifyExpectedType,
 +  unifyType, unifyKind, unifyInvisibleType,
    unifyExprType, unifyTypeAndEmit, promoteTcType,
    swapOverTyVars, touchabilityTest, checkTopShape, lhsPriority,
    UnifyEnv(..), updUEnvLoc, setUEnvRole,
@@ -57,7 +60,7 @@ module GHC.Tc.Utils.Unify (
    simpleUnifyCheck, UnifyCheckCaller(..), SimpleUnifyResult(..),
 -  fillInferResult,
 +  fillInferResult, fillInferResultDS
    ) where
  import GHC.Prelude
@@ -796,12 +799,14 @@ matchExpectedFunTys :: forall a.
  -- Postcondition:
  --   If exp_ty is Check {}, then [ExpPatType] and ExpRhoType results are all Check{}
  --   If exp_ty is Infer {}, then [ExpPatType] and ExpRhoType results are all Infer{}
 -matchExpectedFunTys herald _ arity (Infer inf_res) thing_inside
 +matchExpectedFunTys herald _ctxt arity (Infer inf_res) thing_inside
    = do { arg_tys <- mapM (new_infer_arg_ty herald) [1 .. arity]
         ; res_ty  <- newInferExpType
         ; result  <- thing_inside (map ExpFunPatTy arg_tys) res_ty
         ; arg_tys <- mapM (\(Scaled m t) -> Scaled m <$> readExpType t) arg_tys
         ; res_ty  <- readExpType res_ty
 +         -- NB: mkScaledFunTys arg_tys res_ty does not contain any foralls
 +         -- (even nested ones), so no need to instantiate.
         ; co <- fillInferResult (mkScaledFunTys arg_tys res_ty) inf_res
         ; return (mkWpCastN co, result) }
@@ -1223,7 +1228,21 @@ unification variable.  We discard the evidence.
  -}
+-
 +-- | A version of 'fillInferResult' that also performs deep instantiation
 +-- when deep subsumption is enabled.
 +--
 +-- See also Note [Instantiation of InferResult].
 +fillInferResultDS :: CtOrigin -> TcRhoType -> InferResult -> TcM HsWrapper
 +fillInferResultDS ct_orig rho inf_res
 +  = do { massertPpr (isRhoTy rho) $
 +           vcat [ text "fillInferResultDS: input type is not a rho-type"
 +                , text "ty:" <+> ppr rho ]
 +       ; ds_flag <- getDeepSubsumptionFlag
 +       ; case ds_flag of
 +              Shallow -> mkWpCastN <$> fillInferResult rho inf_res
 +              Deep    -> do { (inst_wrap, rho') <- deeplyInstantiate ct_orig rho
 +                            ; co <- fillInferResult rho' inf_res
 +                            ; return (mkWpCastN co <.> inst_wrap) } }
  {-
  ************************************************************************
@@ -1290,27 +1309,34 @@ tcWrapResultO :: CtOrigin -> HsExpr GhcRn -> HsExpr GhcTc -> TcSigmaType -> ExpR
  tcWrapResultO orig rn_expr expr actual_ty res_ty
    = do { traceTc "tcWrapResult" (vcat [ text "Actual:  " <+> ppr actual_ty
                                        , text "Expected:" <+> ppr res_ty ])
 -       ; wrap <- tcSubTypeNC orig GenSigCtxt (Just $ HsExprRnThing rn_expr) actual_ty res_ty
 +       ; wrap <- tcSubType orig GenSigCtxt (Just $ HsExprRnThing rn_expr) actual_ty res_ty
         ; return (mkHsWrap wrap expr) }
 -tcWrapResultMono :: HsExpr GhcRn -> HsExpr GhcTc
 -                 -> TcRhoType   -- Actual -- a rho-type not a sigma-type
 -                 -> ExpRhoType  -- Expected
 -                 -> TcM (HsExpr GhcTc)
 --- A version of tcWrapResult to use when the actual type is a
 +-- | A version of 'tcWrapResult' to use when the actual type is a
  -- rho-type, so nothing to instantiate; just go straight to unify.
 --- It means we don't need to pass in a CtOrigin
 +-- It means we don't need to pass in a CtOrigin.
 +tcWrapResultMono :: HasDebugCallStack
 +                 => HsExpr GhcRn -> HsExpr GhcTc
 +                 -> TcRhoType   -- ^ Actual; a rho-type, not a sigma-type
 +                 -> ExpRhoType  -- ^ Expected
 +                 -> TcM (HsExpr GhcTc)
  tcWrapResultMono rn_expr expr act_ty res_ty
 -  = assertPpr (isRhoTy act_ty) (ppr act_ty $$ ppr rn_expr) $
 -    do { co <- unifyExpectedType rn_expr act_ty res_ty
 +  = do { co <- tcSubTypeMono rn_expr act_ty res_ty
         ; return (mkHsWrapCo co expr) }
 -unifyExpectedType :: HsExpr GhcRn
 -                  -> TcRhoType   -- Actual -- a rho-type not a sigma-type
 -                  -> ExpRhoType  -- Expected
 -                  -> TcM TcCoercionN
 -unifyExpectedType rn_expr act_ty exp_ty
 -  = case exp_ty of
 +-- | A version of 'tcSubType' to use when the actual type is a rho-type,
 +-- so that no instantiation is needed.
 +tcSubTypeMono :: HasDebugCallStack
 +              => HsExpr GhcRn
 +              -> TcRhoType   -- ^ Actual; a rho-type, not a sigma-type
 +              -> ExpRhoType  -- ^ Expected
 +              -> TcM TcCoercionN
 +tcSubTypeMono rn_expr act_ty exp_ty
 +  = assertPpr (isDeepRhoTy act_ty)
 +      (vcat [ text "Actual type is not a (deep) rho-type."
 +            , text "act_ty:" <+> ppr act_ty
 +            , text "rn_expr:" <+> ppr rn_expr]) $
 +    case exp_ty of
        Infer inf_res -> fillInferResult act_ty inf_res
        Check exp_ty  -> unifyType (Just $ HsExprRnThing rn_expr) act_ty exp_ty
@@ -1331,46 +1357,39 @@ tcSubTypePat _ _ (Infer inf_res) ty_expected
         ; return (mkWpCastN (mkSymCo co)) }
  ---------------
 -tcSubType :: CtOrigin -> UserTypeCtxt
 -          -> TcSigmaType  -- ^ Actual
 -          -> ExpRhoType   -- ^ Expected
 -          -> TcM HsWrapper
 --- Checks that 'actual' is more polymorphic than 'expected'
 -tcSubType orig ctxt ty_actual ty_expected
 -  = addSubTypeCtxt ty_actual ty_expected $
 -    do { traceTc "tcSubType" (vcat [pprUserTypeCtxt ctxt, ppr ty_actual, ppr ty_expected])
 -       ; tcSubTypeNC orig ctxt Nothing ty_actual ty_expected }
 ----------------
 +-- | A subtype check that performs deep subsumption.
 +-- See also 'tcSubTypeMono', for when no instantiation is required.
  tcSubTypeDS :: HsExpr GhcRn
              -> TcRhoType   -- Actual type -- a rho-type not a sigma-type
              -> TcRhoType   -- Expected type
                             -- DeepSubsumption <=> when checking, this type
                             --                     is deeply skolemised
              -> TcM HsWrapper
 --- Similar signature to unifyExpectedType; does deep subsumption
  -- Only one call site, in GHC.Tc.Gen.App.tcApp
  tcSubTypeDS rn_expr act_rho exp_rho
 -  = tc_sub_type_deep (unifyExprType rn_expr) orig GenSigCtxt act_rho exp_rho
 +  = tc_sub_type_deep Top (unifyExprType rn_expr) orig GenSigCtxt act_rho exp_rho
    where
      orig = exprCtOrigin rn_expr
  ---------------
 -tcSubTypeNC :: CtOrigin          -- ^ Used when instantiating
 -            -> UserTypeCtxt      -- ^ Used when skolemising
 -            -> Maybe TypedThing -- ^ 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
++
 +-- | Checks that the 'actual' type is more polymorphic than the 'expected' type.
 +tcSubType :: CtOrigin          -- ^ Used when instantiating
 +          -> UserTypeCtxt      -- ^ Used when skolemising
 +          -> Maybe TypedThing -- ^ The expression that has type 'actual' (if known)
 +          -> TcSigmaType       -- ^ Actual type
 +          -> ExpRhoType        -- ^ Expected type
 +          -> TcM HsWrapper
 +tcSubType inst_orig ctxt m_thing ty_actual res_ty
    = case res_ty of
        Check ty_expected -> tc_sub_type (unifyType m_thing) inst_orig ctxt
                                         ty_actual ty_expected
        Infer inf_res -> do { (wrap, rho) <- topInstantiate inst_orig ty_actual
                                     -- See Note [Instantiation of InferResult]
 -                          ; co <- fillInferResult rho inf_res
 -                          ; return (mkWpCastN co <.> wrap) }
 +                          ; inst <- fillInferResultDS inst_orig rho inf_res
 +                          ; return (inst <.> wrap) }
  ---------------
  tcSubTypeSigma :: CtOrigin       -- where did the actual type arise / why are we
@@ -1388,9 +1407,9 @@ 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_ds Shallow (unifyType Nothing)
 -                           (AmbiguityCheckOrigin ctxt)
 -                           ctxt ty_actual ty_expected
 +  = tc_sub_type_ds Top Shallow (unifyType Nothing)
 +                             (AmbiguityCheckOrigin ctxt)
 +                             ctxt ty_actual ty_expected
  ---------------
  addSubTypeCtxt :: TcType -> ExpType -> TcM a -> TcM a
@@ -1411,8 +1430,9 @@ addSubTypeCtxt ty_actual ty_expected thing_inside
  {- Note [Instantiation of InferResult]
  ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 -We now always instantiate before filling in InferResult, so that
 -the result is a TcRhoType: see #17173 for discussion.
 +When typechecking expressions (not types, not patterns), we always instantiate
 +before filling in InferResult, so that the result is a TcRhoType.
 +See #17173 for discussion.
  For example:
@@ -1444,6 +1464,9 @@ For example:
  There is one place where we don't want to instantiate eagerly,
  namely in GHC.Tc.Module.tcRnExpr, which implements GHCi's :type
  command. See Note [Implementing :type] in GHC.Tc.Module.
++
 +This also means that, if DeepSubsumption is enabled, we should also instantiate
 +deeply; we do this by using fillInferResultDS.
  -}
  ---------------
@@ -1464,16 +1487,17 @@ tc_sub_type :: (TcType -> TcType -> TcM TcCoercionN)  -- How to unify
  ----------------------
  tc_sub_type unify inst_orig ctxt ty_actual ty_expected
    = do { ds_flag <- getDeepSubsumptionFlag
 -       ; tc_sub_type_ds ds_flag unify inst_orig ctxt ty_actual ty_expected }
 +       ; tc_sub_type_ds Top ds_flag unify inst_orig ctxt ty_actual ty_expected }
  ----------------------
 -tc_sub_type_ds :: DeepSubsumptionFlag
 +tc_sub_type_ds :: Position p -- ^ position in the type (for error messages only)
 +               -> DeepSubsumptionFlag
                 -> (TcType -> TcType -> TcM TcCoercionN)
                 -> CtOrigin -> UserTypeCtxt -> TcSigmaType
                 -> TcSigmaType -> TcM HsWrapper
  -- tc_sub_type_ds is the main subsumption worker function
  -- It takes an explicit DeepSubsumptionFlag
 -tc_sub_type_ds ds_flag unify inst_orig ctxt ty_actual ty_expected
 +tc_sub_type_ds pos ds_flag unify inst_orig ctxt ty_actual ty_expected
    | definitely_poly ty_expected   -- See Note [Don't skolemise unnecessarily]
    , isRhoTyDS ds_flag ty_actual
    = do { traceTc "tc_sub_type (drop to equality)" $
@@ -1490,7 +1514,7 @@ tc_sub_type_ds ds_flag unify inst_orig ctxt ty_actual ty_expected
         ; (sk_wrap, inner_wrap)
              <- tcSkolemise ds_flag ctxt ty_expected $ \sk_rho ->
                 case ds_flag of
 -                 Deep    -> tc_sub_type_deep unify inst_orig ctxt ty_actual sk_rho
 +                 Deep    -> tc_sub_type_deep pos unify inst_orig ctxt ty_actual sk_rho
                   Shallow -> tc_sub_type_shallow unify inst_orig ty_actual sk_rho
         ; return (sk_wrap <.> inner_wrap) }
@@ -1656,7 +1680,7 @@ The effects are in these main places:
     see the call to tcDeeplySkolemise in tcSkolemiseScoped.
 . In GHC.Tc.Gen.App.tcApp we call tcSubTypeDS to match the result
 -   type. Without deep subsumption, unifyExpectedType would be sufficent.
 +   type. Without deep subsumption, tcSubTypeMono would be sufficent.
  In all these cases note that the deep skolemisation must be done /first/.
  Consider (1)
@@ -1669,8 +1693,10 @@ Wrinkles:
  (DS1) Note that we /always/ use shallow subsumption in the ambiguity check.
        See Note [Ambiguity check and deep subsumption].
 -(DS2) Deep subsumption requires deep instantiation too.
 -      See Note [The need for deep instantiation]
 +(DS2) When doing deep subsumption, we must be careful not to needlessly
 +      drop down to unification, e.g. in cases such as:
 +        (Bool -> ∀ d. d->d)   <=   alpha beta gamma
 +      See Note [FunTy vs non-FunTy case in tc_sub_type_deep].
  (DS3) The interaction between deep subsumption and required foralls
        (forall a -> ty) is a bit subtle.  See #24696 and
@@ -1701,6 +1727,69 @@ ToDo: this eta-abstraction plays fast and loose with termination,
        because it can introduce extra lambdas.  Maybe add a `seq` to
        fix this
 +Note [FunTy vs FunTy case in tc_sub_type_deep]
 +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 +The goal of tc_sub_type_deep is to produce an HsWrapper that "proves" that the
 +actual type is a subtype of the expected type. The most important case is how
 +we deal with function arrows. Suppose we have:
++
 +  ty_actual   = act_arg -> act_res
 +  ty_expected = exp_arg -> exp_res
++
 +To produce fun_wrap :: (act_arg -> act_res) ~> (exp_arg -> exp_res), we use
 +the fact that the function arrow is contravariant in its argument type and
 +covariant in its result type. Thus we recursively perform subtype checks
 +on the argument types (with actual/expected switched) and the result types,
 +to get:
++
 +  arg_wrap :: exp_arg ~> act_arg   -- NB: expected/actual have switched sides
 +  res_wrap :: act_res ~> exp_res
++
 +Then fun_wrap = mkWpFun arg_wrap res_wrap.
++
 +Wrinkle [Representation-polymorphism checking during subtyping]
++
 +  Inserting a WpFun HsWrapper amounts to impedance matching in deep subsumption
 +  via eta-expansion:
++
 +    f  ==>  \ (x :: exp_arg) -> res_wrap [ f (arg_wrap [x]) ]
++
 +  As we produce a lambda, we must enforce the representation polymorphism
 +  invariants described in Note [Representation polymorphism invariants] in GHC.Core.
 +  That is, we must ensure that both x (the lambda binder) and (arg_wrap [x]) (the function argument)
 +  have a fixed runtime representation.
++
 +  Note however that desugaring mkWpFun does not always introduce a lambda: if
 +  both the argument and result HsWrappers are casts, then a FunCo cast suffices,
 +  in which case we should not perform representation-polymorphism checking.
++
 +  This means that, in the FunTy/FunTy case of tc_sub_type_deep, we can skip
 +  the representation-polymorphism checks if the produced argument and result
 +  wrappers are identities or casts.
 +  It is important to do so, otherwise we reject valid programs.
++
 +    Here's a contrived example (there are undoubtedly more natural examples)
 +    (see testsuite/tests/rep-poly/NoEtaRequired):
++
 +      type Id :: k -> k
 +      type family Id a where
++
 +      type T :: TYPE r -> TYPE (Id r)
 +      type family T a where
++
 +      test :: forall r (a :: TYPE r). a :~~: T a -> ()
 +      test HRefl =
 +        let
 +          f :: (a -> a) -> ()
 +          f _ = ()
 +          g :: T a -> T a
 +          g = undefined
 +        in f g
++
 +    We don't need to eta-expand `g` to make `f g` typecheck; a cast suffices.
 +    Hence we should not perform representation-polymorphism checks; they would
 +    fail here.
++
  Note [Setting the argument context]
  ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  Consider we are doing the ambiguity check for the (bogus)
@@ -1751,30 +1840,31 @@ complains.
  The easiest solution was to use tcEqMult in tc_sub_type_deep, and
  insist on equality. This is only in the DeepSubsumption code anyway.
 -Note [The need for deep instantiation]
 -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 +Note [FunTy vs non-FunTy case in tc_sub_type_deep]
 +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  Consider this, without Quick Look, but with Deep Subsumption:
     f :: ∀a b c. a b c -> Int
     g :: Bool -> ∀d. d -> d
 -Consider the application (f g).  We need to do the subsumption test
+-
 -  (Bool -> ∀ d. d->d)   <=   (alpha beta gamma)
 +To typecheck the application (f g), we need to do the subsumption test
 -where alpha, beta, gamma are the unification variables that instantiate a,b,c,
 -respectively.  We must not drop down to unification, or we will reject the call.
 -Rather we must deeply instantiate the LHS to get
 +  (Bool -> ∀ d. d->d)   <=   alpha beta gamma
 -  (Bool -> delta -> delta)   <=   (alpha beta gamma)
 +where alpha, beta, gamma are the unification variables that instantiate a,b,c
 +(respectively). We must not drop down to unification, or we will reject the call.
 +Instead, we should only unify alpha := (->), in which case we end up with the
 +usual FunTy vs FunTy case of Note [FunTy vs FunTy case in tc_sub_type_deep]:
 -and now we can unify to get
 +  (Bool -> ∀ d. d->d)   <=   beta -> gamma
 -   alpha = (->)
 -   beta = Bool
 -   gamma = delta -> delta
 +which is straightforwardly solved by beta := Bool, using covariance in the return
 +type of the function arrow, and instantiating the forall before unifying with gamma.
 -Hence the call to `deeplyInstantiate` in `tc_sub_type_deep`.
 +The conclusion is this: when doing a deep subtype check (in tc_sub_type_deep),
 +if the LHS is a FunTy and the RHS is a rho-type which is not a FunTy,
 +then unify the RHS with a FunTy and continue by performing a sub-type check on
 +the LHS vs the new RHS. And vice-versa (if it's the RHS that is a FunTy).
 -See typecheck/should_compile/T11305 for an example of when this is important.
 +See T11305 and T26225 for examples of when this is important.
  Note [Deep subsumption and required foralls]
  ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1837,12 +1927,17 @@ getDeepSubsumptionFlag :: TcM DeepSubsumptionFlag
  getDeepSubsumptionFlag = do { ds <- xoptM LangExt.DeepSubsumption
                              ; if ds then return Deep else return Shallow }
 +-- | 'tc_sub_type_deep' is where the actual work happens for deep subsumption.
 +--
 +-- Given @ty_actual@ (a sigma-type) and @ty_expected@ (deeply skolemised, i.e.
 +-- a deep rho type), it returns an 'HsWrapper' @wrap :: ty_actual ~> ty_expected@.
  tc_sub_type_deep :: HasDebugCallStack
 -                 => (TcType -> TcType -> TcM TcCoercionN)  -- How to unify
 -                 -> CtOrigin       -- Used when instantiating
 -                 -> UserTypeCtxt   -- Used when skolemising
 -                 -> TcSigmaType    -- Actual; a sigma-type
 -                 -> TcRhoType      -- Expected; deeply skolemised
 +                 => Position p     -- ^ Position in the type (for error messages only)
 +                 -> (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_deep t1 t2
@@ -1850,63 +1945,161 @@ tc_sub_type_deep :: HasDebugCallStack
  -- Here is where the work actually happens!
  -- Precondition: ty_expected is deeply skolemised
 -tc_sub_type_deep unify inst_orig ctxt ty_actual ty_expected
 +tc_sub_type_deep pos unify inst_orig ctxt ty_actual ty_expected
    = assertPpr (isDeepRhoTy ty_expected) (ppr ty_expected) $
      do { traceTc "tc_sub_type_deep" $
           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 coreView
 -    go ty_a ty_e | Just ty_a' <- coreView ty_a = go ty_a' ty_e
 -                 | Just ty_e' <- coreView ty_e = go ty_a  ty_e'
 -    go (TyVarTy tv_a) ty_e
 -      = do { lookup_res <- isFilledMetaTyVar_maybe tv_a
 +    -- 'unwrap' removes top-level type synonyms & looks through filled meta-tyvars
 +    unwrap :: TcType -> TcM TcType
 +    unwrap ty
 +      | Just ty' <- coreView ty
 +      = unwrap ty'
 +    unwrap ty@(TyVarTy tv)
 +      = do { lookup_res <- isFilledMetaTyVar_maybe tv
             ; case lookup_res of
 -               Just ty_a' ->
 -                 do { traceTc "tc_sub_type_deep following filled meta-tyvar:"
 -                        (ppr tv_a <+> text "-->" <+> ppr ty_a')
 -                    ; tc_sub_type_deep unify inst_orig ctxt ty_a' ty_e }
 -               Nothing -> just_unify ty_actual ty_expected }
+-
 -    go ty_a@(FunTy { ft_af = af1, ft_mult = act_mult, ft_arg = act_arg, ft_res = act_res })
 -       ty_e@(FunTy { ft_af = af2, ft_mult = exp_mult, ft_arg = exp_arg, ft_res = exp_res })
 -      | isVisibleFunArg af1, isVisibleFunArg af2
 -      = if (isTauTy ty_a && isTauTy ty_e)       -- Short cut common case to avoid
 -        then just_unify ty_actual ty_expected   -- unnecessary eta expansion
 -        else
 -        -- 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_ds Deep unify given_orig GenSigCtxt exp_arg act_arg
 -                          -- GenSigCtxt: See Note [Setting the argument context]
 -           ; res_wrap  <- tc_sub_type_deep unify inst_orig ctxt act_res exp_res
 -           ; tcEqMult inst_orig act_mult exp_mult
 -             -- See Note [Multiplicity in deep subsumption]
 -           ; return (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
 +                 Just ty' -> unwrap ty'
 +                 Nothing  -> return ty }
 +    unwrap ty = return ty
++
 +    go, go1 :: TcType -> TcType -> TcM HsWrapper
 +    go ty_a ty_e =
 +      do { ty_a' <- unwrap ty_a
 +         ; ty_e' <- unwrap ty_e
 +         ; go1 ty_a' ty_e' }
++
 +    -- If ty_actual is not a rho-type, instantiate it first; otherwise
 +    -- unification has no chance of succeeding.
 +    go1 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_deep unify inst_orig ctxt in_rho ty_e
 +           ; body_wrap <- go 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 Note [The need for deep instantiation]
 -             (inst_wrap, rho_a) <- deeplyInstantiate inst_orig ty_actual
 -           ; unify_wrap         <- just_unify rho_a ty_expected
 -           ; return (unify_wrap <.> inst_wrap) }
 +    -- Main case: FunTy vs FunTy. go_fun does the work.
 +    go1 (FunTy { ft_af = af1, ft_mult = act_mult, ft_arg = act_arg, ft_res = act_res })
 +        (FunTy { ft_af = af2, ft_mult = exp_mult, ft_arg = exp_arg, ft_res = exp_res })
 +      | isVisibleFunArg af1
 +      , isVisibleFunArg af2
 +      = go_fun af1 act_mult act_arg act_res
 +               af2 exp_mult exp_arg exp_res
++
 +    -- See Note [FunTy vs non-FunTy case in tc_sub_type_deep]
 +    go1 (FunTy { ft_af = af1, ft_mult = act_mult, ft_arg = act_arg, ft_res = act_res }) ty_e
 +      | isVisibleFunArg af1
 +      = do { exp_mult <- newMultiplicityVar
 +           ; exp_arg  <- newOpenFlexiTyVarTy -- NB: no FRR check needed; we might not need to eta-expand
 +           ; exp_res  <- newOpenFlexiTyVarTy
 +           ; let exp_funTy = FunTy { ft_af = af1, ft_mult = exp_mult, ft_arg = exp_arg, ft_res = exp_res }
 +           ; unify_wrap <- just_unify exp_funTy ty_e
 +           ; fun_wrap <- go_fun af1 act_mult act_arg act_res af1 exp_mult exp_arg exp_res
 +           ; return $ unify_wrap <.> fun_wrap
 +             -- unify_wrap :: exp_funTy ~> ty_e
 +             -- fun_wrap :: ty_a ~> exp_funTy
 +           }
 +    go1 ty_a (FunTy { ft_af = af2, ft_mult = exp_mult, ft_arg = exp_arg, ft_res = exp_res })
 +      | isVisibleFunArg af2
 +      = do { act_mult <- newMultiplicityVar
 +           ; act_arg  <- newOpenFlexiTyVarTy -- NB: no FRR check needed; we might not need to eta-expand
 +           ; act_res  <- newOpenFlexiTyVarTy
 +           ; let act_funTy = FunTy { ft_af = af2, ft_mult = act_mult, ft_arg = act_arg, ft_res = act_res }
++
 +           ; unify_wrap <- just_unify ty_a act_funTy
 +           ; fun_wrap <- go_fun af2 act_mult act_arg act_res af2 exp_mult exp_arg exp_res
 +           ; return $ fun_wrap <.> unify_wrap
 +             -- unify_wrap :: ty_a ~> act_funTy
 +             -- fun_wrap :: act_funTy ~> ty_e
 +           }
++
 +    -- Otherwise, revert to unification.
 +    go1 ty_a ty_e = just_unify ty_a ty_e
      just_unify ty_a ty_e = do { cow <- unify ty_a ty_e
                                ; return (mkWpCastN cow) }
 +    -- FunTy/FunTy case: this is where we insert any necessary eta-expansions.
 +    go_fun :: FunTyFlag -> Mult -> TcType -> TcType -- actual FunTy
 +           -> FunTyFlag -> Mult -> TcType -> TcType -- expected FunTy
 +           -> TcM HsWrapper
 +    go_fun act_af act_mult act_arg act_res exp_af exp_mult exp_arg exp_res
 +      -- See Note [FunTy vs FunTy case in tc_sub_type_deep]
 +      = do { arg_wrap  <- tc_sub_type_ds (Argument pos) Deep unify given_orig GenSigCtxt exp_arg act_arg
 +                          -- GenSigCtxt: See Note [Setting the argument context]
 +           ; res_wrap  <- tc_sub_type_deep (Result pos) unify inst_orig ctxt act_res exp_res
++
 +             -- See Note [Multiplicity in deep subsumption]
 +           ; tcEqMult inst_orig act_mult exp_mult
++
 +           ; mkWpFun_FRR pos
 +               act_af act_mult act_arg act_res
 +               exp_af exp_mult exp_arg exp_res
 +               arg_wrap res_wrap
 +           }
 +      where
 +        given_orig = GivenOrigin (SigSkol GenSigCtxt exp_arg [])
++
 +-- | Like 'mkWpFun', except that it performs representation-polymorphism
 +-- checks on the argument type.
 +mkWpFun_FRR
 +  :: Position p
 +  -> FunTyFlag -> Type -> TcType -> Type --   actual FunTy
 +  -> FunTyFlag -> Type -> TcType -> Type -- expected FunTy
 +  -> HsWrapper -- ^ exp_arg ~> act_arg
 +  -> HsWrapper -- ^ act_res ~> exp_res
 +  -> TcM HsWrapper -- ^ act_funTy ~> exp_funTy
 +mkWpFun_FRR pos act_af act_mult act_arg act_res exp_af exp_mult exp_arg exp_res arg_wrap res_wrap
 +  | needs_eta
 +  -- See Wrinkle [Representation-polymorphism checking during subtyping]
 +  = do { (exp_arg_co,  exp_arg_frr) <- hasFixedRuntimeRep (FRRDeepSubsumption True pos) exp_arg
 +       ; (act_arg_co, _act_arg_frr) <- hasFixedRuntimeRep (FRRDeepSubsumption False pos) act_arg
 +       ; let
 +            exp_arg_fun_co =
 +              mkFunCo Nominal exp_af
 +                 (mkReflCo Nominal exp_mult)
 +                 (mkSymCo exp_arg_co)
 +                 (mkReflCo Nominal exp_res)
 +            act_arg_fun_co =
 +              mkFunCo Nominal act_af
 +                 (mkReflCo Nominal act_mult)
 +                 act_arg_co
 +                 (mkReflCo Nominal act_res)
 +            arg_wrap_frr =
 +              mkWpCastN (mkSymCo exp_arg_co) <.> arg_wrap <.> mkWpCastN act_arg_co
 +               --  exp_arg_co :: exp_arg ~> exp_arg_frr
 +               --  act_arg_co :: act_arg ~> act_arg_frr
 +               --  arg_wrap :: exp_arg ~> act_arg
 +               --  arg_wrap_frr :: exp_arg_frr ~> act_arg_frr
++
 +       -- NB: because of the needs_eta guard, we know that mkWpFun will
 +       -- return (WpFun ...); so we might as well just use the WpFun constructor.
 +       ; return $
 +            mkWpCastN exp_arg_fun_co
 +              <.>
 +            WpFun arg_wrap_frr res_wrap (Scaled exp_mult exp_arg_frr)
 +              <.>
 +            mkWpCastN act_arg_fun_co }
 +  | otherwise
 +  = return $
 +      mkWpFun arg_wrap res_wrap (Scaled exp_mult exp_arg) exp_res
 +        -- NB: because of 'needs_eta', this will never actually be a WpFun.
 +        -- mkWpFun will turn it into a WpHole or WpCast, which is why
 +        -- we can skip the hasFixedRuntimeRep checks in this case.
 +        -- See Wrinkle [Representation-polymorphism checking during subtyping]
 +  where
 +    needs_eta :: Bool
 +    needs_eta =
 +      not (hole_or_cast arg_wrap)
 +        ||
 +      not (hole_or_cast res_wrap)
 +    hole_or_cast :: HsWrapper -> Bool
 +    hole_or_cast WpHole = True
 +    hole_or_cast (WpCast {}) = True
 +    hole_or_cast _ = False
++
  -----------------------
  deeplySkolemise :: SkolemInfo -> TcSigmaType
                  -> TcM ( HsWrapper

compiler/GHC/Types/Id/Make.hs

@@ -1950,7 +1950,7 @@ seqId = pcRepPolyId seqName ty concs info
            Case (Var x) x openBetaTy [Alt DEFAULT [] (Var y)]
      concs = mkRepPolyIdConcreteTyVars
 -        [ ((openBetaTy, Argument 2 Top), runtimeRep2TyVar)]
 +        [ ((openBetaTy, mkArgPos 2 Top), runtimeRep2TyVar)]
      arity = 2
@@ -2009,7 +2009,7 @@ oneShotId = pcRepPolyId oneShotName ty concs info
      arity = 2
      concs = mkRepPolyIdConcreteTyVars
 -        [((openAlphaTy, Argument 2 Top), runtimeRep1TyVar)]
 +        [((openAlphaTy, mkArgPos 2 Top), runtimeRep1TyVar)]
  ----------------------------------------------------------------------
  {- Note [Wired-in Ids for rebindable syntax]
@@ -2054,7 +2054,7 @@ leftSectionId = pcRepPolyId leftSectionName ty concs info
      arity = 2
      concs = mkRepPolyIdConcreteTyVars
 -            [((openAlphaTy, Argument 2 Top), runtimeRep1TyVar)]
 +            [((openAlphaTy, mkArgPos 2 Top), runtimeRep1TyVar)]
  -- See Note [Left and right sections] in GHC.Rename.Expr
  -- See Note [Wired-in Ids for rebindable syntax]
@@ -2088,8 +2088,8 @@ rightSectionId = pcRepPolyId rightSectionName ty concs info
      concs =
        mkRepPolyIdConcreteTyVars
 -        [ ((openAlphaTy, Argument 3 Top), runtimeRep1TyVar)
 -        , ((openBetaTy , Argument 2 Top), runtimeRep2TyVar)]
 +        [ ((openAlphaTy, mkArgPos 3 Top), runtimeRep1TyVar)
 +        , ((openBetaTy , mkArgPos 2 Top), runtimeRep2TyVar)]
  --------------------------------------------------------------------------------
@@ -2119,7 +2119,7 @@ coerceId = pcRepPolyId coerceName ty concs info
            [Alt (DataAlt coercibleDataCon) [eq] (Cast (Var x) (mkCoVarCo eq))]
      concs = mkRepPolyIdConcreteTyVars
 -            [((mkTyVarTy av, Argument 1 Top), rv)]
 +            [((mkTyVarTy av, mkArgPos 1 Top), rv)]
  {-
  Note [seqId magic]

testsuite/tests/corelint/LintEtaExpand.stderr

@@ -15,7 +15,7 @@ in coerce BAD 1
                     CvSubst   = []>
  in coerce BAD 2
  <no location info>: warning:
 -    • The return type of the first argument of the primop ‘catch#’ does not have a fixed runtime representation:
 +    • The result of the first argument of the primop ‘catch#’ does not have a fixed runtime representation:
          a :: TYPE q
      Substitution: <InScope = {a q}
                     IdSubst   = []
@@ -23,7 +23,7 @@ in coerce BAD 2
                     CvSubst   = []>
  in catch# BAD 1
  <no location info>: warning:
 -    • The return type of the first argument of the primop ‘catch#’ does not have a fixed runtime representation:
 +    • The result of the first argument of the primop ‘catch#’ does not have a fixed runtime representation:
          ‘q’ is not concrete.
      Substitution: <InScope = {a q}
                     IdSubst   = []

testsuite/tests/indexed-types/should_fail/T5439.stderr

+-
 -T5439.hs:83:33: error: [GHC-83865]
 -    • Couldn't match expected type: Attempt (HElemOf rs)
 -                  with actual type: Attempt (HHead (HDrop n0 l0))
 -                                    -> Attempt (HElemOf l0)
 -    • Probable cause: ‘($)’ is applied to too few arguments
 -      In the second argument of ‘($)’, namely
 -        ‘inj $ Failure (e :: SomeException)’
 +T5439.hs:83:28: error: [GHC-83865]
 +    • Couldn't match type: Attempt (HElemOf rs)
 +                     with: Attempt (HHead (HDrop n0 l0)) -> Attempt (HElemOf l0)
 +      Expected: f (Attempt (HHead (HDrop n0 l0)) -> Attempt (HElemOf l0))
 +        Actual: f (Attempt (WaitOpResult (WaitOps rs)))
 +    • In the first argument of ‘complete’, namely ‘ev’
 +      In the first argument of ‘($)’, namely ‘complete ev’
        In a stmt of a 'do' block:
          c <- complete ev $ inj $ Failure (e :: SomeException)
 -      In the expression:
 -        do c <- complete ev $ inj $ Failure (e :: SomeException)
 -           return $ c || not first
      • Relevant bindings include
          register :: Bool -> Peano n -> WaitOps (HDrop n rs) -> IO Bool
            (bound at T5439.hs:65:9)
@@ -30,3 +26,4 @@ T5439.hs:83:39: error: [GHC-83865]
          ‘inj $ Failure (e :: SomeException)’
        In a stmt of a 'do' block:
          c <- complete ev $ inj $ Failure (e :: SomeException)
++

testsuite/tests/partial-sigs/should_compile/T10403.stderr

+-
  T10403.hs:16:7: warning: [GHC-88464] [-Wpartial-type-signatures (in -Wdefault)]
      • Found extra-constraints wildcard standing for ‘Functor f’
        Where: ‘f’ is a rigid type variable bound by
 -               the inferred type of h1 :: Functor f => (a1 -> a2) -> f a1 -> H f
 +               the inferred type of h1 :: Functor f => (t -> b) -> f t -> H f
                 at T10403.hs:18:1-41
      • In the type signature: h1 :: _ => _
  T10403.hs:16:12: warning: [GHC-88464] [-Wpartial-type-signatures (in -Wdefault)]
 -    • Found type wildcard ‘_’ standing for ‘(a1 -> a2) -> f a1 -> H f’
 -      Where: ‘a2’, ‘a1’, ‘f’ are rigid type variables bound by
 -               the inferred type of h1 :: Functor f => (a1 -> a2) -> f a1 -> H f
 +    • Found type wildcard ‘_’ standing for ‘(t -> b) -> f t -> H f’
 +      Where: ‘b’, ‘t’, ‘f’ are rigid type variables bound by
 +               the inferred type of h1 :: Functor f => (t -> b) -> f t -> H f
                 at T10403.hs:18:1-41
      • In the type signature: h1 :: _ => _
  T10403.hs:20:7: warning: [GHC-88464] [-Wpartial-type-signatures (in -Wdefault)]
 -    • Found type wildcard ‘_’ standing for ‘(a1 -> a2) -> f a1 -> H f’
 -      Where: ‘a2’, ‘a1’, ‘f’ are rigid type variables bound by
 -               the inferred type of h2 :: (a1 -> a2) -> f a1 -> H f
 +    • Found type wildcard ‘_’ standing for ‘(t -> b) -> f t -> H f’
 +      Where: ‘b’, ‘t’, ‘f’ are rigid type variables bound by
 +               the inferred type of h2 :: (t -> b) -> f t -> H f
                 at T10403.hs:23:1-41
      • In the type signature: h2 :: _
@@ -24,7 +23,8 @@ T10403.hs:23:15: warning: [GHC-39999] [-Wdeferred-type-errors (in -Wdefault)]
      • No instance for ‘Functor f’ arising from a use of ‘fmap’
        Possible fix:
          add (Functor f) to the context of
 -          the inferred type of h2 :: (a1 -> a2) -> f a1 -> H f
 +          the inferred type of h2 :: (t -> b) -> f t -> H f
      • In the second argument of ‘(.)’, namely ‘fmap (const ())’
        In the expression: (H . fmap (const ())) (fmap f b)
        In an equation for ‘h2’: h2 f b = (H . fmap (const ())) (fmap f b)
++

testsuite/tests/partial-sigs/should_fail/T10615.stderr

+-
  T10615.hs:5:7: error: [GHC-88464]
 -    • Found type wildcard ‘_’ standing for ‘w’
 -      Where: ‘w’ is a rigid type variable bound by
 -               the inferred type of f1 :: w -> f
 +    • Found type wildcard ‘_’ standing for ‘t’
 +      Where: ‘t’ is a rigid type variable bound by
 +               the inferred type of f1 :: t -> f
                 at T10615.hs:6:1-10
        To use the inferred type, enable PartialTypeSignatures
      • In the type signature: f1 :: _ -> f
  T10615.hs:6:6: error: [GHC-25897]
 -    • Couldn't match type ‘f’ with ‘b1 -> w’
 -      Expected: w -> f
 -        Actual: w -> b1 -> w
 +    • Couldn't match expected type ‘f’ with actual type ‘b1 -> t’
        ‘f’ is a rigid type variable bound by
 -        the inferred type of f1 :: w -> f
 +        the inferred type of f1 :: t -> f
          at T10615.hs:5:1-12
      • In the expression: const
        In an equation for ‘f1’: f1 = const
 -    • Relevant bindings include f1 :: w -> f (bound at T10615.hs:6:1)
 +    • Relevant bindings include f1 :: t -> f (bound at T10615.hs:6:1)
  T10615.hs:8:7: error: [GHC-88464]
 -    • Found type wildcard ‘_’ standing for ‘w’
 -      Where: ‘w’ is a rigid type variable bound by
 -               the inferred type of f2 :: w -> _f
 +    • Found type wildcard ‘_’ standing for ‘t’
 +      Where: ‘t’ is a rigid type variable bound by
 +               the inferred type of f2 :: t -> _f
                 at T10615.hs:9:1-10
        To use the inferred type, enable PartialTypeSignatures
      • In the type signature: f2 :: _ -> _f
  T10615.hs:9:6: error: [GHC-25897]
 -    • Couldn't match type ‘_f’ with ‘b0 -> w’
 -      Expected: w -> _f
 -        Actual: w -> b0 -> w
 +    • Couldn't match expected type ‘_f’ with actual type ‘b0 -> t’
        ‘_f’ is a rigid type variable bound by
 -        the inferred type of f2 :: w -> _f
 +        the inferred type of f2 :: t -> _f
          at T10615.hs:8:1-13
      • In the expression: const
        In an equation for ‘f2’: f2 = const
 -    • Relevant bindings include f2 :: w -> _f (bound at T10615.hs:9:1)
 +    • Relevant bindings include f2 :: t -> _f (bound at T10615.hs:9:1)

testsuite/tests/rep-poly/NoEtaRequired.hs

 +{-# LANGUAGE Haskell2010 #-}
 +{-# LANGUAGE DataKinds, TypeFamilies, PolyKinds, StandaloneKindSignatures #-}
 +{-# LANGUAGE RankNTypes #-}
 +{-# LANGUAGE ScopedTypeVariables #-}
 +{-# LANGUAGE TypeOperators #-}
 +{-# LANGUAGE UndecidableInstances #-}
++
 +module NoEtaRequired where
++
 +import Data.Proxy
 +import Data.Type.Equality ( (:~~:)(..) )
 +import GHC.Exts ( TYPE, RuntimeRep(..) )
++
 +type Id :: k -> k
 +type family Id a where
++
 +type T :: TYPE r -> TYPE (Id r)
 +type family T a where
++
 +test :: forall r (a :: TYPE r). a :~~: T a -> ()
 +test HRefl =
 +  let
 +    f :: (a -> a) -> ()
 +    f _ = ()
 +    g :: T a -> T a
 +    g = undefined
 +  in f g
 +-- This test makes sure we DO NOT eta-expand 'g' to '\ x -> g x' when trying
 +-- to make 'f g' typecheck. We CANNOT eta-expand here, as the binder 'x' would
 +-- not have a fixed runtime representation.
++

testsuite/tests/rep-poly/T21906.stderr

  T21906.hs:14:17: error: [GHC-55287]
 -    • The return type of the third argument of the primop ‘keepAlive#’
 +    • The result of the third argument of the primop ‘keepAlive#’
        does not have a fixed runtime representation.
        Its type is:
          b1 :: TYPE r1
@@ -12,7 +12,7 @@ T21906.hs:14:17: error: [GHC-55287]
        In an equation for ‘test1’: test1 val s f = keepAlive# val s f
  T21906.hs:21:25: error: [GHC-55287]
 -    • The return type of the first argument of the primop ‘catch#’
 +    • The result of the first argument of the primop ‘catch#’
        does not have a fixed runtime representation.
        Its type is:
          a1 :: TYPE q1
@@ -26,7 +26,7 @@ T21906.hs:21:25: error: [GHC-55287]
            test2 action handle s = catch# action handle s
  T21906.hs:30:17: error: [GHC-55287]
 -    • The nested return type inside the second argument of the primop ‘control0#’
 +    • The result of the first argument of the first argument of the second argument of the primop ‘control0#’
        does not have a fixed runtime representation.
        Its type is:
          b0 :: TYPE r0
@@ -39,7 +39,7 @@ T21906.hs:30:17: error: [GHC-55287]
        In an equation for ‘test3’: test3 tag f s = control0# tag f s
  T21906.hs:35:19: error: [GHC-55287]
 -    • The return type of the first argument of the primop ‘fork#’
 +    • The result of the first argument of the primop ‘fork#’
        does not have a fixed runtime representation.
        Its type is:
          a0 :: TYPE q0

testsuite/tests/rep-poly/all.T

@@ -112,6 +112,7 @@ test('RepPolyWrappedVar', normal, compile_fail, [''])
  test('RepPolyWrappedVar2', [js_skip], compile, [''])
  test('UnliftedNewtypesCoerceFail', normal, compile_fail, [''])
  test('UnliftedNewtypesLevityBinder', normal, compile_fail, [''])
 +test('NoEtaRequired', normal, compile, [''])
  ###############################################################################
  ## The following tests require rewriting in RuntimeReps,                     ##

testsuite/tests/typecheck/should_compile/T26225.hs

 +{-# LANGUAGE DeepSubsumption #-}
 +{-# LANGUAGE NamedWildCards #-}
 +{-# LANGUAGE PartialTypeSignatures #-}
 +{-# LANGUAGE TypeFamilies #-}
 +{-# LANGUAGE UnicodeSyntax #-}
++
 +{-# OPTIONS_GHC -Wno-partial-type-signatures #-}
++
 +module T26225 where
++
 +-- Recall: ty1 is a subtype of ty2, written ty1 ⊑ ty2,
 +--         if we can use ty1 wherever ty2 is expected.
 +--         Can also read as "ty1 is more polymorphic than ty2".
 +-- Example: ∀ a. a -> a  ⊑  Int -> Int, meaning that we can pass
 +--          the identity function where one is expecting a function of type Int -> Int.
++
 +-- Int -> (∀ a. a -> a)  ⊑  α[tau]
 +-- Accepted by GHC.
 +ex0 :: ()
 +ex0 =
 +  let
 +    f :: Int -> (∀ a. a -> a)
 +    f _ = id
 +    g :: _α -> ()
 +    g _ = ()
 +  in g f
++
 +-- ((∀ a. a->a) -> Int) -> Bool  ⊑  α[tau]
 +-- Rejected by GHC up to and including 9.14.
 +ex1' :: ()
 +ex1' =
 +  let
 +    f :: ((∀ a. a -> a) -> Int) -> Bool
 +    f _ = False
 +    g :: _α -> ()
 +    g _ = ()
 +  in g f
 +    -- Couldn't match expected type ‘α’ with actual type ‘((∀ a. a -> a) -> Int) -> Bool’
++
 +-- ((∀ a. a->a) -> Int) -> Bool  ⊑  β[tau] Bool
 +-- Rejected by GHC up to and including 9.14.
 +ex2' :: ()
 +ex2' =
 +  let
 +    f :: ((∀ a. a -> a) -> Int) -> Bool
 +    f _ = False
 +    g :: _β Bool -> ()
 +    g _ = ()
 +  in g f
 +    -- Couldn't match expected type ‘β’ with actual type ‘(->) ((∀ a. a -> a) -> Int)’
++
 +-- ex3 ::  β[tau] Bool  ⊑  (∀ a. a->a) -> Bool
 +-- Rejected by GHC up to and including 9.14.
 +ex3 :: ()
 +ex3 =
 +  let
 +    f :: _β Bool
 +    f = undefined
 +    g :: ((∀ a. a -> a) -> Bool) -> ()
 +    g _ = ()
 +  in g f
 +    -- Couldn't match expected type ‘β’ with actual type ‘(->) (∀ a. a -> a)’
++
 +-- ex3' :: F Int Bool  ⊑  (∀ a. a->a) -> Bool, where F Int = (->) (Int -> Int)
 +-- Rejected by GHC up to and including 9.14.
 +ex3' :: ()
 +ex3' =
 +  let
 +    f :: F Int Bool
 +    f _ = False
 +    g :: ((∀ a. a -> a) -> Bool) -> ()
 +    g _ = ()
 +  in g f
 +    -- • Couldn't match type: Int -> Int
 +    --             with: ∀ a. a -> a
 +    --   Expected: (∀ a. a -> a) -> Bool
 +    --     Actual: F Int Bool
 +type family F a where { F Int = (->) (Int -> Int) }

testsuite/tests/typecheck/should_compile/T26225b.hs

 +{-# LANGUAGE DeepSubsumption #-}
 +{-# LANGUAGE RankNTypes #-}
++
 +module T26225b where
++
 +f :: Int -> (forall a. a->a)
 +f _ x = x
 +g :: Int -> Bool -> Bool
 +g _ x = x
++
 +test3 b =
 +  case b of
 +    True  -> f
 +    False -> g
 +test3' b =
 +  case b of
 +    True  -> g
 +    False -> f
 +-- Both of these currently error with:
 +--   * Couldn't match type: forall a. a -> a
 +--                    with: Bool -> Bool

testsuite/tests/typecheck/should_compile/all.T

@@ -861,6 +861,8 @@ test('DeepSubsumption06', normal, compile, ['-XHaskell98'])
  test('DeepSubsumption07', normal, compile, ['-XHaskell2010'])
  test('DeepSubsumption08', normal, compile, [''])
  test('DeepSubsumption09', normal, compile, [''])
 +test('T26225', normal, compile, [''])
 +test('T26225b', normal, compile, [''])
  test('T21765', normal, compile, [''])
  test('T21951a', normal, compile, ['-Wredundant-strictness-flags'])
  test('T21951b', normal, compile, ['-Wredundant-strictness-flags'])

testsuite/tests/typecheck/should_fail/T12563.stderr deleted

+-
 -T12563.hs:8:15: error: [GHC-91028]
 -    • Couldn't match expected type ‘(forall a. f a) -> f r’
 -                  with actual type ‘p’
 -      Cannot equate type variable ‘p’
 -      with a type involving polytypes: (forall a. f a) -> f r
 -      ‘p’ is a rigid type variable bound by
 -        the inferred type of x :: p -> f r
 -        at T12563.hs:8:1-15
 -    • In the first argument of ‘foo’, namely ‘g’
 -      In the expression: foo g
 -      In the expression: \ g -> foo g
 -    • Relevant bindings include
 -        g :: p (bound at T12563.hs:8:6)
 -        x :: p -> f r (bound at T12563.hs:8:1)

testsuite/tests/typecheck/should_fail/T14618.stderr

+-
  T14618.hs:7:14: error: [GHC-25897]
      • Couldn't match expected type ‘b’ with actual type ‘a’
        ‘a’ is a rigid type variable bound by
@@ -19,3 +18,4 @@ T14618.hs:7:14: error: [GHC-25897]
                  f' = f
      • Relevant bindings include
          safeCoerce :: a -> b (bound at T14618.hs:7:1)
++

testsuite/tests/typecheck/should_fail/T6022.stderr

+-
  T6022.hs:4:1: error: [GHC-80003]
 -    • Non type-variable argument in the constraint: Eq ([a] -> a)
 +    • Non type-variable argument in the constraint: Eq ([t] -> t)
      • When checking the inferred type
 -        f :: forall {a}. Eq ([a] -> a) => ([a] -> a) -> Bool
 +        f :: forall {t}. Eq ([t] -> t) => ([t] -> t) -> Bool
      Suggested fix:
        Perhaps you intended to use the ‘FlexibleContexts’ extension
++

testsuite/tests/typecheck/should_fail/T8883.stderr

+-
  T8883.hs:21:1: error: [GHC-80003]
 -    • Non type-variable argument in the constraint: Functor (PF a)
 +    • Non type-variable argument in the constraint: Functor (PF t)
      • When checking the inferred type
 -        fold :: forall {a} {b}.
 -                (Functor (PF a), Regular a) =>
 -                (PF a b -> b) -> a -> b
 +        fold :: forall {t} {b}.
 +                (Functor (PF t), Regular t) =>
 +                (PF t b -> b) -> t -> b
      Suggested fix:
        Perhaps you intended to use the ‘FlexibleContexts’ extension
++

testsuite/tests/typecheck/should_fail/all.T

@@ -432,7 +432,7 @@ test('T12124', normal, compile_fail, [''])
  test('T12430', normal, compile_fail, [''])
  test('T12589', normal, compile_fail, [''])
  test('T12529', normal, compile_fail, [''])
 -test('T12563', normal, compile_fail, [''])
 +test('T12563', normal, compile, ['']) # Turns out we can accept this one after all!
  test('T12648', normal, compile_fail, [''])
  test('T12729', normal, compile_fail, [''])
  test('T12785b', normal, compile_fail, [''])

testsuite/tests/typecheck/should_fail/tcfail140.stderr

+-
  tcfail140.hs:11:7: error: [GHC-83865]
      • Couldn't match expected type ‘t1 -> t’ with actual type ‘Int’
      • The function ‘f’ is applied to two visible arguments,
@@ -17,13 +16,13 @@ tcfail140.hs:13:10: error: [GHC-83865]
          rot :: p -> t (bound at tcfail140.hs:13:1)
  tcfail140.hs:15:15: error: [GHC-83865]
 -    • Couldn't match expected type ‘a -> b’ with actual type ‘Int’
 +    • Couldn't match expected type ‘t -> b’ with actual type ‘Int’
      • In the first argument of ‘map’, namely ‘(3 `f`)’
        In the expression: map (3 `f`) xs
        In an equation for ‘bot’: bot xs = map (3 `f`) xs
      • Relevant bindings include
 -        xs :: [a] (bound at tcfail140.hs:15:5)
 -        bot :: [a] -> [b] (bound at tcfail140.hs:15:1)
 +        xs :: [t] (bound at tcfail140.hs:15:5)
 +        bot :: [t] -> [b] (bound at tcfail140.hs:15:1)
  tcfail140.hs:17:8: error: [GHC-27346]
      • The data constructor ‘Just’ should have 1 argument, but has been given none
@@ -36,3 +35,4 @@ tcfail140.hs:20:1: error: [GHC-83865]
      • Couldn't match expected type ‘Int’ with actual type ‘t0 -> Bool’
      • The equation for ‘g’ has two visible arguments,
          but its type ‘Int -> Int’ has only one
++