Introduce Concrete# for representation polymorphism checks

PHASE 1: we never rewrite Concrete# evidence.

This patch migrates all the representation polymorphism checks to
the typechecker, using a new constraint form

  Concrete# :: forall k. k -> TupleRep '[]

Whenever a type `ty` must be representation-polymorphic
(e.g. it is the type of an argument to a function), we emit a new
`Concrete# ty` Wanted constraint. If this constraint goes
unsolved, we report a representation-polymorphism error to the user.
The 'FRROrigin' datatype keeps track of the context of the
representation-polymorphism check, for more informative error messages.

This paves the way for further improvements, such as
allowing type families in RuntimeReps and improving the soundness
of typed Template Haskell. This is left as future work (PHASE 2).

fixes #17907 #20277 #20330 #20423 #20426

updates haddock submodule

-------------------------
Metric Decrease:
    T5642
-------------------------

9 files changed, 398 insertions, 55 deletions

diff --git a/compiler/GHC/Tc/Gen/App.hs b/compiler/GHC/Tc/Gen/App.hs
index cc0814cced..22454d1acc 100644
--- a/compiler/GHC/Tc/Gen/App.hs
+++ b/compiler/GHC/Tc/Gen/App.hs
@@ -2,6 +2,7 @@
 {-# LANGUAGE DataKinds           #-}
 {-# LANGUAGE FlexibleContexts    #-}
 {-# LANGUAGE GADTs               #-}
+{-# LANGUAGE LambdaCase          #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeFamilies        #-}
 {-# LANGUAGE UndecidableInstances #-} -- Wrinkle in Note [Trees That Grow]
@@ -21,13 +22,21 @@ module GHC.Tc.Gen.App
 
 import {-# SOURCE #-} GHC.Tc.Gen.Expr( tcPolyExpr )
 
-import GHC.Builtin.Types (multiplicityTy)
+import GHC.Types.Basic ( Arity )
+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 )
 import GHC.Tc.Instance.Family ( tcGetFamInstEnvs, tcLookupDataFamInst_maybe )
 import GHC.Tc.Gen.HsType
 import GHC.Tc.Utils.TcMType
@@ -317,6 +326,22 @@ tcApp rn_expr exp_res_ty
        ; 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
@@ -353,14 +378,221 @@ tcApp rn_expr exp_res_ty
        -- Typecheck the value arguments
        ; tc_args <- tcValArgs do_ql inst_args
 
-       -- Reconstruct, with special case for tagToEnum#
-       ; tc_expr <- if isTagToEnum rn_fun
-                    then tcTagToEnum tc_fun fun_ctxt tc_args app_res_rho
-                    else return (rebuildHsApps tc_fun fun_ctxt tc_args)
+       -- Reconstruct, with a special cases 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)
 
        -- 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 are representation-polymorphic.  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_repy flag in GHC.Core.Lint.lintCoreBindings.
+
+* 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 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 :: [TyCoBinder]
+    arg_tys = fst $ splitPiTys 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 -> FRROrigin) -> 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
+                  -- (only used to report the argument position in error messages)
+           -> Int -- ^ value argument index
+                  -- used to count up to the arity to ensure we don't check too many argument types
+           -> [TyCoBinder]
+           -> 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 (Anon af (Scaled _ arg_ty) : tys)
+          = case af of
+              InvisArg ->
+                go i_visval (i_val + 1) tys
+              VisArg   -> do
+                _concrete_ev <- hasFixedRuntimeRep (mk_frr_orig i_visval) arg_ty
+                go (i_visval + 1) (i_val + 1) tys
+        go i_visval i_val (_: tys)
+          = go i_visval i_val 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_vis_val_args =" <+> ppr nb_applied_vis_val_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 ($)
@@ -438,9 +670,10 @@ tcEValArg :: AppCtxt -> EValArg 'TcpInst -> TcSigmaType -> TcM (LHsExpr GhcTc)
 tcEValArg ctxt (ValArg larg@(L arg_loc arg)) exp_arg_sigma
   = addArgCtxt ctxt larg $
     do { arg' <- tcPolyExpr arg (mkCheckExpType exp_arg_sigma)
+       ; _concrete_ev <- hasFixedRuntimeRep (FRRApp arg) exp_arg_sigma
        ; return (L arg_loc arg') }
 
-tcEValArg ctxt (ValArgQL { va_expr = larg@(L arg_loc _)
+tcEValArg ctxt (ValArgQL { va_expr = larg@(L arg_loc arg)
                          , va_fun = (inner_fun, fun_ctxt)
                          , va_args = inner_args
                          , va_ty = app_res_rho }) exp_arg_sigma
@@ -448,6 +681,7 @@ tcEValArg ctxt (ValArgQL { va_expr = larg@(L arg_loc _)
     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
+       ; _concrete_ev <- hasFixedRuntimeRep (FRRApp arg) exp_arg_sigma
        ; traceTc "tcEValArg }" empty
        ; return (L arg_loc $ mkHsWrapCo co $
                  rebuildHsApps inner_fun fun_ctxt tc_args) }
diff --git a/compiler/GHC/Tc/Gen/Arrow.hs b/compiler/GHC/Tc/Gen/Arrow.hs
index 0d0e482b35..45e8f08a5e 100644
--- a/compiler/GHC/Tc/Gen/Arrow.hs
+++ b/compiler/GHC/Tc/Gen/Arrow.hs
@@ -22,6 +22,7 @@ import GHC.Hs.Syn.Type
 import GHC.Tc.Errors.Types
 import GHC.Tc.Gen.Match
 import GHC.Tc.Gen.Head( tcCheckId )
+import GHC.Tc.Utils.Concrete ( hasFixedRuntimeRep )
 import GHC.Tc.Utils.TcType
 import GHC.Tc.Utils.TcMType
 import GHC.Tc.Gen.Bind
@@ -91,13 +92,14 @@ tcProc :: LPat GhcRn -> LHsCmdTop GhcRn         -- proc pat -> expr
        -> ExpRhoType                            -- Expected type of whole proc expression
        -> TcM (LPat GhcTc, LHsCmdTop GhcTc, TcCoercion)
 
-tcProc pat cmd@(L _ (HsCmdTop names _)) exp_ty
+tcProc pat cmd@(L loc (HsCmdTop names _)) exp_ty
   = do  { exp_ty <- expTypeToType exp_ty  -- no higher-rank stuff with arrows
         ; (co, (exp_ty1, res_ty)) <- matchExpectedAppTy exp_ty
         ; (co1, (arr_ty, arg_ty)) <- matchExpectedAppTy exp_ty1
         -- start with the names as they are used to desugar the proc itself
         -- See #17423
-        ; names' <- mapM (tcSyntaxName ProcOrigin arr_ty) names
+        ; names' <- setSrcSpan loc $
+            mapM (tcSyntaxName ProcOrigin arr_ty) names
         ; let cmd_env = CmdEnv { cmd_arr = arr_ty }
         ; (pat', cmd') <- newArrowScope
                           $ tcCheckPat (ArrowMatchCtxt ProcExpr) pat (unrestricted arg_ty)
@@ -141,9 +143,10 @@ tcCmdTop env names (L loc (HsCmdTop _names cmd)) cmd_ty@(cmd_stk, res_ty)
 ----------------------------------------
 tcCmd  :: CmdEnv -> LHsCmd GhcRn -> CmdType -> TcM (LHsCmd GhcTc)
         -- The main recursive function
-tcCmd env (L loc cmd) res_ty
+tcCmd env (L loc cmd) cmd_ty@(_, res_ty)
   = setSrcSpan (locA loc) $ do
-        { cmd' <- tc_cmd env cmd res_ty
+        { cmd' <- tc_cmd env cmd cmd_ty
+        ; _concrete_ev <- hasFixedRuntimeRep (FRRArrow $ ArrowCmdResTy cmd) res_ty
         ; return (L loc cmd') }
 
 tc_cmd :: CmdEnv -> HsCmd GhcRn  -> CmdType -> TcM (HsCmd GhcTc)
@@ -219,6 +222,10 @@ tc_cmd env cmd@(HsCmdArrApp _ fun arg ho_app lr) (_, res_ty)
 
         ; arg' <- tcCheckMonoExpr arg arg_ty
 
+        ; _concrete_ev <- hasFixedRuntimeRep
+                        (FRRArrow $ ArrowCmdArrApp (unLoc fun) (unLoc arg) ho_app)
+                        fun_ty
+
         ; return (HsCmdArrApp fun_ty fun' arg' ho_app lr) }
   where
        -- Before type-checking f, use the environment of the enclosing
@@ -243,6 +250,9 @@ tc_cmd env cmd@(HsCmdApp x fun arg) (cmd_stk, res_ty)
     do  { arg_ty <- newOpenFlexiTyVarTy
         ; fun'   <- tcCmd env fun (mkPairTy arg_ty cmd_stk, res_ty)
         ; arg'   <- tcCheckMonoExpr arg arg_ty
+        ; _concrete_ev <- hasFixedRuntimeRep
+                        (FRRArrow $ ArrowCmdApp (unLoc fun) (unLoc arg))
+                        arg_ty
         ; return (HsCmdApp x fun' arg') }
 
 -------------------------------------------
@@ -271,6 +281,15 @@ tc_cmd env
                                          , m_pats = pats'
                                          , m_grhss = grhss' })
               arg_tys = map (unrestricted . hsLPatType) pats'
+
+        ; _concrete_evs <-
+              zipWithM
+                (\ (Scaled _ arg_ty) i ->
+                  hasFixedRuntimeRep (FRRArrow $ ArrowCmdLam i) arg_ty)
+                arg_tys
+                [1..]
+
+        ; let
               cmd' = HsCmdLam x (MG { mg_alts = L l [match']
                                     , mg_ext = MatchGroupTc arg_tys res_ty
                                     , mg_origin = origin })
@@ -326,11 +345,12 @@ tc_cmd env cmd@(HsCmdArrForm x expr f fixity cmd_args) (cmd_stk, res_ty)
 
   where
     tc_cmd_arg :: LHsCmdTop GhcRn -> TcM (LHsCmdTop GhcTc, TcType)
-    tc_cmd_arg cmd@(L _ (HsCmdTop names _))
+    tc_cmd_arg cmd@(L loc (HsCmdTop names _))
        = do { arr_ty <- newFlexiTyVarTy arrowTyConKind
             ; stk_ty <- newFlexiTyVarTy liftedTypeKind
             ; res_ty <- newFlexiTyVarTy liftedTypeKind
-            ; names' <- mapM (tcSyntaxName ProcOrigin arr_ty) names
+            ; names' <- setSrcSpan loc $
+                mapM (tcSyntaxName ArrowCmdOrigin arr_ty) names
             ; let env' = env { cmd_arr = arr_ty }
             ; cmd' <- tcCmdTop env' names' cmd (stk_ty, res_ty)
             ; return (cmd',  mkCmdArrTy env' (mkPairTy alphaTy stk_ty) res_ty) }
diff --git a/compiler/GHC/Tc/Gen/Bind.hs b/compiler/GHC/Tc/Gen/Bind.hs
index e540e3db91..93fa9a7e2c 100644
--- a/compiler/GHC/Tc/Gen/Bind.hs
+++ b/compiler/GHC/Tc/Gen/Bind.hs
@@ -34,6 +34,7 @@ import GHC.Data.FastString
 import GHC.Hs
 import GHC.Tc.Errors.Types
 import GHC.Tc.Gen.Sig
+import GHC.Tc.Utils.Concrete ( hasFixedRuntimeRep )
 import GHC.Tc.Utils.Monad
 import GHC.Tc.Types.Origin
 import GHC.Tc.Utils.Env
@@ -519,6 +520,11 @@ tcPolyBinds sig_fn prag_fn rec_group rec_tc closed bind_list
          InferGen mn        -> tcPolyInfer rec_tc prag_fn sig_fn mn bind_list
          CheckGen lbind sig -> tcPolyCheck prag_fn sig lbind
 
+    ; _concrete_evs <-
+        mapM (\ poly_id ->
+          hasFixedRuntimeRep (FRRBinder $ idName poly_id) (idType poly_id))
+          poly_ids
+
     ; traceTc "} End of bindings for" (vcat [ ppr binder_names, ppr rec_group
                                             , vcat [ppr id <+> ppr (idType id) | id <- poly_ids]
                                           ])
@@ -1181,7 +1187,7 @@ tcMonoBinds :: RecFlag  -- Whether the binding is recursive for typechecking pur
             -> [LHsBind GhcRn]
             -> TcM (LHsBinds GhcTc, [MonoBindInfo])
 
--- SPECIAL CASE 1: see Note [Inference for non-recursive function bindings]
+-- SPECIAL CASE 1: see Note [Special case for non-recursive function bindings]
 tcMonoBinds is_rec sig_fn no_gen
            [ L b_loc (FunBind { fun_id = L nm_loc name
                               , fun_matches = matches })]
@@ -1210,7 +1216,7 @@ tcMonoBinds is_rec sig_fn no_gen
                        , mbi_sig       = Nothing
                        , mbi_mono_id   = mono_id }]) }
 
--- SPECIAL CASE 2: see Note [Inference for non-recursive pattern bindings]
+-- SPECIAL CASE 2: see Note [Special case for non-recursive pattern bindings]
 tcMonoBinds is_rec sig_fn no_gen
            [L b_loc (PatBind { pat_lhs = pat, pat_rhs = grhss })]
   | NonRecursive <- is_rec   -- ...binder isn't mentioned in RHS
@@ -1470,6 +1476,7 @@ tcRhs (TcPatBind infos pat' grhss pat_ty)
     do  { traceTc "tcRhs: pat bind" (ppr pat' $$ ppr pat_ty)
         ; grhss' <- addErrCtxt (patMonoBindsCtxt pat' grhss) $
                     tcGRHSsPat grhss (mkCheckExpType pat_ty)
+
         ; return ( PatBind { pat_lhs = pat', pat_rhs = grhss'
                            , pat_ext = pat_ty
                            , pat_ticks = ([],[]) } )}
diff --git a/compiler/GHC/Tc/Gen/Expr.hs b/compiler/GHC/Tc/Gen/Expr.hs
index 899a69353e..077414b96a 100644
--- a/compiler/GHC/Tc/Gen/Expr.hs
+++ b/compiler/GHC/Tc/Gen/Expr.hs
@@ -40,6 +40,7 @@ import GHC.Types.Error
 import GHC.Core.Multiplicity
 import GHC.Core.UsageEnv
 import GHC.Tc.Errors.Types
+import GHC.Tc.Utils.Concrete ( hasFixedRuntimeRep, mkWpFun )
 import GHC.Tc.Utils.Instantiate
 import GHC.Tc.Gen.App
 import GHC.Tc.Gen.Head
@@ -344,7 +345,16 @@ tcExpr (ExplicitSum _ alt arity expr) res_ty
        ; (coi, arg_tys) <- matchExpectedTyConApp sum_tc res_ty
        ; -- Drop levity vars, we don't care about them here
          let arg_tys' = drop arity arg_tys
-       ; expr' <- tcCheckPolyExpr expr (arg_tys' `getNth` (alt - 1))
+             arg_ty   = arg_tys' `getNth` (alt - 1)
+       ; expr' <- tcCheckPolyExpr expr arg_ty
+       -- Check the whole res_ty, not just the arg_ty, to avoid #20277.
+       -- Example:
+       --   a :: TYPE rep (representation-polymorphic)
+       --   (# 17# | #) :: (# Int# | a #)
+       -- This should cause an error, even though (17# :: Int#)
+       -- is not representation-polymorphic: we don't know how
+       -- wide the concrete representation of the sum type will be.
+       ; _concrete_ev <- hasFixedRuntimeRep FRRUnboxedSum res_ty
        ; return $ mkHsWrapCo coi (ExplicitSum arg_tys' alt arity expr' ) }
 
 
@@ -938,12 +948,17 @@ tcTupArgs :: [HsTupArg GhcRn] -> [TcSigmaType] -> TcM [HsTupArg GhcTc]
 tcTupArgs args tys
   = do massert (equalLength args tys)
        checkTupSize (length args)
-       mapM go (args `zip` tys)
+       zipWith3M go [1,2..] args tys
   where
-    go (Missing {},     arg_ty) = do { mult <- newFlexiTyVarTy multiplicityTy
-                                     ; return (Missing (Scaled mult arg_ty)) }
-    go (Present x expr, arg_ty) = do { expr' <- tcCheckPolyExpr expr arg_ty
-                                     ; return (Present x expr') }
+    go :: Int -> HsTupArg GhcRn -> TcType -> TcM (HsTupArg GhcTc)
+    go i (Missing {})     arg_ty
+      = do { mult <- newFlexiTyVarTy multiplicityTy
+           ; _concrete_ev <- hasFixedRuntimeRep (FRRTupleSection i) arg_ty
+           ; return (Missing (Scaled mult arg_ty)) }
+    go i (Present x expr) arg_ty
+      = do { expr' <- tcCheckPolyExpr expr arg_ty
+           ; _concrete_ev <- hasFixedRuntimeRep (FRRTupleArg i) arg_ty
+           ; return (Present x expr') }
 
 ---------------------------
 -- See TcType.SyntaxOpType also for commentary
@@ -1003,8 +1018,8 @@ tcSynArgE :: CtOrigin
            -- ^ returns a wrapper :: (type of right shape) "->" (type passed in)
 tcSynArgE orig sigma_ty syn_ty thing_inside
   = do { (skol_wrap, (result, ty_wrapper))
-           <- tcSkolemise GenSigCtxt sigma_ty $ \ rho_ty ->
-              go rho_ty syn_ty
+           <- tcSkolemise GenSigCtxt sigma_ty
+                (\ rho_ty -> go rho_ty syn_ty)
        ; return (result, skol_wrap <.> ty_wrapper) }
     where
     go rho_ty SynAny
@@ -1046,13 +1061,11 @@ tcSynArgE orig sigma_ty syn_ty thing_inside
                        do { result <- thing_inside (arg_results ++ res_results) ([arg_mult] ++ arg_res_mults ++ res_res_mults)
                           ; return (result, arg_tc_ty, res_tc_ty, arg_mult) }}
 
-           ; return ( result
-                    , match_wrapper <.>
-                      mkWpFun (arg_wrapper2 <.> arg_wrapper1) res_wrapper
-                              (Scaled op_mult arg_ty) res_ty doc ) }
+           ; fun_wrap <- mkWpFun (arg_wrapper2 <.> arg_wrapper1) res_wrapper
+                              (Scaled op_mult arg_ty) res_ty (WpFunSyntaxOp orig)
+           ; return (result, match_wrapper <.> fun_wrap) }
       where
         herald = text "This rebindable syntax expects a function with"
-        doc = text "When checking a rebindable syntax operator arising from" <+> ppr orig
 
     go rho_ty (SynType the_ty)
       = do { wrap   <- tcSubTypePat orig GenSigCtxt the_ty rho_ty
@@ -1374,6 +1387,9 @@ tcRecordField con_like flds_w_tys (L loc (FieldOcc sel_name lbl)) rhs
   | Just field_ty <- assocMaybe flds_w_tys sel_name
       = addErrCtxt (fieldCtxt field_lbl) $
         do { rhs' <- tcCheckPolyExprNC rhs field_ty
+           ; _concrete_ev <-
+                hasFixedRuntimeRep (FRRRecordUpdate (unLoc lbl) (unLoc rhs))
+                  field_ty
            ; let field_id = mkUserLocal (nameOccName sel_name)
                                         (nameUnique sel_name)
                                         Many field_ty loc
diff --git a/compiler/GHC/Tc/Gen/Head.hs b/compiler/GHC/Tc/Gen/Head.hs
index 78f9b0265a..bfaba5efcc 100644
--- a/compiler/GHC/Tc/Gen/Head.hs
+++ b/compiler/GHC/Tc/Gen/Head.hs
@@ -22,6 +22,7 @@ module GHC.Tc.Gen.Head
        , splitHsApps, rebuildHsApps
        , addArgWrap, isHsValArg
        , countLeadingValArgs, isVisibleArg, pprHsExprArgTc
+       , countVisAndInvisValArgs, countHsWrapperInvisArgs
 
        , tcInferAppHead, tcInferAppHead_maybe
        , tcInferId, tcCheckId
@@ -75,6 +76,7 @@ import GHC.Types.SrcLoc
 import GHC.Utils.Misc
 import GHC.Data.Maybe
 import GHC.Utils.Outputable as Outputable
+import GHC.Utils.Panic
 import GHC.Utils.Panic.Plain
 import Control.Monad
 
@@ -323,6 +325,36 @@ isVisibleArg (EValArg {})  = True
 isVisibleArg (ETypeArg {}) = True
 isVisibleArg _             = False
 
+-- | Count visible and invisible value arguments in a list
+-- of 'HsExprArg' arguments.
+countVisAndInvisValArgs :: [HsExprArg id] -> Arity
+countVisAndInvisValArgs []                  = 0
+countVisAndInvisValArgs (EValArg {} : args) = 1 + countVisAndInvisValArgs args
+countVisAndInvisValArgs (EWrap wrap : args) =
+  case wrap of { EHsWrap hsWrap            -> countHsWrapperInvisArgs hsWrap + countVisAndInvisValArgs args
+               ; EPar   {}                 -> countVisAndInvisValArgs args
+               ; EExpand {}                -> countVisAndInvisValArgs args }
+countVisAndInvisValArgs (EPrag {}   : args) = countVisAndInvisValArgs args
+countVisAndInvisValArgs (ETypeArg {}: args) = countVisAndInvisValArgs args
+
+-- | Counts the number of invisible term-level arguments applied by an 'HsWrapper'.
+-- Precondition: this wrapper contains no abstractions.
+countHsWrapperInvisArgs :: HsWrapper -> Arity
+countHsWrapperInvisArgs = go
+  where
+    go WpHole = 0
+    go (WpCompose wrap1 wrap2) = go wrap1 + go wrap2
+    go fun@(WpFun {}) = nope fun
+    go (WpCast {}) = 0
+    go evLam@(WpEvLam {}) = nope evLam
+    go (WpEvApp _) = 1
+    go tyLam@(WpTyLam {}) = nope tyLam
+    go (WpTyApp _) = 0
+    go (WpLet _) = 0
+    go (WpMultCoercion {}) = 0
+
+    nope x = pprPanic "countHsWrapperInvisApps" (ppr x)
+
 instance OutputableBndrId (XPass p) => Outputable (HsExprArg p) where
   ppr (EValArg { eva_arg = arg })      = text "EValArg" <+> ppr arg
   ppr (EPrag _ p)                      = text "EPrag" <+> ppr p
diff --git a/compiler/GHC/Tc/Gen/Match.hs b/compiler/GHC/Tc/Gen/Match.hs
index c8eb8fd233..ab767b877c 100644
--- a/compiler/GHC/Tc/Gen/Match.hs
+++ b/compiler/GHC/Tc/Gen/Match.hs
@@ -49,6 +49,7 @@ import GHC.Tc.Gen.Head( tcCheckId )
 import GHC.Tc.Utils.TcMType
 import GHC.Tc.Utils.TcType
 import GHC.Tc.Gen.Bind
+import GHC.Tc.Utils.Concrete ( hasFixedRuntimeRep )
 import GHC.Tc.Utils.Unify
 import GHC.Tc.Types.Origin
 import GHC.Tc.Types.Evidence
@@ -226,6 +227,10 @@ tcMatches ctxt pat_tys rhs_ty (MG { mg_alts = L l matches
   = do { tcEmitBindingUsage bottomUE
        ; pat_tys <- mapM scaledExpTypeToType pat_tys
        ; rhs_ty  <- expTypeToType rhs_ty
+       ; _concrete_evs <- zipWithM
+                       (\ i (Scaled _ pat_ty) ->
+                         hasFixedRuntimeRep (FRRMatch (mc_what ctxt) i) pat_ty)
+                       [1..] pat_tys
        ; return (MG { mg_alts = L l []
                     , mg_ext = MatchGroupTc pat_tys rhs_ty
                     , mg_origin = origin }) }
@@ -236,6 +241,10 @@ tcMatches ctxt pat_tys rhs_ty (MG { mg_alts = L l matches
        ; tcEmitBindingUsage $ supUEs usages
        ; pat_tys  <- mapM readScaledExpType pat_tys
        ; rhs_ty   <- readExpType rhs_ty
+       ; _concrete_evs <- zipWithM
+                       (\ i (Scaled _ pat_ty) ->
+                         hasFixedRuntimeRep (FRRMatch (mc_what ctxt) i) pat_ty)
+                       [1..] pat_tys
        ; return (MG { mg_alts   = L l matches'
                     , mg_ext    = MatchGroupTc pat_tys rhs_ty
                     , mg_origin = origin }) }
@@ -431,6 +440,7 @@ tcGuardStmt ctxt (BindStmt _ pat rhs) res_ty thing_inside
           -- two multiplicity to still be the same.
           (rhs', rhs_ty) <- tcScalingUsage Many $ tcInferRhoNC rhs
                                    -- Stmt has a context already
+        ; _concrete_ev <- hasFixedRuntimeRep FRRBindStmtGuard rhs_ty
         ; (pat', thing)  <- tcCheckPat_O (StmtCtxt ctxt) (lexprCtOrigin rhs)
                                          pat (unrestricted rhs_ty) $
                             thing_inside res_ty
@@ -583,14 +593,16 @@ tcMcStmt _ (LastStmt x body noret return_op) res_ty thing_inside
 
 tcMcStmt ctxt (BindStmt xbsrn pat rhs) res_ty thing_inside
            -- (>>=) :: rhs_ty -> (pat_ty -> new_res_ty) -> res_ty
-  = do  { ((rhs', pat_mult, pat', thing, new_res_ty), bind_op')
+  = do  { ((rhs_ty, rhs', pat_mult, pat', thing, new_res_ty), bind_op')
             <- tcSyntaxOp MCompOrigin (xbsrn_bindOp xbsrn)
                           [SynRho, SynFun SynAny SynRho] res_ty $
                \ [rhs_ty, pat_ty, new_res_ty] [rhs_mult, fun_mult, pat_mult] ->
                do { rhs' <- tcScalingUsage rhs_mult $ tcCheckMonoExprNC rhs rhs_ty
                   ; (pat', thing) <- tcScalingUsage fun_mult $ tcCheckPat (StmtCtxt ctxt) pat (Scaled pat_mult pat_ty) $
                                      thing_inside (mkCheckExpType new_res_ty)
-                  ; return (rhs', pat_mult, pat', thing, new_res_ty) }
+                  ; return (rhs_ty, rhs', pat_mult, pat', thing, new_res_ty) }
+
+        ; _concrete_ev <- hasFixedRuntimeRep (FRRBindStmt MonadComprehension) rhs_ty
 
         -- If (but only if) the pattern can fail, typecheck the 'fail' operator
         ; fail_op' <- fmap join . forM (xbsrn_failOp xbsrn) $ \fail ->
@@ -613,17 +625,23 @@ tcMcStmt _ (BodyStmt _ rhs then_op guard_op) res_ty thing_inside
           --    guard_op :: test_ty -> rhs_ty
           --    then_op  :: rhs_ty -> new_res_ty -> res_ty
           -- Where test_ty is, for example, Bool
-        ; ((thing, rhs', rhs_ty, guard_op'), then_op')
+        ; ((thing, rhs', rhs_ty, new_res_ty, test_ty, guard_op'), then_op')
             <- tcSyntaxOp MCompOrigin then_op [SynRho, SynRho] res_ty $
                \ [rhs_ty, new_res_ty] [rhs_mult, fun_mult] ->
-               do { (rhs', guard_op')
+               do { ((rhs', test_ty), guard_op')
                       <- tcScalingUsage rhs_mult $
                          tcSyntaxOp MCompOrigin guard_op [SynAny]
                                     (mkCheckExpType rhs_ty) $
-                         \ [test_ty] [test_mult] ->
-                         tcScalingUsage test_mult $ tcCheckMonoExpr rhs test_ty
+                         \ [test_ty] [test_mult] -> do
+                           rhs' <- tcScalingUsage test_mult $ tcCheckMonoExpr rhs test_ty
+                           return $ (rhs', test_ty)
                   ; thing <- tcScalingUsage fun_mult $ thing_inside (mkCheckExpType new_res_ty)
-                  ; return (thing, rhs', rhs_ty, guard_op') }
+                  ; return (thing, rhs', rhs_ty, new_res_ty, test_ty, guard_op') }
+
+        ; _evTerm1 <- hasFixedRuntimeRep FRRBodyStmtGuard test_ty
+        ; _evTerm2 <- hasFixedRuntimeRep (FRRBodyStmt MonadComprehension 1) rhs_ty
+        ; _evTerm3 <- hasFixedRuntimeRep (FRRBodyStmt MonadComprehension 2) new_res_ty
+
         ; return (BodyStmt rhs_ty rhs' then_op' guard_op', thing) }
 
 -- Grouping statements
@@ -850,13 +868,15 @@ tcDoStmt ctxt (BindStmt xbsrn pat rhs) res_ty thing_inside
                 -- This level of generality is needed for using do-notation
                 -- in full generality; see #1537
 
-          ((rhs', pat_mult, pat', new_res_ty, thing), bind_op')
+          ((rhs_ty, rhs', pat_mult, pat', new_res_ty, thing), bind_op')
             <- tcSyntaxOp DoOrigin (xbsrn_bindOp xbsrn) [SynRho, SynFun SynAny SynRho] res_ty $
                 \ [rhs_ty, pat_ty, new_res_ty] [rhs_mult,fun_mult,pat_mult] ->
                 do { rhs' <-tcScalingUsage rhs_mult $ tcCheckMonoExprNC rhs rhs_ty
                    ; (pat', thing) <- tcScalingUsage fun_mult $ tcCheckPat (StmtCtxt ctxt) pat (Scaled pat_mult pat_ty) $
                                       thing_inside (mkCheckExpType new_res_ty)
-                   ; return (rhs', pat_mult, pat', new_res_ty, thing) }
+                   ; return (rhs_ty, rhs', pat_mult, pat', new_res_ty, thing) }
+
+        ; _concrete_ev <- hasFixedRuntimeRep (FRRBindStmt DoNotation) rhs_ty
 
         -- If (but only if) the pattern can fail, typecheck the 'fail' operator
         ; fail_op' <- fmap join . forM (xbsrn_failOp xbsrn) $ \fail ->
@@ -884,12 +904,14 @@ tcDoStmt ctxt (ApplicativeStmt _ pairs mb_join) res_ty thing_inside
 tcDoStmt _ (BodyStmt _ rhs then_op _) res_ty thing_inside
   = do  {       -- Deal with rebindable syntax;
                 --   (>>) :: rhs_ty -> new_res_ty -> res_ty
-        ; ((rhs', rhs_ty, thing), then_op')
+        ; ((rhs', rhs_ty, new_res_ty, thing), then_op')
             <- tcSyntaxOp DoOrigin then_op [SynRho, SynRho] res_ty $
                \ [rhs_ty, new_res_ty] [rhs_mult,fun_mult] ->
                do { rhs' <- tcScalingUsage rhs_mult $ tcCheckMonoExprNC rhs rhs_ty
                   ; thing <- tcScalingUsage fun_mult $ thing_inside (mkCheckExpType new_res_ty)
-                  ; return (rhs', rhs_ty, thing) }
+                  ; return (rhs', rhs_ty, new_res_ty, thing) }
+        ; _evTerm1 <- hasFixedRuntimeRep (FRRBodyStmt DoNotation 1) rhs_ty
+        ; _evTerm2 <- hasFixedRuntimeRep (FRRBodyStmt DoNotation 2) new_res_ty
         ; return (BodyStmt rhs_ty rhs' then_op' noSyntaxExpr, thing) }
 
 tcDoStmt ctxt (RecStmt { recS_stmts = L l stmts, recS_later_ids = later_names
diff --git a/compiler/GHC/Tc/Gen/Pat.hs b/compiler/GHC/Tc/Gen/Pat.hs
index 78a4e22901..332ea601b1 100644
--- a/compiler/GHC/Tc/Gen/Pat.hs
+++ b/compiler/GHC/Tc/Gen/Pat.hs
@@ -36,6 +36,7 @@ import GHC.Rename.Utils
 import GHC.Tc.Errors.Types
 import GHC.Tc.Utils.Zonk
 import GHC.Tc.Gen.Sig( TcPragEnv, lookupPragEnv, addInlinePrags )
+import GHC.Tc.Utils.Concrete ( mkWpFun )
 import GHC.Tc.Utils.Monad
 import GHC.Tc.Utils.Instantiate
 import GHC.Types.Error
@@ -445,12 +446,12 @@ tc_pat pat_ty penv ps_pat thing_inside = case ps_pat of
 
         ; let Scaled w h_pat_ty = pat_ty
         ; pat_ty <- readExpType h_pat_ty
-        ; let expr_wrap2' = mkWpFun expr_wrap2 idHsWrapper
-                                    (Scaled w pat_ty) inf_res_sigma doc
-               -- expr_wrap2' :: (inf_arg_ty -> inf_res_sigma) "->"
-               --                (pat_ty -> inf_res_sigma)
+        ; expr_wrap2' <- mkWpFun expr_wrap2 idHsWrapper
+                            (Scaled w pat_ty) inf_res_sigma (WpFunViewPat $ unLoc expr)
+        -- expr_wrap2' :: (inf_arg_ty -> inf_res_sigma) "->"
+        --                (pat_ty -> inf_res_sigma)
+        ; let
               expr_wrap = expr_wrap2' <.> expr_wrap1 <.> mult_wrap
-              doc = text "When checking the view pattern function:" <+> (ppr expr)
 
         ; return $ (ViewPat pat_ty (mkLHsWrap expr_wrap expr') pat', res) }
 
@@ -656,6 +657,7 @@ AST is used for the subtraction operation.
                   ; return (lit2', wrap, bndr_id) }
 
         ; pat_ty <- readExpType pat_exp_ty
+
         -- The Report says that n+k patterns must be in Integral
         -- but it's silly to insist on this in the RebindableSyntax case
         ; unlessM (xoptM LangExt.RebindableSyntax) $
diff --git a/compiler/GHC/Tc/Gen/Rule.hs b/compiler/GHC/Tc/Gen/Rule.hs
index 73dedfbaf5..46b1e16313 100644
--- a/compiler/GHC/Tc/Gen/Rule.hs
+++ b/compiler/GHC/Tc/Gen/Rule.hs
@@ -477,12 +477,17 @@ getRuleQuantCts wc
         new_skol_tvs = skol_tvs `extendVarSetList` ic_skols imp
 
     rule_quant_ct :: TcTyCoVarSet -> Ct -> Bool
-    rule_quant_ct skol_tvs ct
-      | EqPred _ t1 t2 <- classifyPredType (ctPred ct)
-      , not (ok_eq t1 t2)
-       = False        -- Note [RULE quantification over equalities]
-      | otherwise
-      = tyCoVarsOfCt ct `disjointVarSet` skol_tvs
+    rule_quant_ct skol_tvs ct = case classifyPredType (ctPred ct) of
+      EqPred _ t1 t2
+        | not (ok_eq t1 t2)
+        -> False        -- Note [RULE quantification over equalities]
+      SpecialPred {}
+        -- RULES must never quantify over special predicates, as that
+        -- would leak internal GHC implementation details to the user.
+        --
+        -- Tests (for Concrete# predicates): RepPolyRule{1,2,3}.
+        -> False
+      _ -> tyCoVarsOfCt ct `disjointVarSet` skol_tvs
 
     ok_eq t1 t2
        | t1 `tcEqType` t2 = False
diff --git a/compiler/GHC/Tc/Gen/Sig.hs b/compiler/GHC/Tc/Gen/Sig.hs
index 67715e9b5b..bec5af03b0 100644
--- a/compiler/GHC/Tc/Gen/Sig.hs
+++ b/compiler/GHC/Tc/Gen/Sig.hs
@@ -32,15 +32,15 @@ import GHC.Driver.Backend
 import GHC.Hs
 
 
-import GHC.Tc.Errors.Types ( TcRnMessage(..), LevityCheckProvenance(..) )
+import GHC.Tc.Errors.Types ( FixedRuntimeRepProvenance(..), TcRnMessage(..) )
 import GHC.Tc.Gen.HsType
 import GHC.Tc.Types
 import GHC.Tc.Solver( pushLevelAndSolveEqualitiesX, reportUnsolvedEqualities )
 import GHC.Tc.Utils.Monad
+import GHC.Tc.Utils.TcMType ( checkTypeHasFixedRuntimeRep )
 import GHC.Tc.Utils.Zonk
 import GHC.Tc.Types.Origin
 import GHC.Tc.Utils.TcType
-import GHC.Tc.Utils.TcMType
 import GHC.Tc.Validity ( checkValidType )
 import GHC.Tc.Utils.Unify( tcSkolemise, unifyType )
 import GHC.Tc.Utils.Instantiate( topInstantiate, tcInstTypeBndrs )
@@ -452,10 +452,15 @@ tcPatSynSig name sig_ty@(L _ (HsSig{sig_bndrs = hs_outer_bndrs, sig_body = hs_ty
        ; checkValidType ctxt $
          build_patsyn_type implicit_bndrs univ_bndrs req ex_bndrs prov body_ty
 
-       -- arguments become the types of binders. We thus cannot allow
-       -- representation polymorphism here
-       ; let (arg_tys, _) = tcSplitFunTys body_ty
-       ; mapM_ (checkForLevPoly LevityCheckPatSynSig . scaledThing) arg_tys
+       -- Neither argument types nor the return type may be representation polymorphic.
+       -- This is because, when creating a matcher:
+       --   - the argument types become the the binder types (see test RepPolyPatySynArg),
+       --   - the return type becomes the scrutinee type (see test RepPolyPatSynRes).
+       ; let (arg_tys, res_ty) = tcSplitFunTys body_ty
+       ; mapM_
+           (\(Scaled _ arg_ty) -> checkTypeHasFixedRuntimeRep FixedRuntimeRepPatSynSigArg arg_ty)
+           arg_tys
+       ; checkTypeHasFixedRuntimeRep FixedRuntimeRepPatSynSigRes res_ty
 
        ; traceTc "tcTySig }" $
          vcat [ text "kvs"          <+> ppr_tvs (binderVars kv_bndrs)