Typecheck remaining ValArgs in rebuildHsApps

This patch refactors hasFixedRuntimeRep_remainingValArgs, renaming it
to tcRemainingValArgs. The logic is moved to rebuildHsApps, which
ensures consistent behaviour across tcApp and quickLookArg1/tcEValArg.

This patch also refactors the treatment of stupid theta for data
constructors, changing the place we drop stupid theta arguments
from dsConLike to mkDataConRep (now the datacon wrapper drops these
arguments).

We decided not to implement PHASE 2 of the FixedRuntimeRep plan for
these remaining ValArgs. Future directions are outlined on the wiki:
  https://gitlab.haskell.org/ghc/ghc/-/wikis/Remaining-ValArgs

Fixes #21544 and #21650

11 files changed, 514 insertions, 404 deletions

diff --git a/compiler/GHC/Core/DataCon.hs b/compiler/GHC/Core/DataCon.hs
index 064cdc866f..01ab6414c3 100644
--- a/compiler/GHC/Core/DataCon.hs
+++ b/compiler/GHC/Core/DataCon.hs
@@ -250,6 +250,8 @@ in wrapper_reqd in GHC.Types.Id.Make.mkDataConRep.
 * Type variables may be permuted; see MkId
   Note [Data con wrappers and GADT syntax]
 
+* Datatype contexts require dropping some dictionary arguments.
+  See Note [Instantiating stupid theta].
 
 Note [The stupid context]
 ~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -282,7 +284,7 @@ gets inferred type
 
 I say the context is "stupid" because the dictionaries passed
 are immediately discarded -- they do nothing and have no benefit.
-(See Note [Instantiating stupid theta] in GHC.Tc.Gen.Head.)
+(See Note [Instantiating stupid theta].)
 It's a flaw in the language.
 
 GHC has made some efforts to correct this flaw. In GHC, datatype contexts
@@ -326,6 +328,30 @@ Some other notes about stupid contexts:
   result, dcStupidTheta is always empty for data types defined using GADT
   syntax.
 
+Note [Instantiating stupid theta]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider a data type with a "stupid theta" (see
+Note [The stupid context]):
+
+  data Ord a => T a = MkT (Maybe a)
+
+We want to generate an Ord constraint for every use of MkT; but
+we also want to allow visible type application, such as
+
+   MkT @Int
+
+To achieve this, the wrapper for a data (or newtype) constructor
+with a datatype context contains a lambda which drops the dictionary
+argments corresponding to the datatype context:
+
+   /\a \(_d:Ord a). MkT @a
+
+Notice that the wrapper discards the dictionary argument d.
+We don't need it; it was only there to generate a Wanted constraint.
+(That is why it is stupid.)
+
+This all happens in GHC.Types.Id.Make.mkDataConRep.
+
 ************************************************************************
 *                                                                      *
 \subsection{Data constructors}
@@ -1449,9 +1475,10 @@ dataConWrapperType :: DataCon -> Type
 -- mentions the family tycon, not the internal one.
 dataConWrapperType (MkData { dcUserTyVarBinders = user_tvbs,
                              dcOtherTheta = theta, dcOrigArgTys = arg_tys,
-                             dcOrigResTy = res_ty })
+                             dcOrigResTy = res_ty,
+                             dcStupidTheta = stupid_theta })
   = mkInvisForAllTys user_tvbs $
-    mkInvisFunTysMany theta $
+    mkInvisFunTysMany (stupid_theta ++ theta) $
     mkVisFunTys arg_tys $
     res_ty
 
diff --git a/compiler/GHC/Core/Lint.hs b/compiler/GHC/Core/Lint.hs
index f9cac8af61..f6043bdbfa 100644
--- a/compiler/GHC/Core/Lint.hs
+++ b/compiler/GHC/Core/Lint.hs
@@ -1167,7 +1167,7 @@ checkCanEtaExpand (Var fun_id) args app_ty
             = ty : go (i+1) bndrs
 
       bad_arg_tys :: [Type]
-      bad_arg_tys = check_args . map fst $ getRuntimeArgTys app_ty
+      bad_arg_tys = check_args . map (scaledThing . fst) $ getRuntimeArgTys app_ty
         -- We use 'getRuntimeArgTys' to find all the argument types,
         -- including those hidden under newtypes. For example,
         -- if `FunNT a b` is a newtype around `a -> b`, then
diff --git a/compiler/GHC/Core/Opt/Simplify.hs b/compiler/GHC/Core/Opt/Simplify.hs
index f052bae942..c44fd1d62a 100644
--- a/compiler/GHC/Core/Opt/Simplify.hs
+++ b/compiler/GHC/Core/Opt/Simplify.hs
@@ -2904,8 +2904,14 @@ doCaseToLet scrut case_bndr
   | isTyCoVar case_bndr    -- Respect GHC.Core
   = isTyCoArg scrut        -- Note [Core type and coercion invariant]
 
-  | isUnliftedType (idType case_bndr)
-    -- OK to call isUnliftedType: scrutinees always have a fixed RuntimeRep (see FRRCase)
+  | isUnliftedType (exprType scrut)
+    -- We can call isUnliftedType here: scrutinees always have a fixed RuntimeRep (see FRRCase).
+    -- Note however that we must check 'scrut' (which is an 'OutExpr') and not 'case_bndr'
+    -- (which is an 'InId'): see Note [Dark corner with representation polymorphism].
+    -- Using `exprType` is typically cheap becuase `scrut` is typically a variable.
+    -- We could instead use mightBeUnliftedType (idType case_bndr), but that hurts
+    -- the brain more.  Consider that if this test ever turns out to be a perf
+    -- problem (which seems unlikely).
   = exprOkForSpeculation scrut
 
   | otherwise  -- Scrut has a lifted type
diff --git a/compiler/GHC/Core/Type.hs b/compiler/GHC/Core/Type.hs
index 419c0c8806..7029125768 100644
--- a/compiler/GHC/Core/Type.hs
+++ b/compiler/GHC/Core/Type.hs
@@ -2153,14 +2153,14 @@ splitPiTys ty = split ty ty []
 --   newtype N a = MkN (a -> N a)
 --   getRuntimeArgTys (N a) == repeat (a, VisArg)
 -- @
-getRuntimeArgTys :: Type -> [(Type, AnonArgFlag)]
+getRuntimeArgTys :: Type -> [(Scaled Type, AnonArgFlag)]
 getRuntimeArgTys = go
   where
-    go :: Type -> [(Type, AnonArgFlag)]
+    go :: Type -> [(Scaled Type, AnonArgFlag)]
     go (ForAllTy _ res)
       = go res
-    go (FunTy { ft_arg = arg, ft_res = res, ft_af = af })
-      = (arg, af) : go res
+    go (FunTy { ft_mult = w, ft_arg = arg, ft_res = res, ft_af = af })
+      = (Scaled w arg, af) : go res
     go ty
       | Just ty' <- coreView ty
       = go ty'
diff --git a/compiler/GHC/HsToCore/Expr.hs b/compiler/GHC/HsToCore/Expr.hs
index 5feee52901..834be5907d 100644
--- a/compiler/GHC/HsToCore/Expr.hs
+++ b/compiler/GHC/HsToCore/Expr.hs
@@ -773,23 +773,21 @@ dsHsConLike (PatSynCon ps)
   | otherwise
   = pprPanic "dsConLike" (ppr ps)
 
-dsConLike :: ConLike -> [TcTyVar] -> [Scaled Type] -> DsM CoreExpr
--- This function desugars ConLikeTc
+-- | This function desugars 'ConLikeTc': it eta-expands
+-- data constructors to make linear types work.
+--
 -- See Note [Typechecking data constructors] in GHC.Tc.Gen.Head
