[Git][ghc/ghc][wip/9.4.6-backports] Typecheck remaining ValArgs in rebuildHsApps

Zubin (@wz1000) gitlab at gitlab.haskell.org
Thu Aug 3 20:52:22 UTC 2023



Zubin pushed to branch wip/9.4.6-backports at Glasgow Haskell Compiler / GHC


Commits:
48f74650 by sheaf at 2023-08-04T02:21:55+05:30
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

(cherry picked from commit 28880828182a32bcb39ce8230965a8bc17aeb218)

- - - - -


27 changed files:

- compiler/GHC/Core/DataCon.hs
- compiler/GHC/Core/Lint.hs
- compiler/GHC/Core/Opt/Simplify.hs
- compiler/GHC/Core/Type.hs
- compiler/GHC/HsToCore/Expr.hs
- compiler/GHC/Tc/Gen/App.hs
- compiler/GHC/Tc/Gen/Head.hs
- compiler/GHC/Tc/Gen/Pat.hs
- compiler/GHC/Tc/Types/Origin.hs
- compiler/GHC/Types/Basic.hs
- compiler/GHC/Types/Id/Make.hs
- testsuite/tests/rename/should_fail/rnfail055.stderr
- testsuite/tests/rep-poly/RepPolyMagic.stderr
- testsuite/tests/rep-poly/RepPolyRightSection.stderr
- + testsuite/tests/rep-poly/RepPolyTuple2.hs
- + testsuite/tests/rep-poly/RepPolyTuple2.stderr
- + testsuite/tests/rep-poly/RepPolyUnliftedNewtype.hs
- testsuite/tests/rep-poly/T13233.stderr
- testsuite/tests/rep-poly/T14561.stderr
- testsuite/tests/rep-poly/T14561b.stderr
- testsuite/tests/rep-poly/T17817.stderr
- + testsuite/tests/rep-poly/T21544.hs
- + testsuite/tests/rep-poly/T21650_a.stderr
- + testsuite/tests/rep-poly/T21650_b.stderr
- testsuite/tests/rep-poly/UnliftedNewtypesCoerceFail.stderr
- testsuite/tests/rep-poly/UnliftedNewtypesLevityBinder.stderr
- testsuite/tests/rep-poly/all.T


Changes:

=====================================
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}
@@ -1483,9 +1509,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
 


=====================================
compiler/GHC/Core/Lint.hs
=====================================
@@ -1144,7 +1144,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


=====================================
compiler/GHC/Core/Opt/Simplify.hs
=====================================
@@ -2903,8 +2903,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


=====================================
compiler/GHC/Core/Type.hs
=====================================
@@ -2147,14 +2147,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'


=====================================
compiler/GHC/HsToCore/Expr.hs
=====================================
@@ -1031,23 +1031,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) }
 
 {-
 ************************************************************************


=====================================
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
@@ -379,239 +359,33 @@ tcApp rn_expr exp_res_ty
                      -- app_res_rho and exp_res_ty are both rho-types, so without
                      -- deep subsumption unifyExpectedType would be sufficient
 
-       ; whenDOptM Opt_D_dump_tc_trace $
-         do { inst_args <- mapM zonkArg inst_args  -- Only when tracing
-            ; 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 (mkHsWrap res_wrap 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 ($)
@@ -649,6 +423,7 @@ zonkArg arg = return arg
 
 
 ----------------
+
 tcValArgs :: Bool                    -- Quick-look on?
           -> [HsExprArg 'TcpInst]    -- Actual argument
           -> TcM [HsExprArg 'TcpTc]  -- Resulting argument
@@ -698,9 +473,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') }
 
 {- *********************************************************************
@@ -1424,15 +1203,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 ()


=====================================
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 )
@@ -287,25 +288,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
@@ -820,8 +1112,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 $
@@ -845,22 +1140,31 @@ nonBidirectionalErr name = TcRnUnknownMessage $ mkPlainError noHints $
   text "non-bidirectional pattern synonym"
   <+> quotes (ppr name) <+> text "used in an expression"
 
-{- 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.
@@ -870,93 +1174,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`.
 -}
 
 {-


=====================================
compiler/GHC/Tc/Gen/Pat.hs
=====================================
@@ -935,7 +935,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..]


=====================================
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,
@@ -1016,21 +1016,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.
   --
@@ -1102,21 +1098,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)
@@ -1153,6 +1161,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 at .
+
+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


=====================================
compiler/GHC/Types/Basic.hs
=====================================
@@ -107,8 +107,6 @@ module GHC.Types.Basic (
 
         Levity(..), mightBeLifted, mightBeUnlifted,
 
-        ExprOrPat(..),
-
         NonStandardDefaultingStrategy(..),
         DefaultingStrategy(..), defaultNonStandardTyVars,
 
@@ -1927,25 +1925,6 @@ mightBeUnlifted :: Maybe Levity -> Bool
 mightBeUnlifted (Just Lifted) = False
 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


=====================================
compiler/GHC/Types/Id/Make.hs
=====================================
@@ -684,8 +684,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
@@ -741,6 +743,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
 
@@ -751,7 +754,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
@@ -790,6 +793,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


=====================================
testsuite/tests/rename/should_fail/rnfail055.stderr
=====================================
@@ -52,6 +52,7 @@ RnFail055.hs-boot:15:1: error:
     The roles do not match.
     Roles on abstract types default to ‘representational’ in boot files.
     The datatype contexts do not match
+    The constructors do not match: The types for ‘T2’ differ
 
 RnFail055.hs-boot:17:11: error:
     ‘T3’ is exported by the hs-boot file, but not exported by the module


=====================================
testsuite/tests/rep-poly/RepPolyMagic.stderr
=====================================
@@ -4,23 +4,15 @@ RepPolyMagic.hs:12:7: error:
       The second argument of ‘seq’
       does not have a fixed runtime representation.
       Its type is:
-        b0 :: TYPE c1
-      Cannot unify ‘r’ with the type variable ‘c1’
-      because it is not a concrete ‘RuntimeRep’.
+        b :: TYPE r
     • In the expression: seq
       In an equation for ‘foo’: foo = seq
-    • Relevant bindings include
-        foo :: a -> b -> b (bound at RepPolyMagic.hs:12:1)
 
 RepPolyMagic.hs:15:7: error:
     • Unsaturated use of a representation-polymorphic primitive function.
       The second argument of ‘oneShot’
       does not have a fixed runtime representation.
       Its type is:
-        a0 :: TYPE c0
-      Cannot unify ‘r’ with the type variable ‘c0’
-      because it is not a concrete ‘RuntimeRep’.
+        a :: TYPE r
     • In the expression: oneShot
       In an equation for ‘bar’: bar = oneShot
-    • Relevant bindings include
-        bar :: (a -> a) -> a -> a (bound at RepPolyMagic.hs:15:1)


=====================================
testsuite/tests/rep-poly/RepPolyRightSection.stderr
=====================================
@@ -4,10 +4,6 @@ RepPolyRightSection.hs:14:11: error:
       The third argument of ‘rightSection’
       does not have a fixed runtime representation.
       Its type is:
-        a :: TYPE c0
-      Cannot unify ‘r’ with the type variable ‘c0’
-      because it is not a concrete ‘RuntimeRep’.
+        a :: TYPE r
     • In the expression: `g` undefined
       In an equation for ‘test2’: test2 = (`g` undefined)
-    • Relevant bindings include
-        test2 :: a -> a (bound at RepPolyRightSection.hs:14:1)


=====================================
testsuite/tests/rep-poly/RepPolyTuple2.hs
=====================================
@@ -0,0 +1,21 @@
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UnboxedTuples #-}
+
+module RepPolyTuple2 where
+
+import GHC.Exts
+
+type RR :: RuntimeRep
+type family RR where { RR = FloatRep }
+type F :: TYPE RR
+type family F where { F = Float# }
+
+{-# NOINLINE expensive #-}
+expensive :: Float -> Float
+expensive x = cos x ** 123.45
+
+tup x = (# , #) @LiftedRep @RR (expensive x)


=====================================
testsuite/tests/rep-poly/RepPolyTuple2.stderr
=====================================
@@ -0,0 +1,10 @@
+
+RepPolyTuple2.hs:21:9: error:
+    • Unsaturated use of a representation-polymorphic data constructor.
+      The second argument of ‘(#,#)’
+      does not have a fixed runtime representation.
+      Its type is:
+        b :: TYPE RR
+    • In the expression: (#,#) @LiftedRep @RR (expensive x)
+      In an equation for ‘tup’:
+          tup x = (#,#) @LiftedRep @RR (expensive x)


=====================================
testsuite/tests/rep-poly/RepPolyUnliftedNewtype.hs
=====================================
@@ -0,0 +1,55 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DatatypeContexts #-}
+{-# LANGUAGE LinearTypes #-}
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE PartialTypeSignatures #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE UnliftedNewtypes #-}
+
+module RepPolyUnliftedNewtype where
+
+import GHC.Exts
+import GHC.Types (Multiplicity(..))
+
+type C :: forall (r :: RuntimeRep). TYPE r -> Constraint
+class C a
+instance C Int#
+
+type N :: forall (r :: RuntimeRep). TYPE r -> TYPE r
+newtype C a => N a = MkN a
+
+f1, f2, f3, f4, f5, f6, f7 :: Int# %Many -> N Int#
+f1 = MkN
+f2 = MkN @_
+f3 = MkN @IntRep
+f4 = MkN @_      @_
+f5 = MkN @_      @Int#
+f6 = MkN @IntRep @_
+f7 = MkN @IntRep @Int#
+
+g1, g2, g3, g4, g5, g6, g7 :: Int# %Many -> N Int#
+g1 x = MkN               x
+g2 x = MkN @_            x
+g3 x = MkN @IntRep       x
+g4 x = MkN @_      @_    x
+g5 x = MkN @_      @Int# x
+g6 x = MkN @IntRep @_    x
+g7 x = MkN @IntRep @Int# x
+
+h3, h5, h6, h7 :: _ => _ %Many -> N _
+h3 = MkN @IntRep
+h5 = MkN @_      @Int#
+h6 = MkN @IntRep @_
+h7 = MkN @IntRep @Int#
+
+k1 (x :: Int#) = MkN               x
+k2 (x :: Int#) = MkN @_            x
+k3  x          = MkN @IntRep       x
+k4 (x :: Int#) = MkN @_      @_    x
+k5  x          = MkN @_      @Int# x
+k6  x          = MkN @IntRep @_    x
+k7  x          = MkN @IntRep @Int# x
+
+l1 = (MkN :: Int# %Many -> N Int#)


=====================================
testsuite/tests/rep-poly/T13233.stderr
=====================================
@@ -1,24 +1,30 @@
 
 T13233.hs:14:11: error:
-    • The data constructor argument in second position
-      does not have a fixed runtime representation.
-      Its type is:
-        b1 :: TYPE c3
-      Cannot unify ‘rep’ with the type variable ‘c3’
-      because it is not a concrete ‘RuntimeRep’.
+    • • Unsaturated use of a representation-polymorphic data constructor.
+        The second argument of ‘(#,#)’
+        does not have a fixed runtime representation.
+        Its type is:
+          a :: TYPE rep
+      • Unsaturated use of a representation-polymorphic data constructor.
+        The first argument of ‘(#,#)’
+        does not have a fixed runtime representation.
+        Its type is:
+          a :: TYPE rep
     • In the first argument of ‘bar’, namely ‘(#,#)’
       In the expression: bar (#,#)
       In an equation for ‘baz’: baz = bar (#,#)
-    • Relevant bindings include
-        baz :: a -> a -> (# a, a #) (bound at T13233.hs:14:1)
 
 T13233.hs:22:16: error:
-    • The data constructor argument in second position
-      does not have a fixed runtime representation.
-      Its type is:
-        b0 :: TYPE c1
-      Cannot unify ‘rep2’ with the type variable ‘c1’
-      because it is not a concrete ‘RuntimeRep’.
+    • • Unsaturated use of a representation-polymorphic data constructor.
+        The second argument of ‘(#,#)’
+        does not have a fixed runtime representation.
+        Its type is:
+          b :: TYPE rep2
+      • Unsaturated use of a representation-polymorphic data constructor.
+        The first argument of ‘(#,#)’
+        does not have a fixed runtime representation.
+        Its type is:
+          a :: TYPE rep1
     • In the first argument of ‘obscure’, namely ‘(#,#)’
       In the expression: obscure (#,#)
       In an equation for ‘quux’: quux = obscure (#,#)


=====================================
testsuite/tests/rep-poly/T14561.stderr
=====================================
@@ -4,10 +4,6 @@ T14561.hs:12:9: error:
       The first argument of ‘unsafeCoerce#’
       does not have a fixed runtime representation.
       Its type is:
-        a0 :: TYPE c0
-      Cannot unify ‘r’ with the type variable ‘c0’
-      because it is not a concrete ‘RuntimeRep’.
+        a :: TYPE r
     • In the expression: unsafeCoerce#
       In an equation for ‘badId’: badId = unsafeCoerce#
-    • Relevant bindings include
-        badId :: a -> a (bound at T14561.hs:12:1)


=====================================
testsuite/tests/rep-poly/T14561b.stderr
=====================================
@@ -4,10 +4,6 @@ T14561b.hs:12:9: error:
       The first argument of ‘coerce’
       does not have a fixed runtime representation.
       Its type is:
-        a0 :: TYPE c0
-      Cannot unify ‘r’ with the type variable ‘c0’
-      because it is not a concrete ‘RuntimeRep’.
+        a :: TYPE r
     • In the expression: coerce
       In an equation for ‘badId’: badId = coerce
-    • Relevant bindings include
-        badId :: a -> a (bound at T14561b.hs:12:1)


=====================================
testsuite/tests/rep-poly/T17817.stderr
=====================================
@@ -4,15 +4,6 @@ T17817.hs:16:10: error:
       The first argument of ‘mkWeak#’
       does not have a fixed runtime representation.
       Its type is:
-        a0 :: TYPE ('BoxedRep c0)
-      Cannot unify ‘l’ with the type variable ‘c0’
-      because it is not a concrete ‘Levity’.
+        a :: TYPE ('BoxedRep l)
     • In the expression: mkWeak#
       In an equation for ‘primop’: primop = mkWeak#
-    • Relevant bindings include
-        primop :: a
-                  -> b
-                  -> (State# RealWorld -> (# State# RealWorld, c #))
-                  -> State# RealWorld
-                  -> (# State# RealWorld, Weak# b #)
-          (bound at T17817.hs:16:1)


=====================================
testsuite/tests/rep-poly/T21544.hs
=====================================
@@ -0,0 +1,29 @@
+
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DatatypeContexts #-}
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UnliftedNewtypes #-}
+
+module T21544 where
+
+import Data.Kind
+import GHC.Exts
+
+
+type N1 :: forall (r :: RuntimeRep) -> TYPE r -> TYPE r
+data family N1 r a
+newtype instance N1 r a = MkN1 a
+
+foo1 :: Int# -> N1 IntRep Int#
+foo1 = MkN1
+
+
+type N2 :: forall (r :: RuntimeRep) -> TYPE r -> Type -> Type -> Type -> TYPE r
+data family N2 r a i
+newtype instance Ord b => N2 r a Int b c = MkN2 a
+
+foo2 :: Ord b => Int# -> N2 IntRep Int# Int b c
+foo2 = MkN2


=====================================
testsuite/tests/rep-poly/T21650_a.stderr
=====================================
@@ -0,0 +1,18 @@
+
+T21650_a.hs:25:8: error:
+    • Unsaturated use of a representation-polymorphic newtype constructor.
+      The first argument of ‘MkN’
+      does not have a fixed runtime representation.
+      Its type is:
+        F Float :: TYPE (R Float)
+    • In the expression: MkN
+      In an equation for ‘foo1’: foo1 = MkN
+
+T21650_a.hs:28:10: error:
+    • Unsaturated use of a representation-polymorphic newtype constructor.
+      The first argument of ‘MkN’
+      does not have a fixed runtime representation.
+      Its type is:
+        F Double :: TYPE (R Double)
+    • In the expression: MkN
+      In an equation for ‘foo2’: foo2 _ = MkN


=====================================
testsuite/tests/rep-poly/T21650_b.stderr
=====================================
@@ -0,0 +1,18 @@
+
+T21650_b.hs:34:7: error:
+    • Unsaturated use of a representation-polymorphic newtype constructor.
+      The first argument of ‘MkN’
+      does not have a fixed runtime representation.
+      Its type is:
+        a :: TYPE (RR T1 t2)
+    • In the expression: MkN
+      In an equation for ‘foo’: foo = MkN
+
+T21650_b.hs:37:7: error:
+    • Unsaturated use of a representation-polymorphic newtype constructor.
+      The first argument of ‘MkN’
+      does not have a fixed runtime representation.
+      Its type is:
+        a :: TYPE (RR T1 t2)
+    • In the expression: MkN
+      In an equation for ‘bar’: bar = MkN


=====================================
testsuite/tests/rep-poly/UnliftedNewtypesCoerceFail.stderr
=====================================
@@ -4,10 +4,6 @@ UnliftedNewtypesCoerceFail.hs:15:8: error:
       The first argument of ‘coerce’
       does not have a fixed runtime representation.
       Its type is:
-        a0 :: TYPE c0
-      Cannot unify ‘rep’ with the type variable ‘c0’
-      because it is not a concrete ‘RuntimeRep’.
+        x :: TYPE rep
     • In the expression: coerce
       In an equation for ‘goof’: goof = coerce
-    • Relevant bindings include
-        goof :: x -> y (bound at UnliftedNewtypesCoerceFail.hs:15:1)


=====================================
testsuite/tests/rep-poly/UnliftedNewtypesLevityBinder.stderr
=====================================
@@ -1,12 +1,9 @@
 
 UnliftedNewtypesLevityBinder.hs:16:7: error:
-    • The newtype constructor argument
+    • Unsaturated use of a representation-polymorphic newtype constructor.
+      The first argument of ‘IdentC’
       does not have a fixed runtime representation.
       Its type is:
-        a0 :: TYPE c0
-      Cannot unify ‘r’ with the type variable ‘c0’
-      because it is not a concrete ‘RuntimeRep’.
+        a :: TYPE r
     • In the expression: IdentC
       In an equation for ‘bad’: bad = IdentC
-    • Relevant bindings include
-        bad :: a -> Ident a (bound at UnliftedNewtypesLevityBinder.hs:16:1)


=====================================
testsuite/tests/rep-poly/all.T
=====================================
@@ -28,7 +28,10 @@ test('T20423', normal, compile_fail, [''])
 test('T20423b', normal, compile_fail, [''])
 test('T20426', normal, compile_fail, [''])
 test('T21239', normal, compile, [''])
+test('T21544', normal, compile, ['-Wno-deprecated-flags'])
 
+test('EtaExpandStupid1', normal, compile, ['-Wno-deprecated-flags'])
+test('EtaExpandStupid2', normal, compile_fail, ['-Wno-deprecated-flags'])
 test('LevPolyLet', normal, compile_fail, [''])
 test('PandocArrowCmd', normal, compile, [''])
 test('RepPolyApp', normal, compile_fail, [''])
@@ -77,6 +80,8 @@ test('RepPolyTupleSection', normal, compile_fail, [''])
 test('RepPolyUnboxedPatterns', normal, compile_fail, [''])
 test('RepPolyUnliftedDatatype', normal, compile, [''])
 test('RepPolyUnliftedDatatype2', normal, compile, ['-O'])
+test('RepPolyUnliftedNewtype', normal, compile,
+     ['-fno-warn-partial-type-signatures -fno-warn-deprecated-flags'])
 test('RepPolyWildcardPattern', normal, compile_fail, [''])
 test('RepPolyWrappedVar', normal, compile_fail, [''])
 test('RepPolyWrappedVar2', normal, compile, [''])
@@ -104,5 +109,5 @@ test('T20363_show_co', normal, compile_fail                         ##
 test('T20363b', normal, compile_fail, [''])                         ##
 test('RepPolyCase2', normal, compile_fail, [''])                    ##
 test('RepPolyRule3', normal, compile_fail, [''])                    ##
+test('RepPolyTuple2', normal, compile_fail, ['']) ## see #21683     ##
 ######################################################################
-test('T23153', normal, compile_fail, [''])



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/48f746502bc64d25e8eb7094ba7a26f484585279

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/48f746502bc64d25e8eb7094ba7a26f484585279
You're receiving this email because of your account on gitlab.haskell.org.


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20230803/2fedc961/attachment-0001.html>


More information about the ghc-commits mailing list