---     for what is going on here
+dsConLike :: ConLike -> [TcTyVar] -> [Scaled Type] -> DsM CoreExpr
 dsConLike con tvs tys
   = do { ds_con <- dsHsConLike con
        ; ids    <- newSysLocalsDs tys
-                   -- newSysLocalDs: /can/ be lev-poly; see
+           -- NB: these 'Id's may be representation-polymorphic;
+           -- see Wrinkle [Representation-polymorphic lambda] in
+           -- Note [Typechecking data constructors] in GHC.Tc.Gen.Head.
        ; return (mkLams tvs $
                  mkLams ids $
                  ds_con `mkTyApps` mkTyVarTys tvs
-                        `mkVarApps` drop_stupid ids) }
-  where
-
-    drop_stupid = dropList (conLikeStupidTheta con)
-    -- drop_stupid: see Note [Instantiating stupid theta]
-    --              in GHC.Tc.Gen.Head
+                        `mkVarApps` ids) }
 
 {-
 ************************************************************************
diff --git a/compiler/GHC/Tc/Gen/App.hs b/compiler/GHC/Tc/Gen/App.hs
index 8f59daf24a..ecb79b8248 100644
--- a/compiler/GHC/Tc/Gen/App.hs
+++ b/compiler/GHC/Tc/Gen/App.hs
@@ -2,7 +2,6 @@
 {-# LANGUAGE DataKinds           #-}
 {-# LANGUAGE FlexibleContexts    #-}
 {-# LANGUAGE GADTs               #-}
-{-# LANGUAGE LambdaCase          #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeFamilies        #-}
 {-# LANGUAGE UndecidableInstances #-} -- Wrinkle in Note [Trees That Grow]
@@ -22,21 +21,14 @@ module GHC.Tc.Gen.App
 
 import {-# SOURCE #-} GHC.Tc.Gen.Expr( tcPolyExpr )
 
-import GHC.Types.Basic ( Arity, ExprOrPat(Expression) )
-import GHC.Types.Id ( idArity, idName, hasNoBinding )
-import GHC.Types.Name ( isWiredInName )
 import GHC.Types.Var
 import GHC.Builtin.Types ( multiplicityTy )
-import GHC.Core.ConLike  ( ConLike(..) )
-import GHC.Core.DataCon ( dataConRepArity
-                        , isNewDataCon, isUnboxedSumDataCon, isUnboxedTupleDataCon )
 import GHC.Tc.Gen.Head
 import GHC.Hs
 import GHC.Tc.Errors.Types
 import GHC.Tc.Utils.Monad
 import GHC.Tc.Utils.Unify
 import GHC.Tc.Utils.Instantiate
-import GHC.Tc.Utils.Concrete ( hasFixedRuntimeRep_syntactic )
 import GHC.Tc.Instance.Family ( tcGetFamInstEnvs, tcLookupDataFamInst_maybe )
 import GHC.Tc.Gen.HsType
 import GHC.Tc.Utils.TcMType
@@ -331,28 +323,16 @@ tcApp :: HsExpr GhcRn -> ExpRhoType -> TcM (HsExpr GhcTc)
 -- See Note [tcApp: typechecking applications]
 tcApp rn_expr exp_res_ty
   | (fun@(rn_fun, fun_ctxt), rn_args) <- splitHsApps rn_expr
-  = do { (tc_fun, fun_sigma) <- tcInferAppHead fun rn_args
+  = do { traceTc "tcApp {" $
+           vcat [ text "rn_fun:" <+> ppr rn_fun
+                , text "rn_args:" <+> ppr rn_args ]
+
+       ; (tc_fun, fun_sigma) <- tcInferAppHead fun rn_args
 
        -- Instantiate
        ; do_ql <- wantQuickLook rn_fun
        ; (delta, inst_args, app_res_rho) <- tcInstFun do_ql True fun fun_sigma rn_args
 
-       -- Check for representation polymorphism in the case that
-       -- the head of the application is a primop or data constructor
-       -- which has argument types that are representation-polymorphic.
-       -- This amounts to checking that the leftover argument types,
-       -- up until the arity, are not representation-polymorphic,
-       -- so that we can perform eta-expansion later without introducing
-       -- representation-polymorphic binders.
-       --
-       -- See Note [Checking for representation-polymorphic built-ins]
-       ; traceTc "tcApp FRR" $
-           vcat
-             [ text "tc_fun =" <+> ppr tc_fun
-             , text "inst_args =" <+> ppr inst_args
-             , text "app_res_rho =" <+> ppr app_res_rho ]
-       ; hasFixedRuntimeRep_remainingValArgs inst_args app_res_rho tc_fun
-
        -- Quick look at result
        ; app_res_rho <- if do_ql
                         then quickLookResultType delta app_res_rho exp_res_ty
@@ -375,239 +355,33 @@ tcApp rn_expr exp_res_ty
        ; res_co <- perhaps_add_res_ty_ctxt $
                    unifyExpectedType rn_expr app_res_rho exp_res_ty
 
-       ; whenDOptM Opt_D_dump_tc_trace $
-         do { inst_args <- mapM zonkArg inst_args  -- Only when tracing
-            ; traceTc "tcApp" (vcat [ text "rn_fun"       <+> ppr rn_fun
-                               , text "inst_args"    <+> brackets (pprWithCommas pprHsExprArgTc inst_args)
-                               , text "do_ql:  "     <+> ppr do_ql
-                               , text "fun_sigma:  " <+> ppr fun_sigma
-                               , text "delta:      " <+> ppr delta
-                               , text "app_res_rho:" <+> ppr app_res_rho
-                               , text "exp_res_ty:"  <+> ppr exp_res_ty
-                               , text "rn_expr:"     <+> ppr rn_expr ]) }
-
        -- Typecheck the value arguments
        ; tc_args <- tcValArgs do_ql inst_args
 
-       -- Reconstruct, with a special cases for tagToEnum#.
+       -- Reconstruct, with a special case for tagToEnum#.
        ; tc_expr <-
           if isTagToEnum rn_fun
           then tcTagToEnum tc_fun fun_ctxt tc_args app_res_rho
-          else do return (rebuildHsApps tc_fun fun_ctxt tc_args)
+          else do rebuildHsApps tc_fun fun_ctxt tc_args app_res_rho
+
+       ; whenDOptM Opt_D_dump_tc_trace $
+         do { inst_args <- mapM zonkArg inst_args  -- Only when tracing
+            ; traceTc "tcApp }" (vcat [ text "rn_fun:"      <+> ppr rn_fun
+                                      , text "rn_args:"     <+> ppr rn_args
+                                      , text "inst_args"    <+> brackets (pprWithCommas pprHsExprArgTc inst_args)
+                                      , text "do_ql:  "     <+> ppr do_ql
+                                      , text "fun_sigma:  " <+> ppr fun_sigma
+                                      , text "delta:      " <+> ppr delta
+                                      , text "app_res_rho:" <+> ppr app_res_rho
+                                      , text "exp_res_ty:"  <+> ppr exp_res_ty
+                                      , text "rn_expr:"     <+> ppr rn_expr
+                                      , text "tc_fun:"      <+> ppr tc_fun
+                                      , text "tc_args:"     <+> ppr tc_args
+                                      , text "tc_expr:"     <+> ppr tc_expr ]) }
 
        -- Wrap the result
        ; return (mkHsWrapCo res_co tc_expr) }
 
-{-
-Note [Checking for representation-polymorphic built-ins]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-We cannot have representation-polymorphic or levity-polymorphic
-function arguments. See Note [Representation polymorphism invariants]
-in GHC.Core.  That is checked by the calls to `hasFixedRuntimeRep` in
-`tcEValArg`.
-
-But some /built-in/ functions have representation-polymorphic argument
-types. Users can't define such Ids; they are all GHC built-ins or data
-constructors.  Specifically they are:
-
-1. A few wired-in Ids like unsafeCoerce#, with compulsory unfoldings.
-2. Primops, such as raise#.
-3. Newtype constructors with `UnliftedNewtypes` that have
-   a representation-polymorphic argument.
-4. Representation-polymorphic data constructors: unboxed tuples
-   and unboxed sums.
-
-For (1) consider
-  badId :: forall r (a :: TYPE r). a -> a
-  badId = unsafeCoerce# @r @r @a @a
-
-The wired-in function
-  unsafeCoerce# :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep)
-                   (a :: TYPE r1) (b :: TYPE r2).
-                   a -> b
-has a convenient but representation-polymorphic type. It has no
-binding; instead it has a compulsory unfolding, after which we
-would have
-  badId = /\r /\(a :: TYPE r). \(x::a). ...body of unsafeCorece#...
-And this is no good because of that rep-poly \(x::a).  So we want
-to reject this.
-
-On the other hand
-  goodId :: forall (a :: Type). a -> a
-  goodId = unsafeCoerce# @LiftedRep @LiftedRep @a @a
-
-is absolutely fine, because after we inline the unfolding, the \(x::a)
-is representation-monomorphic.
-
-Test cases: T14561, RepPolyWrappedVar2.
-
-For primops (2) the situation is similar; they are eta-expanded in
-CorePrep to be saturated, and that eta-expansion must not add a
-representation-polymorphic lambda.
-
-Test cases: T14561b, RepPolyWrappedVar, UnliftedNewtypesCoerceFail.
-
-For (3), consider a representation-polymorphic newtype with
-UnliftedNewtypes:
-
-  type Id :: forall r. TYPE r -> TYPE r
-  newtype Id a where { MkId :: a }
-
-  bad :: forall r (a :: TYPE r). a -> Id a
-  bad = MkId @r @a             -- Want to reject
-
-  good :: forall (a :: Type). a -> Id a
-  good = MkId @LiftedRep @a   -- Want to accept
-
-Test cases: T18481, UnliftedNewtypesLevityBinder
-
-So these three cases need special treatment. We add a special case
-in tcApp to check whether an application of an Id has any remaining
-representation-polymorphic arguments, after instantiation and application
-of previous arguments.  This is achieved by the hasFixedRuntimeRep_remainingValArgs
-function, which computes the types of the remaining value arguments, and checks
-that each of these have a fixed runtime representation using hasFixedRuntimeRep.
-
-Wrinkles
-
-* Because of Note [Typechecking data constructors] in GHC.Tc.Gen.Head,
-  we desugar a representation-polymorphic data constructor application
-  like this:
-     (/\(r :: RuntimeRep) (a :: TYPE r) \(x::a). K r a x) @LiftedRep Int 4
-  That is, a rep-poly lambda applied to arguments that instantiate it in
-  a rep-mono way.  It's a bit like a compulsory unfolding that has been
-  inlined, but not yet beta-reduced.
-
-  Because we want to accept this, we switch off Lint's representation
-  polymorphism checks when Lint checks the output of the desugarer;
-  see the lf_check_fixed_rep flag in GHC.Core.Lint.lintCoreBindings.
-
-  We then rely on the simple optimiser to beta reduce these
-  representation-polymorphic lambdas (e.g. GHC.Core.SimpleOpt.simple_app).
-
-* Arity.  We don't want to check for arguments past the
-  arity of the function.  For example
-
-      raise# :: forall {r :: RuntimeRep} (a :: Type) (b :: TYPE r). a -> b
-
-  has arity 1, so an instantiation such as:
-
-      foo :: forall w r (z :: TYPE r). w -> z -> z
-      foo = raise# @w @(z -> z)
-
-  is unproblematic.  This means we must take care not to perform a
-  representation-polymorphism check on `z`.
-
-  To achieve this, we consult the arity of the 'Id' which is the head
-  of the application (or just use 1 for a newtype constructor),
-  and keep track of how many value-level arguments we have seen,
-  to ensure we stop checking once we reach the arity.
-  This is slightly complicated by the need to include both visible
-  and invisible arguments, as the arity counts both:
-  see GHC.Tc.Gen.Head.countVisAndInvisValArgs.
-
-  Test cases: T20330{a,b}
-
--}
-
--- | Check for representation-polymorphism in the remaining argument types
--- of a variable or data constructor, after it has been instantiated and applied to some arguments.
---
--- See Note [Checking for representation-polymorphic built-ins]
-hasFixedRuntimeRep_remainingValArgs :: [HsExprArg 'TcpInst] -> TcRhoType -> HsExpr GhcTc -> TcM ()
-hasFixedRuntimeRep_remainingValArgs applied_args app_res_rho = \case
-
-  HsVar _ (L _ fun_id)
-
-    -- (1): unsafeCoerce#
-    -- 'unsafeCoerce#' is peculiar: it is patched in manually as per
-    -- Note [Wiring in unsafeCoerce#] in GHC.HsToCore.
-    -- Unfortunately, even though its arity is set to 1 in GHC.HsToCore.mkUnsafeCoercePrimPair,
-    -- at this stage, if we query idArity, we get 0. This is because
-    -- we end up looking at the non-patched version of unsafeCoerce#
-    -- defined in Unsafe.Coerce, and that one indeed has arity 0.
-    --
-    -- We thus manually specify the correct arity of 1 here.
-    | idName fun_id == unsafeCoercePrimName
-    -> check_thing fun_id 1 (FRRNoBindingResArg fun_id)
-
-    -- (2): primops and other wired-in representation-polymorphic functions,
-    -- such as 'rightSection', 'oneShot', etc; see bindings with Compulsory unfoldings
-    -- in GHC.Types.Id.Make
-    | isWiredInName (idName fun_id) && hasNoBinding fun_id
-    -> check_thing fun_id (idArity fun_id) (FRRNoBindingResArg fun_id)
-       -- NB: idArity consults the IdInfo of the Id. This can be a problem
-       -- in the presence of hs-boot files, as we might not have finished
-       -- typechecking; inspecting the IdInfo at this point can cause
-       -- strange Core Lint errors (see #20447).
-       -- We avoid this entirely by only checking wired-in names,
-       -- as those are the only ones this check is applicable to anyway.
-
-
-  XExpr (ConLikeTc (RealDataCon con) _ _)
-  -- (3): Representation-polymorphic newtype constructors.
-    | isNewDataCon con
-  -- (4): Unboxed tuples and unboxed sums
-    || isUnboxedTupleDataCon con
-    || isUnboxedSumDataCon con
-    -> check_thing con (dataConRepArity con) (FRRDataConArg Expression con)
-
-  _ -> return ()
-
-  where
-    nb_applied_vis_val_args :: Int
-    nb_applied_vis_val_args = count isHsValArg applied_args
-
-    nb_applied_val_args :: Int
-    nb_applied_val_args = countVisAndInvisValArgs applied_args
-
-    arg_tys :: [(Type,AnonArgFlag)]
-    arg_tys = getRuntimeArgTys app_res_rho
-    -- We do not need to zonk app_res_rho first, because the number of arrows
-    -- in the (possibly instantiated) inferred type of the function will
-    -- be at least the arity of the function.
-
-    check_thing :: Outputable thing
-                => thing
-                -> Arity
-                -> (Int -> FixedRuntimeRepContext)
-                -> TcM ()
-    check_thing thing arity mk_frr_orig = do
-      traceTc "tcApp remainingValArgs check_thing" (debug_msg thing arity)
-      go (nb_applied_vis_val_args + 1) (nb_applied_val_args + 1) arg_tys
-      where
-        go :: Int -- visible value argument index, starting from 1
-                  -- only used to report the argument position in error messages
-           -> Int -- value argument index, starting from 1
-                  -- used to count up to the arity to ensure we don't check too many argument types
-           -> [(Type, AnonArgFlag)] -- run-time argument types
-           -> TcM ()
-        go _ i_val _
-          | i_val > arity
-          = return ()
-        go _ _ []
-          -- Should never happen: it would mean that the arity is higher
-          -- than the number of arguments apparent from the type
-          = pprPanic "hasFixedRuntimeRep_remainingValArgs" (debug_msg thing arity)
-        go i_visval !i_val ((arg_ty, af) : tys)
-          = case af of
-              InvisArg ->
-                go i_visval (i_val + 1) tys
-              VisArg   -> do
-                hasFixedRuntimeRep_syntactic (mk_frr_orig i_visval) arg_ty
-                go (i_visval + 1) (i_val + 1) tys
-
-    -- A message containing all the relevant info, in case this functions
-    -- needs to be debugged again at some point.
-    debug_msg :: Outputable thing => thing -> Arity -> SDoc
-    debug_msg thing arity =
-      vcat
-        [ text "thing =" <+> ppr thing
-        , text "arity =" <+> ppr arity
-        , text "applied_args =" <+> ppr applied_args
-        , text "nb_applied_val_args =" <+> ppr nb_applied_val_args
-        , text "arg_tys =" <+> ppr arg_tys ]
-
 --------------------
 wantQuickLook :: HsExpr GhcRn -> TcM Bool
 -- GHC switches on impredicativity all the time for ($)
@@ -645,6 +419,7 @@ zonkArg arg = return arg
 
 
 ----------------
+
 tcValArgs :: Bool                    -- Quick-look on?
           -> [HsExprArg 'TcpInst]    -- Actual argument
           -> TcM [HsExprArg 'TcpTc]  -- Resulting argument
@@ -694,9 +469,13 @@ tcEValArg ctxt (ValArgQL { va_expr = larg@(L arg_loc _)
   = addArgCtxt ctxt larg $
     do { traceTc "tcEValArgQL {" (vcat [ ppr inner_fun <+> ppr inner_args ])
        ; tc_args <- tcValArgs True inner_args
-       ; co      <- unifyType Nothing app_res_rho exp_arg_sigma
-       ; let arg' = mkHsWrapCo co $ rebuildHsApps inner_fun fun_ctxt tc_args
-       ; traceTc "tcEValArgQL }" empty
+
+       ; co   <- unifyType Nothing app_res_rho exp_arg_sigma
+       ; arg' <- mkHsWrapCo co <$> rebuildHsApps inner_fun fun_ctxt tc_args app_res_rho
+       ; traceTc "tcEValArgQL }" $
+           vcat [ text "inner_fun:" <+> ppr inner_fun
+                , text "app_res_rho:" <+> ppr app_res_rho
+                , text "exp_arg_sigma:" <+> ppr exp_arg_sigma ]
        ; return (L arg_loc arg') }
 
 {- *********************************************************************
@@ -1418,15 +1197,15 @@ tcTagToEnum tc_fun fun_ctxt tc_args res_ty
          check_enumeration res_ty rep_tc
        ; let rep_ty  = mkTyConApp rep_tc rep_args
              tc_fun' = mkHsWrap (WpTyApp rep_ty) tc_fun
-             tc_expr = rebuildHsApps tc_fun' fun_ctxt [val_arg]
              df_wrap = mkWpCastR (mkTcSymCo coi)
+       ; tc_expr <- rebuildHsApps tc_fun' fun_ctxt [val_arg] res_ty
        ; return (mkHsWrap df_wrap tc_expr) }}}}}
 
   | otherwise
   = failWithTc TcRnTagToEnumMissingValArg
 
   where
-    vanilla_result = return (rebuildHsApps tc_fun fun_ctxt tc_args)
+    vanilla_result = rebuildHsApps tc_fun fun_ctxt tc_args res_ty
 
     check_enumeration ty' tc
       | isEnumerationTyCon tc = return ()
diff --git a/compiler/GHC/Tc/Gen/Head.hs b/compiler/GHC/Tc/Gen/Head.hs
index f663aab407..af4575c490 100644
--- a/compiler/GHC/Tc/Gen/Head.hs
+++ b/compiler/GHC/Tc/Gen/Head.hs
@@ -43,6 +43,7 @@ import GHC.Tc.Utils.Monad
 import GHC.Tc.Utils.Unify
 import GHC.Types.Basic
 import GHC.Types.Error
+import GHC.Tc.Utils.Concrete ( hasFixedRuntimeRep_syntactic )
 import GHC.Tc.Utils.Instantiate
 import GHC.Tc.Instance.Family ( tcLookupDataFamInst )
 import GHC.Core.FamInstEnv    ( FamInstEnvs )
@@ -321,25 +322,316 @@ splitHsApps e = go e (top_ctxt 0 e) []
     dec l (VACall f n _)        = VACall f (n-1) (locA l)
     dec _ ctxt@(VAExpansion {}) = ctxt
 
-rebuildHsApps :: HsExpr GhcTc -> AppCtxt -> [HsExprArg 'TcpTc]-> HsExpr GhcTc
-rebuildHsApps fun _ [] = fun
-rebuildHsApps fun ctxt (arg : args)
+-- | Rebuild an application: takes a type-checked application head
+-- expression together with arguments in the form of typechecked 'HsExprArg's
+-- and returns a typechecked application of the head to the arguments.
+--
+-- This performs a representation-polymorphism check to ensure that the
+-- remaining value arguments in an application have a fixed RuntimeRep.
+--
+-- See Note [Checking for representation-polymorphic built-ins].
+rebuildHsApps :: HsExpr GhcTc
+                      -- ^ the function being applied
+              -> AppCtxt
+              -> [HsExprArg 'TcpTc]
+                      -- ^ the arguments to the function
+              -> TcRhoType
+                      -- ^ result type of the application
+              -> TcM (HsExpr GhcTc)
+rebuildHsApps fun ctxt args app_res_rho
+  = do { tcRemainingValArgs args app_res_rho fun
+       ; return $ rebuild_hs_apps fun ctxt args }
+
+-- | The worker function for 'rebuildHsApps': simply rebuilds
+-- an application chain in which arguments are specified as
+-- typechecked 'HsExprArg's.
+rebuild_hs_apps :: HsExpr GhcTc
+                      -- ^ the function being applied
+              -> AppCtxt
+              -> [HsExprArg 'TcpTc]
+                      -- ^ the arguments to the function
+              -> HsExpr GhcTc
+rebuild_hs_apps fun _ [] = fun
+rebuild_hs_apps fun ctxt (arg : args)
   = case arg of
       EValArg { eva_arg = ValArg arg, eva_ctxt = ctxt' }
-        -> rebuildHsApps (HsApp noAnn lfun arg) ctxt' args
-      ETypeArg { eva_hs_ty = hs_ty, eva_ty  = ty, eva_ctxt = ctxt' }
-        -> rebuildHsApps (HsAppType ty lfun hs_ty) ctxt' args
+        -> rebuild_hs_apps (HsApp noAnn lfun arg) ctxt' args
+      ETypeArg { eva_hs_ty = hs_ty, eva_ty = ty, eva_ctxt = ctxt' }
+        -> rebuild_hs_apps (HsAppType ty lfun hs_ty) ctxt' args
       EPrag ctxt' p
-        -> rebuildHsApps (HsPragE noExtField p lfun) ctxt' args
+        -> rebuild_hs_apps (HsPragE noExtField p lfun) ctxt' args
       EWrap (EPar ctxt')
-        -> rebuildHsApps (gHsPar lfun) ctxt' args
+        -> rebuild_hs_apps (gHsPar lfun) ctxt' args
       EWrap (EExpand orig)
-        -> rebuildHsApps (XExpr (ExpansionExpr (HsExpanded orig fun))) ctxt args
+        -> rebuild_hs_apps (XExpr (ExpansionExpr (HsExpanded orig fun))) ctxt args
       EWrap (EHsWrap wrap)
-        -> rebuildHsApps (mkHsWrap wrap fun) ctxt args
+        -> rebuild_hs_apps (mkHsWrap wrap fun) ctxt args
   where
     lfun = L (noAnnSrcSpan $ appCtxtLoc ctxt) fun
 
+{- Note [Checking for representation-polymorphic built-ins]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We cannot have representation-polymorphic or levity-polymorphic
+function arguments. See Note [Representation polymorphism invariants]
+in GHC.Core.  That is checked by the calls to `hasFixedRuntimeRep` in
+`tcEValArg`.
+
+But some /built-in/ functions have representation-polymorphic argument
+types. Users can't define such Ids; they are all GHC built-ins or data
+constructors.  Specifically they are:
+
+1. A few wired-in Ids such as coerce and unsafeCoerce#,
+2. Primops, such as raise#.
+3. Newtype constructors with `UnliftedNewtypes` which have
+   a representation-polymorphic argument.
+4. Representation-polymorphic data constructors: unboxed tuples
+   and unboxed sums.
+
+For (1) consider
+  badId :: forall r (a :: TYPE r). a -> a
+  badId = unsafeCoerce# @r @r @a @a
+
+The wired-in function
+  unsafeCoerce# :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep)
+                   (a :: TYPE r1) (b :: TYPE r2).
+                   a -> b
+has a convenient but representation-polymorphic type. It has no
+binding; instead it has a compulsory unfolding, after which we
+would have
+  badId = /\r /\(a :: TYPE r). \(x::a). ...body of unsafeCorece#...
+And this is no good because of that rep-poly \(x::a).  So we want
+to reject this.
+
+On the other hand
+  goodId :: forall (a :: Type). a -> a
+  goodId = unsafeCoerce# @LiftedRep @LiftedRep @a @a
+
+is absolutely fine, because after we inline the unfolding, the \(x::a)
+is representation-monomorphic.
+
+Test cases: T14561, RepPolyWrappedVar2.
+
+For primops (2) the situation is similar; they are eta-expanded in
+CorePrep to be saturated, and that eta-expansion must not add a
+representation-polymorphic lambda.
+
+Test cases: T14561b, RepPolyWrappedVar, UnliftedNewtypesCoerceFail.
+
+For (3), consider a representation-polymorphic newtype with
+UnliftedNewtypes:
+
+  type Id :: forall r. TYPE r -> TYPE r
+  newtype Id a where { MkId :: a }
+
+  bad :: forall r (a :: TYPE r). a -> Id a
+  bad = MkId @r @a             -- Want to reject
+
+  good :: forall (a :: Type). a -> Id a
+  good = MkId @LiftedRep @a   -- Want to accept
+
+Test cases: T18481, UnliftedNewtypesLevityBinder
+
+So these cases need special treatment. We add a special case
+in tcApp to check whether an application of an Id has any remaining
+representation-polymorphic arguments, after instantiation and application
+of previous arguments.  This is achieved by the tcRemainingValArgs
+function, which computes the types of the remaining value arguments, and checks
+that each of these have a fixed runtime representation.
+
+Note that this function also ensures that data constructors always
+appear saturated, by performing eta-expansion if necessary.
+See Note [Typechecking data constructors].
+
+Wrinkle [Arity]
+
+  We don't want to check for arguments past the arity of the function.
+
+  For example
+
+      raise# :: forall {r :: RuntimeRep} (a :: Type) (b :: TYPE r). a -> b
+
+  has arity 1, so an instantiation such as:
+
+      foo :: forall w r (z :: TYPE r). w -> z -> z
+      foo = raise# @w @(z -> z)
+
+  is unproblematic.  This means we must take care not to perform a
+  representation-polymorphism check on `z`.
+
+  To achieve this, we consult the arity of the 'Id' which is the head
+  of the application (or just use 1 for a newtype constructor),
+  and keep track of how many value-level arguments we have seen,
+  to ensure we stop checking once we reach the arity.
+  This is slightly complicated by the need to include both visible
+  and invisible arguments, as the arity counts both:
+  see GHC.Tc.Gen.Head.countVisAndInvisValArgs.
+
+  Test cases: T20330{a,b}
+
+Wrinkle [Syntactic check]
+
+  We only perform a syntactic check in tcRemainingValArgs. That is,
+  we will reject partial applications such as:
+
+    type RR :: RuntimeREp
+    type family RR where { RR = IntRep }
+    type T :: TYPE RR
+    type family T where { T = Int# }
+
+    (# , #) @LiftedRep @RR e1
+
+  Why do we reject? Wee would need to elaborate this partial application
+  of (# , #) as follows:
+
+    let x1 = e1
+    in
+      ( \ @(ty2 :: TYPE RR) (x2 :: ty2 |> TYPE RR[0])
+      -> ( ( (# , #) @LiftedRep @RR @Char @ty2 x1 ) |> co1 )
+           x2
+      ) |> co2
+
+  That is, we need to cast the partial application
+
+    (# , #) @LiftedRep @RR @Char @ty2 x1
+
+  so that the next argument we provide to it has a fixed RuntimeRep,
+  and then eta-expand it. This is quite tricky, and other parts
+  of the compiler aren't set up to handle this mix of applications
+  and casts (e.g. checkCanEtaExpand in GHC.Core.Lint).
+
+  So we refrain from doing so, and instead limit ourselves to a simple syntactic
+  check. See the wiki page https://gitlab.haskell.org/ghc/ghc/-/wikis/Remaining-ValArgs
+  for a more in-depth discussion.
+-}
+
+-- | Typecheck the remaining value arguments in a partial application,
+-- ensuring they have a fixed RuntimeRep in the sense of Note [Fixed RuntimeRep]
+-- in GHC.Tc.Utils.Concrete.
+--
+-- Example:
+--
+-- > repPolyId :: forall r (a :: TYPE r). a -> a
+-- > repPolyId = coerce
+--
+-- This is an invalid instantiation of 'coerce', as we can't eta expand it
+-- to
+--
+-- > \@r \@(a :: TYPE r) (x :: a) -> coerce @r @a @a x
+--
+-- because the binder `x` does not have a fixed runtime representation.
+tcRemainingValArgs :: HasDebugCallStack
+                   => [HsExprArg 'TcpTc]
+                   -> TcRhoType
+                   -> HsExpr GhcTc
+                   -> TcM ()
+tcRemainingValArgs applied_args app_res_rho fun = case fun of
+
+  HsVar _ (L _ fun_id)
+
+    -- (1): unsafeCoerce#
+    -- 'unsafeCoerce#' is peculiar: it is patched in manually as per
+    -- Note [Wiring in unsafeCoerce#] in GHC.HsToCore.
+    -- Unfortunately, even though its arity is set to 1 in GHC.HsToCore.mkUnsafeCoercePrimPair,
+    -- at this stage, if we query idArity, we get 0. This is because
+    -- we end up looking at the non-patched version of unsafeCoerce#
+    -- defined in Unsafe.Coerce, and that one indeed has arity 0.
+    --
+    -- We thus manually specify the correct arity of 1 here.
+    | idName fun_id == unsafeCoercePrimName
+    -> tc_remaining_args 1 (RepPolyWiredIn fun_id)
+
+    -- (2): primops and other wired-in representation-polymorphic functions,
+    -- such as 'rightSection', 'oneShot', etc; see bindings with Compulsory unfoldings
+    -- in GHC.Types.Id.Make
+    | isWiredInName (idName fun_id) && hasNoBinding fun_id
+    -> tc_remaining_args (idArity fun_id) (RepPolyWiredIn fun_id)
+       -- NB: idArity consults the IdInfo of the Id. This can be a problem
+       -- in the presence of hs-boot files, as we might not have finished
+       -- typechecking; inspecting the IdInfo at this point can cause
+       -- strange Core Lint errors (see #20447).
+       -- We avoid this entirely by only checking wired-in names,
+       -- as those are the only ones this check is applicable to anyway.
+
+  XExpr (ConLikeTc (RealDataCon con) _ _)
+    -- (3): Representation-polymorphic newtype constructors.
+    | isNewDataCon con
+    -- (4): Unboxed tuples and unboxed sums
+    || isUnboxedTupleDataCon con
+    || isUnboxedSumDataCon con
+    -> tc_remaining_args (dc_val_arity con) (RepPolyDataCon con)
+
+  _ -> return ()
+
+  where
+
+    dc_val_arity :: DataCon -> Arity
+    dc_val_arity con = count (not . isEqPrimPred) (dataConTheta con)
+                     + length (dataConStupidTheta con)
+                     + dataConSourceArity con
+      -- Count how many value-level arguments this data constructor expects:
+      --    - dictionary arguments from the context (including the stupid context),
+      --    - source value arguments.
+      -- Tests: EtaExpandDataCon, EtaExpandStupid{1,2}.
+
+    nb_applied_vis_val_args :: Int
+    nb_applied_vis_val_args = count isHsValArg applied_args
+
+    nb_applied_val_args :: Int
+    nb_applied_val_args = countVisAndInvisValArgs applied_args
+
+    tc_remaining_args :: Arity -> RepPolyFun -> TcM ()
+    tc_remaining_args arity rep_poly_fun =
+      tc_rem_args
+        (nb_applied_vis_val_args + 1)
+        (nb_applied_val_args + 1)
+        rem_arg_tys
+
+      where
+
+      rem_arg_tys :: [(Scaled Type, AnonArgFlag)]
+      rem_arg_tys = getRuntimeArgTys app_res_rho
+        -- We do not need to zonk app_res_rho first, because the number of arrows
+        -- in the (possibly instantiated) inferred type of the function will
+        -- be at least the arity of the function.
+
+      -- The following function is essentially "mapM hasFixedRuntimeRep rem_arg_tys",
+      -- but we need to keep track of indices for error messages, hence the manual recursion.
+      tc_rem_args :: Int
+                     -- visible value argument index, starting from 1
+                     -- (only used to report the argument position in error messages)
+                  -> Int
+                     -- value argument index, starting from 1
+                     -- used to count up to the arity to ensure that
+                     -- we don't check too many argument types
+                  -> [(Scaled Type, AnonArgFlag)]
+                     -- run-time argument types
+                  -> TcM ()
+      tc_rem_args _ i_val _
+        | i_val > arity
+        = return ()
+      tc_rem_args _ _ []
+        -- Should never happen: it would mean that the arity is higher
+        -- than the number of arguments apparent from the type.
+        = pprPanic "tcRemainingValArgs" debug_msg
+      tc_rem_args i_visval !i_val ((Scaled _ arg_ty, af) : tys)
+        = do { let (i_visval', arg_pos) =
+                     case af of { InvisArg -> ( i_visval    , ArgPosInvis )
+                                ; VisArg   -> ( i_visval + 1, ArgPosVis i_visval ) }
+                   frr_ctxt = FRRNoBindingResArg rep_poly_fun arg_pos
+             ; hasFixedRuntimeRep_syntactic frr_ctxt arg_ty
+                 -- Why is this a syntactic check? See Wrinkle [Syntactic check] in
+                 -- Note [Checking for representation-polymorphic built-ins].
+             ; tc_rem_args i_visval' (i_val + 1) tys }
+
+      debug_msg :: SDoc
+      debug_msg =
+        vcat
+          [ text "app_head =" <+> ppr fun
+          , text "arity =" <+> ppr arity
+          , text "applied_args =" <+> ppr applied_args
+          , text "nb_applied_val_args =" <+> ppr nb_applied_val_args ]
+
+
 isHsValArg :: HsExprArg id -> Bool
 isHsValArg (EValArg {}) = True
 isHsValArg _            = False
@@ -845,8 +1137,11 @@ tcInferDataCon con
 
        ; let full_theta  = stupid_theta ++ theta
              all_arg_tys = map unrestricted full_theta ++ scaled_arg_tys
-                -- stupid-theta must come first
+                -- We are building the type of the data con wrapper, so the
+                -- type must precisely match the construction in
+                -- GHC.Core.DataCon.dataConWrapperType.
                 -- See Note [Instantiating stupid theta]
+                -- in GHC.Core.DataCon.
 
        ; return ( XExpr (ConLikeTc (RealDataCon con) tvs all_arg_tys)
                 , mkInvisForAllTys tvbs $ mkPhiTy full_theta $
@@ -868,22 +1163,31 @@ tcInferPatSyn id_name ps
 nonBidirectionalErr :: Name -> TcRnMessage
 nonBidirectionalErr = TcRnPatSynNotBidirectional
 
-{- Note [Typechecking data constructors]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+{- Note [Adding the implicit parameter to 'assert']
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The typechecker transforms (assert e1 e2) to (assertError e1 e2).
+This isn't really the Right Thing because there's no way to "undo"
+if you want to see the original source code in the typechecker
+output.  We'll have fix this in due course, when we care more about
+being able to reconstruct the exact original program.
+
+Note [Typechecking data constructors]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 As per Note [Polymorphisation of linear fields] in
 GHC.Core.Multiplicity, linear fields of data constructors get a
 polymorphic multiplicity when the data constructor is used as a term:
 
     Just :: forall {p} a. a %p -> Maybe a
 
-So at an occurrence of a data constructor we do the following,
-mostly in tcInferDataCon:
+So at an occurrence of a data constructor we do the following:
+
+1. Typechecking, in tcInferDataCon.
 
-1. Get its type, say
-    K :: forall (r :: RuntimeRep) (a :: TYPE r). a %1 -> T r a
-   Note the %1: it is linear
+  a. Get the original type of the constructor, say
+     K :: forall (r :: RuntimeRep) (a :: TYPE r). a %1 -> T r a
+     Note the %1: it is linear
 
-2. We are going to return a ConLikeTc, thus:
+  b. We are going to return a ConLikeTc, thus:
      XExpr (ConLikeTc K [r,a] [Scaled p a])
       :: forall (r :: RuntimeRep) (a :: TYPE r). a %p -> T r a
    where 'p' is a fresh multiplicity unification variable.
@@ -893,93 +1197,71 @@ mostly in tcInferDataCon:
    the fresh multiplicity variable in the ConLikeTc; along with
    the type of the ConLikeTc. This is done by linear_to_poly.
 
-3. If the argument is not linear (perhaps explicitly declared as
+   If the argument is not linear (perhaps explicitly declared as
    non-linear by the user), don't bother with this.
 
-4. The (ConLikeTc K [r,a] [Scaled p a]) is later desugared by
-   GHC.HsToCore.Expr.dsConLike to:
+2. Desugaring, in dsConLike.
+
+  a. The (ConLikeTc K [r,a] [Scaled p a]) is desugared to
      (/\r (a :: TYPE r). \(x %p :: a). K @r @a x)
    which has the desired type given in the previous bullet.
+
    The 'p' is the multiplicity unification variable, which
    will by now have been unified to something, or defaulted in
    `GHC.Tc.Utils.Zonk.commitFlexi`. So it won't just be an
    (unbound) variable.
 
-Wrinkles
-
-* Note that the [TcType] is strictly redundant anyway; those are the
-  type variables from the dataConUserTyVarBinders of the data constructor.
-  Similarly in the [Scaled TcType] field of ConLikeTc, the types come directly
-  from the data constructor.  The only bit that /isn't/ redundant is the
-  fresh multiplicity variables!
-
-  So an alternative would be to define ConLikeTc like this:
-      | ConLikeTc [TcType]    -- Just the multiplicity variables
-  But then the desugarer would need to repeat some of the work done here.
-  So for now at least ConLikeTc records this strictly-redundant info.
-
-* The lambda expression we produce in (4) can have representation-polymorphic
-  arguments, as indeed in (/\r (a :: TYPE r). \(x %p :: a). K @r @a x),
-  we have a lambda-bound variable x :: (a :: TYPE r).
-  This goes against the representation polymorphism invariants given in
-  Note [Representation polymorphism invariants] in GHC.Core. The trick is that
-  this this lambda will always be instantiated in a way that upholds the invariants.
-  This is achieved as follows:
-
-    A. Any arguments to such lambda abstractions are guaranteed to have
-       a fixed runtime representation. This is enforced in 'tcApp' by
-       'matchActualFunTySigma'.
-
-    B. If there are fewer arguments than there are bound term variables,
-       hasFixedRuntimeRep_remainingValArgs will ensure that we are still
-       instantiating at a representation-monomorphic type, e.g.
-
-       ( /\r (a :: TYPE r). \ (x %p :: a). K @r @a x) @IntRep @Int#
-         :: Int# -> T IntRep Int#
-
-  We then rely on the simple optimiser to beta reduce the lambda.
+   So a saturated application (K e), where e::Int will desugar to
+     (/\r (a :: TYPE r). ..etc..)
+        @LiftedRep @Int e
+   and all those lambdas will beta-reduce away in the simple optimiser
+   (see Wrinkle [Representation-polymorphic lambdas] below).
 
-* See Note [Instantiating stupid theta] for an extra wrinkle
+   But for an /unsaturated/ application, such as `map (K @LiftedRep @Int) xs`,
+   beta reduction will leave (\x %Many :: Int. K x), which is the type `map`
+   expects whereas if we had just plain K, with its linear type, we'd
+   get a type mismatch. That's why we do this funky desugaring.
 
+Wrinkles
 
-Note [Adding the implicit parameter to 'assert']
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-The typechecker transforms (assert e1 e2) to (assertError e1 e2).
-This isn't really the Right Thing because there's no way to "undo"
-if you want to see the original source code in the typechecker
-output.  We'll have fix this in due course, when we care more about
-being able to reconstruct the exact original program.
-
+  [ConLikeTc arguments]
 
-Note [Instantiating stupid theta]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider a data type with a "stupid theta" (see
-Note [The stupid context] in GHC.Core.DataCon):
+    Note that the [TcType] argument to ConLikeTc is strictly redundant; those are
+    the type variables from the dataConUserTyVarBinders of the data constructor.
+    Similarly in the [Scaled TcType] field of ConLikeTc, the types come directly
+    from the data constructor.  The only bit that /isn't/ redundant is the
+    fresh multiplicity variables!
 
-  data Ord a => T a = MkT (Maybe a)
+    So an alternative would be to define ConLikeTc like this:
+        | ConLikeTc [TcType]    -- Just the multiplicity variables
+    But then the desugarer would need to repeat some of the work done here.
+    So for now at least ConLikeTc records this strictly-redundant info.
 
-We want to generate an Ord constraint for every use of MkT; but
-we also want to allow visible type application, such as
-   MkT @Int
+  [Representation-polymorphic lambdas]
 
-So we generate (ConLikeTc MkT [a] [Ord a, Maybe a]), with type
-   forall a. Ord a => Maybe a -> T a
+    The lambda expression we produce in (4) can have representation-polymorphic
+    arguments, as indeed in (/\r (a :: TYPE r). \(x %p :: a). K @r @a x),
+    we have a lambda-bound variable x :: (a :: TYPE r).
+    This goes against the representation polymorphism invariants given in
+    Note [Representation polymorphism invariants] in GHC.Core. The trick is that
+    this this lambda will always be instantiated in a way that upholds the invariants.
+    This is achieved as follows:
 
-Now visible type application will work fine. But we desugar the
-ConLikeTc to
-   /\a \(d:Ord a) (x:Maybe a). MkT x
-Notice that 'd' is dropped in this desugaring. We don't need it;
-it was only there to generate a Wanted constraint. (That is why
-it is stupid.)  To achieve this:
+      A. Any arguments to such lambda abstractions are guaranteed to have
+         a fixed runtime representation. This is enforced in 'tcApp' by
+         'matchActualFunTySigma'.
 
-* We put the stupid-thata at the front of the list of argument
-  types in ConLikeTc
+      B. If there are fewer arguments than there are bound term variables,
+         hasFixedRuntimeRep_remainingValArgs will ensure that we are still
+         instantiating at a representation-monomorphic type, e.g.
 
-* GHC.HsToCore.Expr.dsConLike generates /lambdas/ for all the
-  arguments, but drops the stupid-theta arguments when building the
-  /application/.
+         ( /\r (a :: TYPE r). \ (x %p :: a). K @r @a x) @IntRep @Int#
+           :: Int# -> T IntRep Int#
 
-Nice.
+      C. In the output of the desugarer in (4) above, we have a representation
+         polymorphic lambda, which Lint would normally reject. So for that one
+         pass, we switch off Lint's representation-polymorphism checks; see
+         the `lf_check_fixed_rep` flag in `LintFlags`.
 -}
 
 {-
diff --git a/compiler/GHC/Tc/Gen/Pat.hs b/compiler/GHC/Tc/Gen/Pat.hs
index 62deebfe78..9a0caedd11 100644
--- a/compiler/GHC/Tc/Gen/Pat.hs
+++ b/compiler/GHC/Tc/Gen/Pat.hs
@@ -930,7 +930,7 @@ tcDataConPat penv (L con_span con_name) data_con pat_ty_scaled
         ; zipWithM_
             ( \ i arg_sty ->
               hasFixedRuntimeRep_syntactic
-                (FRRDataConArg Pattern data_con i)
+                (FRRDataConPatArg data_con i)
                 (scaledThing arg_sty)
             )
             [1..]
diff --git a/compiler/GHC/Tc/Types/Origin.hs b/compiler/GHC/Tc/Types/Origin.hs
index 2d4505b67d..137ee8f02e 100644
--- a/compiler/GHC/Tc/Types/Origin.hs
+++ b/compiler/GHC/Tc/Types/Origin.hs
@@ -31,7 +31,7 @@ module GHC.Tc.Types.Origin (
   -- * FixedRuntimeRep origin
   FixedRuntimeRepOrigin(..), FixedRuntimeRepContext(..),
   pprFixedRuntimeRepContext,
-  StmtOrigin(..),
+  StmtOrigin(..), RepPolyFun(..), ArgPos(..),
 
   -- * Arrow command origin
   FRRArrowContext(..), pprFRRArrowContext,
@@ -1021,21 +1021,17 @@ data FixedRuntimeRepContext
   -- Test cases: RepPolyCase{1,2}.
   | FRRCase
 
-  -- | An instantiation of a newtype/data constructor in which
+  -- | An instantiation of a newtype/data constructor pattern in which
   -- an argument type does not have a fixed runtime representation.
   --
-  -- The argument can either be an expression or a pattern.
-  --
-  -- Test cases:
-  --  Expression: UnliftedNewtypesLevityBinder.
-  --     Pattern: T20363.
-  | FRRDataConArg !ExprOrPat !DataCon !Int
+  -- Test case: T20363.
+  | FRRDataConPatArg !DataCon !Int
 
-  -- | An instantiation of an 'Id' with no binding (e.g. `coerce`, `unsafeCoerce#`)
+  -- | An instantiation of a function with no binding (e.g. `coerce`, `unsafeCoerce#`, an unboxed tuple 'DataCon')
   -- in which one of the remaining arguments types does not have a fixed runtime representation.
   --
-  -- Test cases: RepPolyWrappedVar, T14561, UnliftedNewtypesCoerceFail.
-  | FRRNoBindingResArg !Id !Int
+  -- Test cases: RepPolyWrappedVar, T14561, UnliftedNewtypesLevityBinder, UnliftedNewtypesCoerceFail.
+  | FRRNoBindingResArg !RepPolyFun !ArgPos
 
   -- | Arguments to unboxed tuples must have fixed runtime representations.
   --
@@ -1110,21 +1106,33 @@ pprFixedRuntimeRepContext FRRPatSynArg
   = text "The pattern synonym argument pattern"
 pprFixedRuntimeRepContext FRRCase
   = text "The scrutinee of the case statement"
-pprFixedRuntimeRepContext (FRRDataConArg expr_or_pat con i)
+pprFixedRuntimeRepContext (FRRDataConPatArg con i)
   = text "The" <+> what
   where
-    arg, what :: SDoc
-    arg = case expr_or_pat of
-      Expression -> text "argument"
-      Pattern    -> text "pattern"
+    what :: SDoc
     what
       | isNewDataCon con
-      = text "newtype constructor" <+> arg
+      = text "newtype constructor pattern"
       | otherwise
-      = text "data constructor" <+> arg <+> text "in" <+> speakNth i <+> text "position"
-pprFixedRuntimeRepContext (FRRNoBindingResArg fn i)
-  = vcat [ text "Unsaturated use of a representation-polymorphic primitive function."
-         , text "The" <+> speakNth i <+> text "argument of" <+> quotes (ppr $ getName fn) ]
+      = text "data constructor pattern in" <+> speakNth i <+> text "position"
+pprFixedRuntimeRepContext (FRRNoBindingResArg fn arg_pos)
+  = vcat [ text "Unsaturated use of a representation-polymorphic" <+> what_fun <> dot
+         , what_arg <+> text "argument of" <+> quotes (ppr fn) ]
+  where
+    what_fun, what_arg :: SDoc
+    what_fun = case fn of
+      RepPolyWiredIn {} -> text "primitive function"
+      RepPolyDataCon dc -> what_con <+> text "constructor"
+        where
+          what_con :: SDoc
+          what_con
+            | isNewDataCon dc
+            = text "newtype"
+            | otherwise
+            = text "data"
+    what_arg = case arg_pos of
+      ArgPosInvis -> text "An invisible"
+      ArgPosVis i -> text "The" <+> speakNth i
 pprFixedRuntimeRepContext (FRRTupleArg i)
   = text "The tuple argument in" <+> speakNth i <+> text "position"
 pprFixedRuntimeRepContext (FRRTupleSection i)
@@ -1161,6 +1169,30 @@ instance Outputable StmtOrigin where
   ppr MonadComprehension = text "monad comprehension"
   ppr DoNotation         = quotes ( text "do" ) <+> text "statement"
 
+-- | A function with representation-polymorphic arguments,
+-- such as @coerce@ or @(#, #)@.
+--
+-- Used for reporting partial applications of representation-polymorphic
+-- functions in error messages.
+data RepPolyFun
+  = RepPolyWiredIn !Id
+    -- ^ A wired-in function with representation-polymorphic
+    -- arguments, such as 'coerce'.
+  | RepPolyDataCon !DataCon
+    -- ^ A data constructor with representation-polymorphic arguments,
+    -- such as an unboxed tuple or a newtype constructor with @-XUnliftedNewtypes@.
+
+instance Outputable RepPolyFun where
+  ppr (RepPolyWiredIn id) = ppr id
+  ppr (RepPolyDataCon dc) = ppr dc
+
+-- | The position of an argument (to be reported in an error message).
+data ArgPos
+  = ArgPosInvis
+    -- ^ Invisible argument: don't report its position to the user.
+  | ArgPosVis !Int
+    -- ^ Visible argument in i-th position.
+
 {- *********************************************************************
 *                                                                      *
                        FixedRuntimeRep: arrows
diff --git a/compiler/GHC/Types/Basic.hs b/compiler/GHC/Types/Basic.hs
index b2c2b1e103..7ef2ff6446 100644
--- a/compiler/GHC/Types/Basic.hs
+++ b/compiler/GHC/Types/Basic.hs
@@ -105,8 +105,6 @@ module GHC.Types.Basic (
 
         Levity(..), mightBeLifted, mightBeUnlifted,
 
-        ExprOrPat(..),
-
         NonStandardDefaultingStrategy(..),
         DefaultingStrategy(..), defaultNonStandardTyVars,
 
@@ -1922,25 +1920,6 @@ mightBeUnlifted _             = True
 
 {- *********************************************************************
 *                                                                      *
-                     Expressions vs Patterns
-*                                                                      *
-********************************************************************* -}
-
--- | Are we dealing with an expression or a pattern?
---
--- Used only for the textual output of certain error messages;
--- see the 'FRRDataConArg' constructor of 'FixedRuntimeRepContext'.
-data ExprOrPat
-  = Expression
-  | Pattern
-  deriving Eq
-
-instance Outputable ExprOrPat where
-  ppr Expression = text "expression"
-  ppr Pattern    = text "pattern"
-
-{- *********************************************************************
-*                                                                      *
                         Defaulting options
 *                                                                      *
 ********************************************************************* -}
diff --git a/compiler/GHC/Types/Id/Make.hs b/compiler/GHC/Types/Id/Make.hs
index 6b7f1053b9..9628bea733 100644
--- a/compiler/GHC/Types/Id/Make.hs
+++ b/compiler/GHC/Types/Id/Make.hs
@@ -679,8 +679,10 @@ mkDataConRep dc_bang_opts fam_envs wrap_name data_con
 
   | otherwise
   = do { wrap_args <- mapM (newLocal (fsLit "conrep")) wrap_arg_tys
-       ; wrap_body <- mk_rep_app (wrap_args `zip` dropList eq_spec unboxers)
+       ; wrap_body <- mk_rep_app (dropList stupid_theta wrap_args `zip` dropList eq_spec unboxers)
                                  initial_wrap_app
+                        -- Drop the stupid theta arguments, as per
+                        -- Note [Instantiating stupid theta] in GHC.Core.DataCon.
 
        ; let wrap_id = mkGlobalId (DataConWrapId data_con) wrap_name wrap_ty wrap_info
              wrap_info = noCafIdInfo
@@ -735,6 +737,7 @@ mkDataConRep dc_bang_opts fam_envs wrap_name data_con
   where
     (univ_tvs, ex_tvs, eq_spec, theta, orig_arg_tys, _orig_res_ty)
       = dataConFullSig data_con
+    stupid_theta = dataConStupidTheta data_con
     wrap_tvs     = dataConUserTyVars data_con
     res_ty_args  = substTyVars (mkTvSubstPrs (map eqSpecPair eq_spec)) univ_tvs
 
@@ -745,7 +748,7 @@ mkDataConRep dc_bang_opts fam_envs wrap_name data_con
     ev_ibangs    = map (const HsLazy) ev_tys
     orig_bangs   = dataConSrcBangs data_con
 
-    wrap_arg_tys = (map unrestricted theta) ++ orig_arg_tys
+    wrap_arg_tys = (map unrestricted $ stupid_theta ++ theta) ++ orig_arg_tys
     wrap_arity   = count isCoVar ex_tvs + length wrap_arg_tys
              -- The wrap_args are the arguments *other than* the eq_spec
              -- Because we are going to apply the eq_spec args manually in the
@@ -784,6 +787,10 @@ mkDataConRep dc_bang_opts fam_envs wrap_name data_con
                      -- worker expects, it needs a data con wrapper to reorder
                      -- the type variables.
                      -- See Note [Data con wrappers and GADT syntax].
+      || not (null stupid_theta)
+                     -- If the data constructor has a datatype context,
+                     -- we need a wrapper in order to drop the stupid arguments.
+                     -- See Note [Instantiating stupid theta] in GHC.Core.DataCon.
 
     initial_wrap_app = Var (dataConWorkId data_con)
                        `mkTyApps`  res_ty_args