Fix isLiftedType_maybe and handle fallout

As #20837 pointed out, `isLiftedType_maybe` returned `Just False` in
many situations where it should return `Nothing`, because it didn't
take into account type families or type variables.

In this patch, we fix this issue. We rename `isLiftedType_maybe` to
`typeLevity_maybe`, which now returns a `Levity` instead of a boolean.
We now return `Nothing` for types with kinds of the form
`TYPE (F a1 ... an)` for a type family `F`, as well as
`TYPE (BoxedRep l)` where `l` is a type variable.

This fix caused several other problems, as other parts of the compiler
were relying on `isLiftedType_maybe` returning a `Just` value, and were
now panicking after the above fix. There were two main situations in
which panics occurred:

  1. Issues involving the let/app invariant. To uphold that invariant,
     we need to know whether something is lifted or not. If we get an
     answer of `Nothing` from `isLiftedType_maybe`, then we don't know
     what to do. As this invariant isn't particularly invariant, we
     can change the affected functions to not panic, e.g. by behaving
     the same in the `Just False` case and in the `Nothing` case
     (meaning: no observable change in behaviour compared to before).

  2. Typechecking of data (/newtype) constructor patterns. Some programs
     involving patterns with unknown representations were accepted, such
     as T20363. Now that we are stricter, this caused further issues,
     culminating in Core Lint errors. However, the behaviour was
     incorrect the whole time; the incorrectness only being revealed by
     this change, not triggered by it.

     This patch fixes this by overhauling where the representation
     polymorphism involving pattern matching are done. Instead of doing
     it in `tcMatches`, we instead ensure that the `matchExpected`
     functions such as `matchExpectedFunTys`, `matchActualFunTySigma`,
     `matchActualFunTysRho` allow return argument pattern types which
     have a fixed RuntimeRep (as defined in Note [Fixed RuntimeRep]).
     This ensures that the pattern matching code only ever handles types
     with a known runtime representation. One exception was that
     patterns with an unknown representation type could sneak in via
     `tcConPat`, which points to a missing representation-polymorphism
     check, which this patch now adds.

     This means that we now reject the program in #20363, at least until
     we implement PHASE 2 of FixedRuntimeRep (allowing type families in
     RuntimeRep positions). The aforementioned refactoring, in which
     checks have been moved to `matchExpected` functions, is a first
     step in implementing PHASE 2 for patterns.

Fixes #20837

21 files changed, 499 insertions, 265 deletions

diff --git a/compiler/GHC/Tc/Deriv/Generics.hs b/compiler/GHC/Tc/Deriv/Generics.hs
index dde32082e6..6240de3205 100644
--- a/compiler/GHC/Tc/Deriv/Generics.hs
+++ b/compiler/GHC/Tc/Deriv/Generics.hs
@@ -183,7 +183,7 @@ canDoGenerics dit@(DerivInstTys{dit_rep_tc = tc})
 
         -- Nor can we do the job if it's an existential data constructor,
         -- Nor if the args are polymorphic types (I don't think)
-    bad_arg_type ty = (isUnliftedType ty && not (allowedUnliftedTy ty))
+    bad_arg_type ty = (mightBeUnliftedType ty && not (allowedUnliftedTy ty))
                       || not (isTauTy ty)
 
 -- Returns True the Type argument is an unlifted type which has a
diff --git a/compiler/GHC/Tc/Deriv/Utils.hs b/compiler/GHC/Tc/Deriv/Utils.hs
index 5fe1f6b185..d25db38be0 100644
--- a/compiler/GHC/Tc/Deriv/Utils.hs
+++ b/compiler/GHC/Tc/Deriv/Utils.hs
@@ -911,7 +911,7 @@ cond_args cls _ dit@(DerivInstTys{dit_rep_tc = rep_tc})
   where
     bad_args = [ arg_ty | con <- tyConDataCons rep_tc
                         , arg_ty <- derivDataConInstArgTys con dit
-                        , isLiftedType_maybe arg_ty /= Just True
+                        , mightBeUnliftedType arg_ty
                         , not (ok_ty arg_ty) ]
 
     cls_key = classKey cls
diff --git a/compiler/GHC/Tc/Errors/Ppr.hs b/compiler/GHC/Tc/Errors/Ppr.hs
index f6e71f57cf..ad78cfaf76 100644
--- a/compiler/GHC/Tc/Errors/Ppr.hs
+++ b/compiler/GHC/Tc/Errors/Ppr.hs
@@ -1741,8 +1741,43 @@ pprTcSolverReportMsg _ (FixedRuntimeRepError frr_infos) =
         (if length frr_infos > 1 then (bullet <+>) else id) $
           vcat [ sep [ pprFRROrigin frr_orig
                      , text "does not have a fixed runtime representation." ]
-               , text "Its type is:"
-               , nest 2 $ ppr ty <+> dcolon <+> pprWithTYPE (typeKind ty) ]
+               , type_printout ty ]
+
+    -- Don't print out the type (only the kind), if the type includes
+    -- a confusing cast, unless the user passed -fprint-explicit-coercions.
+    --
+    -- Example:
+    --
+    --   In T20363, we have a representation-polymorphism error with a type
+    --   of the form
+    --
+    --     ( (# #) |> co ) :: TYPE NilRep
+    --
+    --   where NilRep is a nullary type family application which reduces to TupleRep '[].
+    --   We prefer avoiding showing the cast to the user, but we also don't want to
+    --   print the confusing:
+    --
+    --     (# #) :: TYPE NilRep
+    --
+    --  So in this case we simply don't print the type, only the kind.
+    confusing_cast :: Type -> Bool
+    confusing_cast ty =
+      case ty of
+        CastTy inner_ty _
+          -- A confusing cast is one that is responsible
+          -- for a representation-polymorphism error.
+          -> isConcrete (typeKind inner_ty)
+        _ -> False
+
+    type_printout :: Type -> SDoc
+    type_printout ty =
+      sdocOption sdocPrintExplicitCoercions $ \ show_coercions ->
+        if confusing_cast ty && not show_coercions
+        then vcat [ text "Its kind is:"
+                  , nest 2 $ pprWithTYPE (typeKind ty)
+                  , text "(Use -fprint-explicit-coercions to see the full type.)" ]
+        else vcat [ text "Its type is:"
+                  , nest 2 $ ppr ty <+> dcolon <+> pprWithTYPE (typeKind ty) ]
 
     -- In PHASE 1 of FixedRuntimeRep, we don't allow rewriting in hasFixedRuntimeRep,
     -- so we add a special message to explain this to the user.
diff --git a/compiler/GHC/Tc/Gen/App.hs b/compiler/GHC/Tc/Gen/App.hs
index ddf94f1410..743587ed25 100644
--- a/compiler/GHC/Tc/Gen/App.hs
+++ b/compiler/GHC/Tc/Gen/App.hs
@@ -22,7 +22,7 @@ module GHC.Tc.Gen.App
 
 import {-# SOURCE #-} GHC.Tc.Gen.Expr( tcPolyExpr )
 
-import GHC.Types.Basic ( Arity )
+import GHC.Types.Basic ( Arity, ExprOrPat(Expression) )
 import GHC.Types.Id ( idArity, idName, hasNoBinding )
 import GHC.Types.Name ( isWiredInName )
 import GHC.Types.Var
@@ -547,7 +547,7 @@ hasFixedRuntimeRep_remainingValArgs applied_args app_res_rho = \case
   -- (4): Unboxed tuples and unboxed sums
     || isUnboxedTupleDataCon con
     || isUnboxedSumDataCon con
-    -> check_thing con (dataConRepArity con) (FRRDataConArg con)
+    -> check_thing con (dataConRepArity con) (FRRDataConArg Expression con)
 
   _ -> return ()
 
@@ -673,12 +673,11 @@ tcValArgs do_ql args
            ; return (eva { eva_arg    = ValArg arg'
                          , eva_arg_ty = Scaled mult arg_ty }) }
 
-tcEValArg :: AppCtxt -> EValArg 'TcpInst -> TcSigmaType -> TcM (LHsExpr GhcTc)
+tcEValArg :: AppCtxt -> EValArg 'TcpInst -> TcSigmaTypeFRR -> TcM (LHsExpr GhcTc)
 -- Typecheck one value argument of a function call
 tcEValArg ctxt (ValArg larg@(L arg_loc arg)) exp_arg_sigma
   = addArgCtxt ctxt larg $
     do { arg' <- tcPolyExpr arg (mkCheckExpType exp_arg_sigma)
-       ; hasFixedRuntimeRep_MustBeRefl (FRRApp arg') exp_arg_sigma
        ; return (L arg_loc arg') }
 
 tcEValArg ctxt (ValArgQL { va_expr = larg@(L arg_loc _)
@@ -690,7 +689,6 @@ tcEValArg ctxt (ValArgQL { va_expr = larg@(L arg_loc _)
        ; 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
-       ; hasFixedRuntimeRep_MustBeRefl (FRRApp arg') exp_arg_sigma
        ; traceTc "tcEValArgQL }" empty
        ; return (L arg_loc arg') }
 
@@ -741,9 +739,6 @@ tcInstFun do_ql inst_final (rn_fun, fun_ctxt) fun_sigma rn_args
           VAExpansion orig _ -> addExprCtxt orig thing_inside
           VACall {}          -> thing_inside
 
-    herald = sep [ text "The function" <+> quotes (ppr rn_fun)
-                 , text "is applied to"]
-
     -- Count value args only when complaining about a function
     -- applied to too many value args
     -- See Note [Herald for matchExpectedFunTys] in GHC.Tc.Utils.Unify.
@@ -776,8 +771,8 @@ tcInstFun do_ql inst_final (rn_fun, fun_ctxt) fun_sigma rn_args
 
     -----------
     go, go1 :: Delta
-            -> [HsExprArg 'TcpInst]  -- Accumulator, reversed
-            -> [Scaled TcSigmaType]  -- Value args to which applied so far
+            -> [HsExprArg 'TcpInst]     -- Accumulator, reversed
+            -> [Scaled TcSigmaTypeFRR]  -- Value args to which applied so far
             -> TcSigmaType -> [HsExprArg 'TcpRn]
             -> TcM (Delta, [HsExprArg 'TcpInst], TcSigmaType)
 
@@ -873,10 +868,12 @@ tcInstFun do_ql inst_final (rn_fun, fun_ctxt) fun_sigma rn_args
 
     -- Rule IARG from Fig 4 of the QL paper:
     go1 delta acc so_far fun_ty
-        (eva@(EValArg { eva_arg = ValArg arg, eva_ctxt = ctxt })  : rest_args)
-      = do { (wrap, arg_ty, res_ty) <- matchActualFunTySigma herald
-                                          (Just $ HsExprRnThing rn_fun)
-                                          (n_val_args, so_far) fun_ty
+        (eva@(EValArg { eva_arg = ValArg arg, eva_ctxt = ctxt }) : rest_args)
+      = do { (wrap, arg_ty, res_ty) <-
+                matchActualFunTySigma
+                  (ExpectedFunTyArg (HsExprRnThing rn_fun) (unLoc arg))
+                  (Just $ HsExprRnThing rn_fun)
+                  (n_val_args, so_far) fun_ty
           ; (delta', arg') <- if do_ql
                               then addArgCtxt ctxt arg $
                                    -- Context needed for constraints
@@ -1053,8 +1050,8 @@ Wrinkles:
 
 ----------------
 quickLookArg :: Delta
-             -> LHsExpr GhcRn       -- Argument
-             -> Scaled TcSigmaType  -- Type expected by the function
+             -> LHsExpr GhcRn          -- ^ Argument
+             -> Scaled TcSigmaTypeFRR  -- ^ Type expected by the function
              -> TcM (Delta, EValArg 'TcpInst)
 -- See Note [Quick Look at value arguments]
 --
@@ -1093,7 +1090,7 @@ isGuardedTy ty
   | Just {} <- tcSplitAppTy_maybe ty        = True
   | otherwise                               = False
 
-quickLookArg1 :: Bool -> Delta -> LHsExpr GhcRn -> TcSigmaType
+quickLookArg1 :: Bool -> Delta -> LHsExpr GhcRn -> TcSigmaTypeFRR
               -> TcM (Delta, EValArg 'TcpInst)
 quickLookArg1 guarded delta larg@(L _ arg) arg_ty
   = do { let (fun@(rn_fun, fun_ctxt), rn_args) = splitHsApps arg
diff --git a/compiler/GHC/Tc/Gen/Arrow.hs b/compiler/GHC/Tc/Gen/Arrow.hs
index dd3d19dfab..ad4b67ee88 100644
--- a/compiler/GHC/Tc/Gen/Arrow.hs
+++ b/compiler/GHC/Tc/Gen/Arrow.hs
@@ -163,12 +163,18 @@ tc_cmd env (HsCmdLet x tkLet binds tkIn (L body_loc body)) res_ty
 tc_cmd env in_cmd@(HsCmdCase x scrut matches) (stk, res_ty)
   = addErrCtxt (cmdCtxt in_cmd) $ do
       (scrut', scrut_ty) <- tcInferRho scrut
+      hasFixedRuntimeRep_MustBeRefl
+        (FRRArrow $ ArrowCmdCase { isCmdLamCase = False })
+        scrut_ty
       matches' <- tcCmdMatches env scrut_ty matches (stk, res_ty)
       return (HsCmdCase x scrut' matches')
 
 tc_cmd env in_cmd@(HsCmdLamCase x matches) (stk, res_ty)
   = addErrCtxt (cmdCtxt in_cmd) $ do
       (co, [scrut_ty], stk') <- matchExpectedCmdArgs 1 stk
+      hasFixedRuntimeRep_MustBeRefl
+        (FRRArrow $ ArrowCmdCase { isCmdLamCase = True })
+        scrut_ty
       matches' <- tcCmdMatches env scrut_ty matches (stk', res_ty)
       return (mkHsCmdWrap (mkWpCastN co) (HsCmdLamCase x matches'))
 
@@ -365,7 +371,9 @@ tc_cmd _ cmd _
 -- | Typechecking for case command alternatives. Used for both
 -- 'HsCmdCase' and 'HsCmdLamCase'.
 tcCmdMatches :: CmdEnv
-             -> TcType                           -- ^ type of the scrutinee
+             -> TcType -- ^ Type of the scrutinee.
+                       -- Must have a fixed RuntimeRep as per
+                       -- Note [Fixed RuntimeRep] in GHC.Tc.Utils.Concrete
              -> MatchGroup GhcRn (LHsCmd GhcRn)  -- ^ case alternatives
              -> CmdType
              -> TcM (MatchGroup GhcTc (LHsCmd GhcTc))
diff --git a/compiler/GHC/Tc/Gen/Bind.hs b/compiler/GHC/Tc/Gen/Bind.hs
index a14ff790fa..3adbb1b0d6 100644
--- a/compiler/GHC/Tc/Gen/Bind.hs
+++ b/compiler/GHC/Tc/Gen/Bind.hs
@@ -1212,7 +1212,7 @@ tcMonoBinds is_rec sig_fn no_gen
     do { (grhss', pat_ty) <- tcInfer $ \ exp_ty ->
                              tcGRHSsPat grhss exp_ty
 
-       ; let exp_pat_ty :: Scaled ExpSigmaType
+       ; let exp_pat_ty :: Scaled ExpSigmaTypeFRR
              exp_pat_ty = unrestricted (mkCheckExpType pat_ty)
        ; (pat', mbis) <- tcLetPat (const Nothing) no_gen pat exp_pat_ty $
                          mapM lookupMBI bndrs
@@ -1342,7 +1342,7 @@ mono_id in the first place.
 data TcMonoBind         -- Half completed; LHS done, RHS not done
   = TcFunBind  MonoBindInfo  SrcSpan (MatchGroup GhcRn (LHsExpr GhcRn))
   | TcPatBind [MonoBindInfo] (LPat GhcTc) (GRHSs GhcRn (LHsExpr GhcRn))
-              TcSigmaType
+              TcSigmaTypeFRR
 
 tcLhs :: TcSigFun -> LetBndrSpec -> HsBind GhcRn -> TcM TcMonoBind
 -- Only called with plan InferGen (LetBndrSpec = LetLclBndr)
diff --git a/compiler/GHC/Tc/Gen/Expr.hs b/compiler/GHC/Tc/Gen/Expr.hs
index 189eb989c5..3043bed44c 100644
--- a/compiler/GHC/Tc/Gen/Expr.hs
+++ b/compiler/GHC/Tc/Gen/Expr.hs
@@ -40,7 +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_MustBeRefl, mkWpFun )
+import GHC.Tc.Utils.Concrete ( hasFixedRuntimeRep_MustBeRefl )
 import GHC.Tc.Utils.Instantiate
 import GHC.Tc.Gen.App
 import GHC.Tc.Gen.Head
@@ -262,22 +262,15 @@ tcExpr (HsLam _ match) res_ty
         ; return (mkHsWrap wrap (HsLam noExtField match')) }
   where
     match_ctxt = MC { mc_what = LambdaExpr, mc_body = tcBody }
-    herald = sep [ text "The lambda expression" <+>
-                   quotes (pprSetDepth (PartWay 1) $
-                           pprMatches match),
-                        -- The pprSetDepth makes the abstraction print briefly
-                   text "has"]
+    herald = ExpectedFunTyLam match
 
 tcExpr e@(HsLamCase x matches) res_ty
   = do { (wrap, matches')
-           <- tcMatchLambda msg match_ctxt matches res_ty
-           -- The laziness annotation is because we don't want to fail here
-           -- if there are multiple arguments
+           <- tcMatchLambda herald match_ctxt matches res_ty
        ; return (mkHsWrap wrap $ HsLamCase x matches') }
   where
-    msg = sep [ text "The function" <+> quotes (ppr e)
-              , text "requires"]
     match_ctxt = MC { mc_what = CaseAlt, mc_body = tcBody }
+    herald = ExpectedFunTyLamCase e
 
 
 
@@ -391,6 +384,7 @@ tcExpr (HsCase x scrut matches) res_ty
         ; (scrut', scrut_ty) <- tcScalingUsage mult $ tcInferRho scrut
 
         ; traceTc "HsCase" (ppr scrut_ty)
+        ; hasFixedRuntimeRep_MustBeRefl FRRCase scrut_ty
         ; matches' <- tcMatchesCase match_ctxt (Scaled mult scrut_ty) matches res_ty
         ; return (HsCase x scrut' matches') }
  where
@@ -945,7 +939,12 @@ arithSeqEltType (Just fl) res_ty
        ; return (idHsWrapper, elt_mult, elt_ty, Just fl') }
 
 ----------------
-tcTupArgs :: [HsTupArg GhcRn] -> [TcSigmaType] -> TcM [HsTupArg GhcTc]
+tcTupArgs :: [HsTupArg GhcRn]
+          -> [TcSigmaType]
+              -- ^ Argument types.
+              -- This function ensures they all have
+              -- a fixed runtime representation.
+          -> TcM [HsTupArg GhcTc]
 tcTupArgs args tys
   = do massert (equalLength args tys)
        checkTupSize (length args)
@@ -984,14 +983,14 @@ tcSyntaxOpGen :: CtOrigin
               -> SyntaxExprRn
               -> [SyntaxOpType]
               -> SyntaxOpType
-              -> ([TcSigmaType] -> [Mult] -> TcM a)
+              -> ([TcSigmaTypeFRR] -> [Mult] -> TcM a)
               -> TcM (a, SyntaxExprTc)
 tcSyntaxOpGen orig (SyntaxExprRn op) arg_tys res_ty thing_inside
   = do { (expr, sigma) <- tcInferAppHead (op, VACall op 0 noSrcSpan) []
              -- Ugh!! But all this code is scheduled for demolition anyway
        ; traceTc "tcSyntaxOpGen" (ppr op $$ ppr expr $$ ppr sigma)
        ; (result, expr_wrap, arg_wraps, res_wrap)
-           <- tcSynArgA orig sigma arg_tys res_ty $
+           <- tcSynArgA orig op sigma arg_tys res_ty $
               thing_inside
        ; traceTc "tcSyntaxOpGen" (ppr op $$ ppr expr $$ ppr sigma )
        ; return (result, SyntaxExprTc { syn_expr = mkHsWrap expr_wrap expr
@@ -1012,12 +1011,13 @@ two tcSynArgs.
 -- works on "expected" types, skolemising where necessary
 -- See Note [tcSynArg]
 tcSynArgE :: CtOrigin
+          -> HsExpr GhcRn -- ^ the operator to check (for error messages only)
           -> TcSigmaType
           -> SyntaxOpType                -- ^ shape it is expected to have
-          -> ([TcSigmaType] -> [Mult] -> TcM a) -- ^ check the arguments
+          -> ([TcSigmaTypeFRR] -> [Mult] -> TcM a) -- ^ check the arguments
           -> TcM (a, HsWrapper)
            -- ^ returns a wrapper :: (type of right shape) "->" (type passed in)
-tcSynArgE orig sigma_ty syn_ty thing_inside
+tcSynArgE orig op sigma_ty syn_ty thing_inside
   = do { (skol_wrap, (result, ty_wrapper))
            <- tcSkolemise GenSigCtxt sigma_ty
                 (\ rho_ty -> go rho_ty syn_ty)
@@ -1055,18 +1055,20 @@ tcSynArgE orig sigma_ty syn_ty thing_inside
                                    pprCtOrigin orig)
 
                      ; let arg_mult = scaledMult arg_ty
-                     ; tcSynArgA orig arg_tc_ty [] arg_shape $
+                     ; tcSynArgA orig op arg_tc_ty [] arg_shape $
                        \ arg_results arg_res_mults ->
-                       tcSynArgE orig res_tc_ty res_shape $
+                       tcSynArgE orig op res_tc_ty res_shape $
                        \ res_results res_res_mults ->
                        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) }}
 
-           ; fun_wrap <- mkWpFun (arg_wrapper2 <.> arg_wrapper1) res_wrapper
-                              (Scaled op_mult arg_ty) res_ty (WpFunSyntaxOp orig)
+           ; let fun_wrap = mkWpFun (arg_wrapper2 <.> arg_wrapper1) res_wrapper
+                              (Scaled op_mult arg_ty) res_ty
+               -- NB: arg_ty comes from matchExpectedFunTys, so it has a
+               -- fixed RuntimeRep, as needed to call mkWpFun.
            ; return (result, match_wrapper <.> fun_wrap) }
       where
-        herald = text "This rebindable syntax expects a function with"
+        herald = ExpectedFunTySyntaxOp orig op
 
     go rho_ty (SynType the_ty)
       = do { wrap   <- tcSubTypePat orig GenSigCtxt the_ty rho_ty
@@ -1076,15 +1078,16 @@ tcSynArgE orig sigma_ty syn_ty thing_inside
 -- works on "actual" types, instantiating where necessary
 -- See Note [tcSynArg]
 tcSynArgA :: CtOrigin
+          -> HsExpr GhcRn -- ^ the operator we are checking (for error messages)
           -> TcSigmaType
           -> [SyntaxOpType]              -- ^ argument shapes
           -> SyntaxOpType                -- ^ result shape
-          -> ([TcSigmaType] -> [Mult] -> TcM a) -- ^ check the arguments
+          -> ([TcSigmaTypeFRR] -> [Mult] -> TcM a) -- ^ check the arguments
           -> TcM (a, HsWrapper, [HsWrapper], HsWrapper)
             -- ^ returns a wrapper to be applied to the original function,
             -- wrappers to be applied to arguments
             -- and a wrapper to be applied to the overall expression
-tcSynArgA orig sigma_ty arg_shapes res_shape thing_inside
+tcSynArgA orig op sigma_ty arg_shapes res_shape thing_inside
   = do { (match_wrapper, arg_tys, res_ty)
            <- matchActualFunTysRho herald orig Nothing
                                    (length arg_shapes) sigma_ty
@@ -1095,22 +1098,22 @@ tcSynArgA orig sigma_ty arg_shapes res_shape thing_inside
               thing_inside (arg_results ++ res_results) (map scaledMult arg_tys ++ arg_res_mults)
        ; return (result, match_wrapper, arg_wrappers, res_wrapper) }
   where
-    herald = text "This rebindable syntax expects a function with"
+    herald = ExpectedFunTySyntaxOp orig op
 
-    tc_syn_args_e :: [TcSigmaType] -> [SyntaxOpType]
-                  -> ([TcSigmaType] -> [Mult] -> TcM a)
+    tc_syn_args_e :: [TcSigmaTypeFRR] -> [SyntaxOpType]
+                  -> ([TcSigmaTypeFRR] -> [Mult] -> TcM a)
                   -> TcM (a, [HsWrapper])
                     -- the wrappers are for arguments
     tc_syn_args_e (arg_ty : arg_tys) (arg_shape : arg_shapes) thing_inside
       = do { ((result, arg_wraps), arg_wrap)
-               <- tcSynArgE     orig arg_ty  arg_shape  $ \ arg1_results arg1_mults ->
-                  tc_syn_args_e      arg_tys arg_shapes $ \ args_results args_mults ->
+               <- tcSynArgE     orig  op arg_ty  arg_shape  $ \ arg1_results arg1_mults ->
+                  tc_syn_args_e          arg_tys arg_shapes $ \ args_results args_mults ->
                   thing_inside (arg1_results ++ args_results) (arg1_mults ++ args_mults)
            ; return (result, arg_wrap : arg_wraps) }
     tc_syn_args_e _ _ thing_inside = (, []) <$> thing_inside [] []
 
-    tc_syn_arg :: TcSigmaType -> SyntaxOpType
-               -> ([TcSigmaType] -> TcM a)
+    tc_syn_arg :: TcSigmaTypeFRR -> SyntaxOpType
+               -> ([TcSigmaTypeFRR] -> TcM a)
                -> TcM (a, HsWrapper)
                   -- the wrapper applies to the overall result
     tc_syn_arg res_ty SynAny thing_inside
diff --git a/compiler/GHC/Tc/Gen/Expr.hs-boot b/compiler/GHC/Tc/Gen/Expr.hs-boot
index 22abe79491..6850e8aed2 100644
--- a/compiler/GHC/Tc/Gen/Expr.hs-boot
+++ b/compiler/GHC/Tc/Gen/Expr.hs-boot
@@ -1,7 +1,8 @@
 module GHC.Tc.Gen.Expr where
 import GHC.Hs              ( HsExpr, LHsExpr, SyntaxExprRn
                            , SyntaxExprTc )
-import GHC.Tc.Utils.TcType ( TcRhoType, TcSigmaType, SyntaxOpType
+import GHC.Tc.Utils.TcType ( TcRhoType, TcSigmaType, TcSigmaTypeFRR
+                           , SyntaxOpType
                            , ExpType, ExpRhoType, ExpSigmaType )
 import GHC.Tc.Types        ( TcM )
 import GHC.Tc.Types.Origin ( CtOrigin )
@@ -32,13 +33,13 @@ tcSyntaxOp :: CtOrigin
            -> SyntaxExprRn
            -> [SyntaxOpType]           -- ^ shape of syntax operator arguments
            -> ExpType                  -- ^ overall result type
-           -> ([TcSigmaType] -> [Mult] -> TcM a) -- ^ Type check any arguments
+           -> ([TcSigmaTypeFRR] -> [Mult] -> TcM a) -- ^ Type check any arguments
            -> TcM (a, SyntaxExprTc)
 
 tcSyntaxOpGen :: CtOrigin
               -> SyntaxExprRn
               -> [SyntaxOpType]
               -> SyntaxOpType
-              -> ([TcSigmaType] -> [Mult] -> TcM a)
+              -> ([TcSigmaTypeFRR] -> [Mult] -> TcM a)
               -> TcM (a, SyntaxExprTc)
 
diff --git a/compiler/GHC/Tc/Gen/Head.hs b/compiler/GHC/Tc/Gen/Head.hs
index 56a995b3ba..3028f540d9 100644
--- a/compiler/GHC/Tc/Gen/Head.hs
+++ b/compiler/GHC/Tc/Gen/Head.hs
@@ -675,14 +675,17 @@ tcInferOverLit lit@(OverLit { ol_val = val
     --   where fromInteger is gotten by looking up from_name, and
     --   the (3 :: Integer) is returned by mkOverLit
     -- Ditto the string literal "foo" to (fromString ("foo" :: String))
-    do { from_id <- tcLookupId from_name
-       ; (wrap1, from_ty) <- topInstantiate orig (idType from_id)
-
+    do { hs_lit <- mkOverLit val
+       ; from_id <- tcLookupId from_name
+       ; (wrap1, from_ty) <- topInstantiate (LiteralOrigin lit) (idType from_id)
+       ; let
+           thing    = NameThing from_name
+           mb_thing = Just thing
+           herald   = ExpectedFunTyArg thing (HsLit noAnn hs_lit)
        ; (wrap2, sarg_ty, res_ty) <- matchActualFunTySigma herald mb_thing
                                                            (1, []) from_ty
-       ; hs_lit <- mkOverLit val
-       ; co <- unifyType mb_thing (hsLitType hs_lit) (scaledThing sarg_ty)
 
+       ; co <- unifyType mb_thing (hsLitType hs_lit) (scaledThing sarg_ty)
        ; let lit_expr = L (l2l loc) $ mkHsWrapCo co $
                         HsLit noAnn hs_lit
              from_expr = mkHsWrap (wrap2 <.> wrap1) $
@@ -692,12 +695,6 @@ tcInferOverLit lit@(OverLit { ol_val = val
                                              , ol_witness = witness
                                              , ol_type = res_ty } }
        ; return (HsOverLit noAnn lit', res_ty) }
-  where
-    orig     = LiteralOrigin lit
-    mb_thing = Just (NameThing from_name)
-    herald   = sep [ text "The function" <+> quotes (ppr from_name)
-                 , text "is applied to"]
-
 
 {- *********************************************************************
 *                                                                      *
diff --git a/compiler/GHC/Tc/Gen/Match.hs b/compiler/GHC/Tc/Gen/Match.hs
index a4f24dbb1b..d6f3590910 100644
--- a/compiler/GHC/Tc/Gen/Match.hs
+++ b/compiler/GHC/Tc/Gen/Match.hs
@@ -121,8 +121,7 @@ tcMatchesFun fun_id matches exp_ty
   where
     fun_name = idName (unLoc fun_id)
     arity  = matchGroupArity matches
-    herald = text "The equation(s) for"
-             <+> quotes (ppr fun_name) <+> text "have"
+    herald = ExpectedFunTyMatches (NameThing fun_name) matches
     ctxt   = GenSigCtxt  -- Was: FunSigCtxt fun_name True
                          -- But that's wrong for f :: Int -> forall a. blah
     what   = FunRhs { mc_fun = fun_id, mc_fixity = Prefix, mc_strictness = strictness }
@@ -145,10 +144,10 @@ parser guarantees that each equation has exactly one argument.
 -}
 
 tcMatchesCase :: (AnnoBody body) =>
-                TcMatchCtxt body                         -- Case context
-             -> Scaled TcSigmaType                       -- Type of scrutinee
-             -> MatchGroup GhcRn (LocatedA (body GhcRn)) -- The case alternatives
-             -> ExpRhoType                    -- Type of whole case expressions
+                TcMatchCtxt body      -- ^ Case context
+             -> Scaled TcSigmaTypeFRR -- ^ Type of scrutinee
+             -> MatchGroup GhcRn (LocatedA (body GhcRn)) -- ^ The case alternatives
+             -> ExpRhoType                               -- ^ Type of the whole case expression
              -> TcM (MatchGroup GhcTc (LocatedA (body GhcTc)))
                 -- Translated alternatives
                 -- wrapper goes from MatchGroup's ty to expected ty
@@ -156,7 +155,7 @@ tcMatchesCase :: (AnnoBody body) =>
 tcMatchesCase ctxt (Scaled scrut_mult scrut_ty) matches res_ty
   = tcMatches ctxt [Scaled scrut_mult (mkCheckExpType scrut_ty)] res_ty matches
 
-tcMatchLambda :: SDoc -- see Note [Herald for matchExpectedFunTys] in GHC.Tc.Utils.Unify
+tcMatchLambda :: ExpectedFunTyOrigin -- see Note [Herald for matchExpectedFunTys] in GHC.Tc.Utils.Unify
               -> TcMatchCtxt HsExpr
               -> MatchGroup GhcRn (LHsExpr GhcRn)
               -> ExpRhoType
@@ -213,8 +212,8 @@ type AnnoBody body
 
 -- | Type-check a MatchGroup.
 tcMatches :: (AnnoBody body ) => TcMatchCtxt body
-          -> [Scaled ExpSigmaType]      -- Expected pattern types
-          -> ExpRhoType          -- Expected result-type of the Match.
+          -> [Scaled ExpSigmaTypeFRR] -- ^ Expected pattern types.
+          -> ExpRhoType               -- ^ Expected result-type of the Match.
           -> MatchGroup GhcRn (LocatedA (body GhcRn))
           -> TcM (MatchGroup GhcTc (LocatedA (body GhcTc)))
 
@@ -227,10 +226,6 @@ 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
-       ; zipWithM_
-            (\ i (Scaled _ pat_ty) ->
-                 hasFixedRuntimeRep_MustBeRefl (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 }) }
@@ -241,10 +236,6 @@ 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
-       ; zipWithM_
-            (\ i (Scaled _ pat_ty) ->
-                hasFixedRuntimeRep_MustBeRefl (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 }) }
diff --git a/compiler/GHC/Tc/Gen/Pat.hs b/compiler/GHC/Tc/Gen/Pat.hs
index 7f31b4edb3..fb629e8826 100644
--- a/compiler/GHC/Tc/Gen/Pat.hs
+++ b/compiler/GHC/Tc/Gen/Pat.hs
@@ -35,7 +35,6 @@ 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
@@ -44,6 +43,7 @@ import GHC.Types.Var
 import GHC.Types.Name
 import GHC.Types.Name.Reader
 import GHC.Core.Multiplicity
+import GHC.Tc.Utils.Concrete ( hasFixedRuntimeRep_MustBeRefl )
 import GHC.Tc.Utils.Env
 import GHC.Tc.Utils.TcMType
 import GHC.Tc.Validity( arityErr )
@@ -83,7 +83,7 @@ import GHC.Data.List.SetOps ( getNth )
 
 tcLetPat :: (Name -> Maybe TcId)
          -> LetBndrSpec
-         -> LPat GhcRn -> Scaled ExpSigmaType
+         -> LPat GhcRn -> Scaled ExpSigmaTypeFRR
          -> TcM a
          -> TcM (LPat GhcTc, a)
 tcLetPat sig_fn no_gen pat pat_ty thing_inside
@@ -99,9 +99,9 @@ tcLetPat sig_fn no_gen pat pat_ty thing_inside
 
 -----------------
 tcPats :: HsMatchContext GhcTc
-       -> [LPat GhcRn]            -- Patterns,
-       -> [Scaled ExpSigmaType]         --   and their types
-       -> TcM a                  --   and the checker for the body
+       -> [LPat GhcRn]             -- ^ atterns
+       -> [Scaled ExpSigmaTypeFRR] -- ^ types of the patterns
+       -> TcM a                    -- ^ checker for the body
        -> TcM ([LPat GhcTc], a)
 
 -- This is the externally-callable wrapper function
@@ -130,7 +130,7 @@ tcInferPat ctxt pat thing_inside
     penv = PE { pe_lazy = False, pe_ctxt = LamPat ctxt, pe_orig = PatOrigin }
 
 tcCheckPat :: HsMatchContext GhcTc
-           -> LPat GhcRn -> Scaled TcSigmaType
+           -> LPat GhcRn -> Scaled TcSigmaTypeFRR
            -> TcM a                     -- Checker for body
            -> TcM (LPat GhcTc, a)
 tcCheckPat ctxt = tcCheckPat_O ctxt PatOrigin
@@ -138,7 +138,7 @@ tcCheckPat ctxt = tcCheckPat_O ctxt PatOrigin
 -- | A variant of 'tcPat' that takes a custom origin
 tcCheckPat_O :: HsMatchContext GhcTc
              -> CtOrigin              -- ^ origin to use if the type needs inst'ing
-             -> LPat GhcRn -> Scaled TcSigmaType
+             -> LPat GhcRn -> Scaled TcSigmaTypeFRR
              -> TcM a                 -- Checker for body
              -> TcM (LPat GhcTc, a)
 tcCheckPat_O ctxt orig pat (Scaled pat_mult pat_ty) thing_inside
@@ -204,7 +204,7 @@ inPatBind (PE { pe_ctxt = LamPat {} }) = False
 *                                                                      *
 ********************************************************************* -}
 
-tcPatBndr :: PatEnv -> Name -> Scaled ExpSigmaType -> TcM (HsWrapper, TcId)
+tcPatBndr :: PatEnv -> Name -> Scaled ExpSigmaTypeFRR -> TcM (HsWrapper, TcId)
 -- (coi, xp) = tcPatBndr penv x pat_ty
 -- Then coi : pat_ty ~ typeof(xp)
 --
@@ -331,7 +331,7 @@ tcMultiple tc_pat penv args thing_inside
         ; loop penv args }
 
 --------------------
-tc_lpat :: Scaled ExpSigmaType
+tc_lpat :: Scaled ExpSigmaTypeFRR
         -> Checker (LPat GhcRn) (LPat GhcTc)
 tc_lpat pat_ty penv (L span pat) thing_inside
   = setSrcSpanA span $
@@ -339,7 +339,7 @@ tc_lpat pat_ty penv (L span pat) thing_inside
                                           thing_inside
         ; return (L span pat', res) }
 
-tc_lpats :: [Scaled ExpSigmaType]
+tc_lpats :: [Scaled ExpSigmaTypeFRR]
          -> Checker [LPat GhcRn] [LPat GhcTc]
 tc_lpats tys penv pats
   = assertPpr (equalLength pats tys) (ppr pats $$ ppr tys) $
@@ -352,7 +352,7 @@ tc_lpats tys penv pats
 checkManyPattern :: Scaled a -> TcM HsWrapper
 checkManyPattern pat_ty = tcSubMult NonLinearPatternOrigin Many (scaledMult pat_ty)
 
-tc_pat  :: Scaled ExpSigmaType
+tc_pat  :: Scaled ExpSigmaTypeFRR
         -- ^ Fully refined result type
         -> Checker (Pat GhcRn) (Pat GhcTc)
         -- ^ Translated pattern
@@ -430,7 +430,7 @@ tc_pat pat_ty penv ps_pat thing_inside = case ps_pat of
                -- Note [View patterns and polymorphism]
 
          -- Expression must be a function
-        ; let herald = text "A view pattern expression expects"
+        ; let herald = ExpectedFunTyViewPat $ unLoc expr
         ; (expr_wrap1, Scaled _mult inf_arg_ty, inf_res_sigma)
             <- matchActualFunTySigma herald (Just . HsExprRnThing $ unLoc expr) (1,[]) expr_ty
                -- See Note [View patterns and polymorphism]
@@ -445,10 +445,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
-        ; 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_wrap2' = mkWpFun expr_wrap2 idHsWrapper
+                              (Scaled w pat_ty) inf_res_sigma
+          -- expr_wrap2' :: (inf_arg_ty -> inf_res_sigma) "->"
+          --                (pat_ty -> inf_res_sigma)
+          -- NB: pat_ty comes from matchActualFunTySigma, so it has a
+          -- fixed RuntimeRep, as needed to call mkWpFun.
         ; let
               expr_wrap = expr_wrap2' <.> expr_wrap1 <.> mult_wrap
 
@@ -855,7 +857,7 @@ same name, leading to shadowing.
 --       with scrutinee of type (T ty)
 
 tcConPat :: PatEnv -> LocatedN Name
-         -> Scaled ExpSigmaType    -- Type of the pattern
+         -> Scaled ExpSigmaTypeFRR    -- Type of the pattern
          -> HsConPatDetails GhcRn -> TcM a
          -> TcM (Pat GhcTc, a)
 tcConPat penv con_lname@(L _ con_name) pat_ty arg_pats thing_inside
@@ -881,7 +883,7 @@ warnMonoLocalBinds
        }
 
 tcDataConPat :: PatEnv -> LocatedN Name -> DataCon
-             -> Scaled ExpSigmaType        -- Type of the pattern
+             -> Scaled ExpSigmaTypeFRR        -- Type of the pattern
              -> HsConPatDetails GhcRn -> TcM a
              -> TcM (Pat GhcTc, a)
 tcDataConPat penv (L con_span con_name) data_con pat_ty_scaled
@@ -925,15 +927,28 @@ tcDataConPat penv (L con_span con_name) data_con pat_ty_scaled
               pat_mult = scaledMult pat_ty_scaled
               arg_tys_scaled = map (scaleScaled pat_mult) arg_tys'
 
-        ; traceTc "tcConPat" (vcat [ ppr con_name
-                                   , pprTyVars univ_tvs
-                                   , pprTyVars ex_tvs
-                                   , ppr eq_spec
-                                   , ppr theta
-                                   , pprTyVars ex_tvs'
-                                   , ppr ctxt_res_tys
-                                   , ppr arg_tys'
-                                   , ppr arg_pats ])
+        -- This check is necessary to uphold the invariant that 'tcConArgs'
+        -- is given argument types with a fixed runtime representation.
+        -- See test case T20363.
+        ; zipWithM_
+            ( \ i arg_sty ->
+              hasFixedRuntimeRep_MustBeRefl
+                (FRRDataConArg Pattern data_con i)
+                (scaledThing arg_sty)
+            )
+            [1..]
+            arg_tys'
+
+        ; traceTc "tcConPat" (vcat [ text "con_name:" <+> ppr con_name
+                                   , text "univ_tvs:" <+> pprTyVars univ_tvs
+                                   , text "ex_tvs:" <+> pprTyVars ex_tvs
+                                   , text "eq_spec:" <+> ppr eq_spec
+                                   , text "theta:" <+> ppr theta
+                                   , text "ex_tvs':" <+> pprTyVars ex_tvs'
+                                   , text "ctxt_res_tys:" <+> ppr ctxt_res_tys
+                                   , text "pat_ty:" <+> ppr pat_ty
+                                   , text "arg_tys':" <+> ppr arg_tys'
+                                   , text "arg_pats" <+> ppr arg_pats ])
         ; if null ex_tvs && null eq_spec && null theta
           then do { -- The common case; no class bindings etc
                     -- (see Note [Arrows and patterns])
@@ -979,7 +994,7 @@ tcDataConPat penv (L con_span con_name) data_con pat_ty_scaled
         } }
 
 tcPatSynPat :: PatEnv -> LocatedN Name -> PatSyn
-            -> Scaled ExpSigmaType         -- Type of the pattern
+            -> Scaled ExpSigmaType         -- ^ Type of the pattern
             -> HsConPatDetails GhcRn -> TcM a
             -> TcM (Pat GhcTc, a)
 tcPatSynPat penv (L con_span con_name) pat_syn pat_ty arg_pats thing_inside
@@ -1028,6 +1043,18 @@ tcPatSynPat penv (L con_span con_name) pat_syn pat_ty arg_pats thing_inside
                       -- see Note [Call-stack tracing of pattern synonyms]
         ; traceTc "instCall" (ppr req_wrap)
 
+          -- Pattern synonyms can never have representation-polymorphic argument types,
+          -- as checked in 'GHC.Tc.Gen.Sig.tcPatSynSig' (see use of 'FixedRuntimeRepPatSynSigArg').
+          -- (If you want to lift this restriction, use 'hasFixedRuntimeRep' here, to match
+          -- 'tcDataConPat'.)
+        ; let
+            bad_arg_tys :: [(Int, Scaled Type)]
+            bad_arg_tys = filter (\ (_, Scaled _ arg_ty) -> typeLevity_maybe arg_ty == Nothing)
+                        $ zip [0..] arg_tys'
+        ; massertPpr (null bad_arg_tys) $
+            vcat [ text "tcPatSynPat: pattern arguments do not have a fixed RuntimeRep"
+                 , text "bad_arg_tys:" <+> ppr bad_arg_tys ]
+
         ; traceTc "checkConstraints {" Outputable.empty
         ; (ev_binds, (arg_pats', res))
              <- checkConstraints (getSkolemInfo skol_info) ex_tvs' prov_dicts' $
@@ -1073,7 +1100,7 @@ and Note [Solving CallStack constraints] in GHC.Tc.Solver.Types
 ----------------------------
 -- | Convenient wrapper for calling a matchExpectedXXX function
 matchExpectedPatTy :: (TcRhoType -> TcM (TcCoercionN, a))
-                    -> PatEnv -> ExpSigmaType -> TcM (HsWrapper, a)
+                    -> PatEnv -> ExpSigmaTypeFRR -> TcM (HsWrapper, a)
 -- See Note [Matching polytyped patterns]
 -- Returns a wrapper : pat_ty ~R inner_ty
 matchExpectedPatTy inner_match (PE { pe_orig = orig }) pat_ty
@@ -1085,13 +1112,14 @@ matchExpectedPatTy inner_match (PE { pe_orig = orig }) pat_ty
 
 ----------------------------
 matchExpectedConTy :: PatEnv
-                   -> TyCon      -- The TyCon that this data
-                                 -- constructor actually returns
-                                 -- In the case of a data family this is
-                                 -- the /representation/ TyCon
-                   -> Scaled ExpSigmaType  -- The type of the pattern; in the
-                                           -- case of a data family this would
-                                           -- mention the /family/ TyCon
+                   -> TyCon
+                       -- ^ The TyCon that this data constructor actually returns.
+                       -- In the case of a data family, this is
+                       -- the /representation/ TyCon.
+                   -> Scaled ExpSigmaTypeFRR
+                       -- ^ The type of the pattern.
+                       -- In the case of a data family, this would
+                       -- mention the /family/ TyCon
                    -> TcM (HsWrapper, [TcSigmaType])
 -- See Note [Matching constructor patterns]
 -- Returns a wrapper : pat_ty "->" T ty1 ... tyn
@@ -1212,7 +1240,7 @@ Wrinkles:
 -}
 
 tcConArgs :: ConLike
-          -> [Scaled TcSigmaType]
+          -> [Scaled TcSigmaTypeFRR]
           -> TCvSubst            -- Instantiating substitution for constructor type
           -> Checker (HsConPatDetails GhcRn) (HsConPatDetails GhcTc)
 tcConArgs con_like arg_tys tenv penv con_args thing_inside = case con_args of
diff --git a/compiler/GHC/Tc/Module.hs b/compiler/GHC/Tc/Module.hs
index aa4be8e76e..dca5bce99e 100644
--- a/compiler/GHC/Tc/Module.hs
+++ b/compiler/GHC/Tc/Module.hs
@@ -2167,7 +2167,7 @@ tcRnStmt hsc_env rdr_stmt
 
         -- None of the Ids should be of unboxed type, because we
         -- cast them all to HValues in the end!
-    mapM_ bad_unboxed (filter (isUnliftedType . idType) zonked_ids) ;
+    mapM_ bad_unboxed (filter (mightBeUnliftedType . idType) zonked_ids) ;
 
     traceTc "tcs 1" empty ;
     this_mod <- getModule ;
diff --git a/compiler/GHC/Tc/Solver/Canonical.hs b/compiler/GHC/Tc/Solver/Canonical.hs
index e1baaba7c0..222a665eaa 100644
--- a/compiler/GHC/Tc/Solver/Canonical.hs
+++ b/compiler/GHC/Tc/Solver/Canonical.hs
@@ -544,6 +544,8 @@ mk_strict_superclasses rec_clss (CtGiven { ctev_evar = evar, ctev_loc = loc })
 
     do_one_given sel_id
       | isUnliftedType sc_pred
+         -- NB: class superclasses are never representation-polymorphic,
+         -- so isUnliftedType is OK here.
       , not (null tvs && null theta)
       = -- See Note [Equality superclasses in quantified constraints]
         return []
diff --git a/compiler/GHC/Tc/TyCl.hs b/compiler/GHC/Tc/TyCl.hs
index 3c2ba8a9b3..302f93e691 100644
--- a/compiler/GHC/Tc/TyCl.hs
+++ b/compiler/GHC/Tc/TyCl.hs
@@ -4515,7 +4515,7 @@ checkNewDataCon con
 
         ; unlifted_newtypes <- xoptM LangExt.UnliftedNewtypes
         ; let allowedArgType =
-                unlifted_newtypes || isLiftedType_maybe (scaledThing arg_ty1) == Just True
+                unlifted_newtypes || typeLevity_maybe (scaledThing arg_ty1) == Just Lifted
         ; checkTc allowedArgType $ TcRnUnknownMessage $ mkPlainError noHints $ vcat
           [ text "A newtype cannot have an unlifted argument type"
           , text "Perhaps you intended to use UnliftedNewtypes"
diff --git a/compiler/GHC/Tc/TyCl/Build.hs b/compiler/GHC/Tc/TyCl/Build.hs
index 8c855dacbc..9f508491dc 100644
--- a/compiler/GHC/Tc/TyCl/Build.hs
+++ b/compiler/GHC/Tc/TyCl/Build.hs
@@ -211,6 +211,8 @@ buildPatSyn :: Name -> Bool
             -> ([InvisTVBinder], ThetaType) -- ^ Univ and req
             -> ([InvisTVBinder], ThetaType) -- ^ Ex and prov
             -> [Type]                       -- ^ Argument types
+                                            -- These must have a fixed RuntimeRep as per
+                                            -- Note [Fixed RuntimeRep] in GHC.Tc.Utils.Concrete.
             -> Type                         -- ^ Result type
             -> [FieldLabel]                 -- ^ Field labels for
                                             --   a record pattern synonym
diff --git a/compiler/GHC/Tc/TyCl/PatSyn.hs b/compiler/GHC/Tc/TyCl/PatSyn.hs
index 8091869187..6e7316d544 100644
--- a/compiler/GHC/Tc/TyCl/PatSyn.hs
+++ b/compiler/GHC/Tc/TyCl/PatSyn.hs
@@ -669,7 +669,10 @@ tc_patsyn_finish :: LocatedN Name   -- ^ PatSyn Name
                  -> TcPragEnv
                  -> ([TcInvisTVBinder], [PredType], TcEvBinds, [EvVar])
                  -> ([TcInvisTVBinder], [TcType], [PredType], [EvTerm])
-                 -> ([LHsExpr GhcTc], [TcType])  -- ^ Pattern arguments and types
+                 -> ([LHsExpr GhcTc], [TcType])
+                   -- ^ Pattern arguments and types.
+                   -- These must have a fixed RuntimeRep as per
+                   -- Note [Fixed RuntimeRep] in GHC.Tc.Utils.Concrete.
                  -> TcType            -- ^ Pattern type
                  -> [FieldLabel]      -- ^ Selector names
                  -- ^ Whether fields, empty if not record PatSyn
@@ -869,6 +872,8 @@ mkPatSynBuilder dir (L _ name)
   = do { builder_name <- newImplicitBinder name mkBuilderOcc
        ; let theta          = req_theta ++ prov_theta
              need_dummy_arg = isUnliftedType pat_ty && null arg_tys && null theta
+                              -- NB: pattern arguments cannot be representation-polymorphic,
+                              -- as checked in 'tcPatSynSig'. So 'isUnliftedType' is OK here.
              builder_sigma  = add_void need_dummy_arg $
                               mkInvisForAllTys univ_bndrs $
                               mkInvisForAllTys ex_bndrs $
diff --git a/compiler/GHC/Tc/Types/Evidence.hs b/compiler/GHC/Tc/Types/Evidence.hs
index cf083b3c6f..74240b1f94 100644
--- a/compiler/GHC/Tc/Types/Evidence.hs
+++ b/compiler/GHC/Tc/Types/Evidence.hs
@@ -8,7 +8,7 @@ module GHC.Tc.Types.Evidence (
   -- * HsWrapper
   HsWrapper(..),
   (<.>), mkWpTyApps, mkWpEvApps, mkWpEvVarApps, mkWpTyLams,
-  mkWpLams, mkWpLet, mkWpCastN, mkWpCastR, collectHsWrapBinders,
+  mkWpLams, mkWpLet, mkWpFun, mkWpCastN, mkWpCastR, collectHsWrapBinders,
   idHsWrapper, isIdHsWrapper,
   pprHsWrapper, hsWrapDictBinders,
 
@@ -281,6 +281,24 @@ WpHole <.> c = c
 c <.> WpHole = c
 c1 <.> c2    = c1 `WpCompose` c2
 
+-- | Smart constructor to create a 'WpFun' 'HsWrapper'.
+--
+-- PRECONDITION: the "from" type of the first wrapper must have a
+-- fixed RuntimeRep (see Note [Fixed RuntimeRep] in GHC.Tc.Utils.Concrete).
+mkWpFun :: HsWrapper -> HsWrapper
+        -> Scaled TcType -- ^ the "from" type of the first wrapper
+                         -- MUST have a fixed RuntimeRep
+        -> TcType        -- ^ either type of the second wrapper (used only when the
+                         -- second wrapper is the identity)
+        -> HsWrapper
+  -- NB: can't check that the argument type has a fixed RuntimeRep with an assertion,
+  -- as we will only be able to know that after typechecking.
+mkWpFun WpHole       WpHole       _             _  = WpHole
+mkWpFun WpHole       (WpCast co2) (Scaled w t1) _  = WpCast (mkTcFunCo Representational (multToCo w) (mkTcRepReflCo t1) co2)
+mkWpFun (WpCast co1) WpHole       (Scaled w _)  t2 = WpCast (mkTcFunCo Representational (multToCo w) (mkTcSymCo co1) (mkTcRepReflCo t2))
+mkWpFun (WpCast co1) (WpCast co2) (Scaled w _)  _  = WpCast (mkTcFunCo Representational (multToCo w) (mkTcSymCo co1) co2)
+mkWpFun co1          co2          t1            _  = WpFun co1 co2 t1
+
 mkWpCastR :: TcCoercionR -> HsWrapper
 mkWpCastR co
   | isTcReflCo co = WpHole
diff --git a/compiler/GHC/Tc/Types/Origin.hs b/compiler/GHC/Tc/Types/Origin.hs
index 38345d82aa..ebbf802026 100644
--- a/compiler/GHC/Tc/Types/Origin.hs
+++ b/compiler/GHC/Tc/Types/Origin.hs
@@ -1,6 +1,7 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE GADTs #-}
+{-# LANGUAGE PolyKinds #-}
 
 {-# OPTIONS_GHC -Wno-incomplete-record-updates #-}
 {-# OPTIONS_GHC -Wno-incomplete-uni-patterns   #-}
@@ -8,16 +9,16 @@
 -- | Describes the provenance of types as they flow through the type-checker.
 -- The datatypes here are mainly used for error message generation.
 module GHC.Tc.Types.Origin (
-  -- UserTypeCtxt
+  -- * UserTypeCtxt
   UserTypeCtxt(..), pprUserTypeCtxt, isSigMaybe,
   ReportRedundantConstraints(..), reportRedundantConstraints,
   redundantConstraintsSpan,
 
-  -- SkolemInfo
+  -- * SkolemInfo
   SkolemInfo(..), SkolemInfoAnon(..), mkSkolemInfo, getSkolemInfo, pprSigSkolInfo, pprSkolInfo,
   unkSkol, unkSkolAnon,
 
-  -- CtOrigin
+  -- * CtOrigin
   CtOrigin(..), exprCtOrigin, lexprCtOrigin, matchesCtOrigin, grhssCtOrigin,
   isVisibleOrigin, toInvisibleOrigin,
   pprCtOrigin, isGivenOrigin, isWantedWantedFunDepOrigin,
@@ -25,16 +26,16 @@ module GHC.Tc.Types.Origin (
 
   TypedThing(..), TyVarBndrs(..),
 
-  -- CtOrigin and CallStack
+  -- * CtOrigin and CallStack
   isPushCallStackOrigin, callStackOriginFS,
-  -- FixedRuntimeRep origin
+  -- * FixedRuntimeRep origin
   FRROrigin(..), pprFRROrigin,
   StmtOrigin(..),
 
-  -- Arrow command origin
+  -- * Arrow command origin
   FRRArrowOrigin(..), pprFRRArrowOrigin,
-  -- HsWrapper WpFun origin
-  WpFunOrigin(..), pprWpFunOrigin,
+  -- * ExpectedFunTy origin
+  ExpectedFunTyOrigin(..), pprExpectedFunTyOrigin, pprExpectedFunTyHerald,
 
   ) where
 
@@ -993,24 +994,21 @@ data FRROrigin
   -- Test cases: LevPolyLet, RepPolyPatBind.
   | FRRBinder !Name
 
-  -- | The type of a pattern in a match group must have a fixed runtime representation.
+  -- | The type of the scrutinee in a case statement must have a
+  -- fixed runtime representation.
   --
-  -- This rules out:
-  --   - individual patterns which don't have a fixed runtime representation,
-  --   - a representation-polymorphic empty case statement,
-  --   - representation-polymorphic GADT pattern matches
-  --     in which individual pattern types have a fixed runtime representation.
-  --
-  -- Test cases: RepPolyRecordPattern, RepPolyUnboxedPatterns,
-  --             RepPolyBinder, RepPolyWildcardPattern, RepPolyMatch,
-  --             RepPolyNPlusK, RepPolyPatBind, T20426.
-  | FRRMatch !(HsMatchContext GhcTc) !Int
+  -- Test cases: RepPolyCase{1,2}.
+  | FRRCase
 
   -- | An instantiation of a newtype/data constructor in which
-  -- one of the remaining arguments types does not have a fixed runtime representation.
+  -- an argument type does not have a fixed runtime representation.
+  --
+  -- The argument can either be an expression or a pattern.
   --
-  -- Test case: UnliftedNewtypesLevityBinder.
-  | FRRDataConArg !DataCon !Int
+  -- Test cases:
+  --  Expression: UnliftedNewtypesLevityBinder.
+  --     Pattern: T20363.
+  | FRRDataConArg !ExprOrPat !DataCon !Int
 
   -- | An instantiation of an 'Id' with no binding (e.g. `coerce`, `unsafeCoerce#`)
   -- in which one of the remaining arguments types does not have a fixed runtime representation.
@@ -1061,10 +1059,14 @@ data FRROrigin
   -- See 'FRRArrowOrigin' for more details.
   | FRRArrow !FRRArrowOrigin
 
-  -- | A representation-polymorphic check arising from an 'HsWrapper'.
+  -- | A representation-polymorphic check arising from a call
+  -- to 'matchExpectedFunTys' or 'matchActualFunTySigma'.
   --
-  -- See 'WpFunOrigin' for more details.
-  | FRRWpFun !WpFunOrigin
+  -- See 'ExpectedFunTyOrigin' for more details.
+  | FRRExpectedFunTy
+      !ExpectedFunTyOrigin
+      !Int
+        -- ^ argument position (0-indexed)
 
 -- | Print the context for a @FixedRuntimeRep@ representation-polymorphism check.
 --
@@ -1072,25 +1074,28 @@ data FRROrigin
 -- which is not fixed. That information is added by 'GHC.Tc.Errors.mkFRRErr'.
 pprFRROrigin :: FRROrigin -> SDoc
 pprFRROrigin (FRRApp arg)
-  = vcat [ text "The function argument"
-         , nest 2 $ quotes (ppr arg) ]
+  = sep [ text "The function argument"
+        , nest 2 $ quotes (ppr arg) ]
 pprFRROrigin (FRRRecordUpdate lbl _arg)
-  = hsep [ text "The record update at field"
-         , quotes (ppr lbl) ]
+  = sep [ text "The record update at field"
+        , quotes (ppr lbl) ]
 pprFRROrigin (FRRBinder binder)
-  = hsep [ text "The binder"
-         , quotes (ppr binder) ]
-pprFRROrigin (FRRMatch matchCtxt i)
-  = text "The" <+> speakNth i <+> text "pattern in the" <+> pprMatchContextNoun matchCtxt
-pprFRROrigin (FRRDataConArg con i)
+  = sep [ text "The binder"
+        , quotes (ppr binder) ]
+pprFRROrigin FRRCase
+  = text "The scrutinee of the case statement"
+pprFRROrigin (FRRDataConArg expr_or_pat con i)
   = text "The" <+> what
   where
-    what :: SDoc
+    arg, what :: SDoc
+    arg = case expr_or_pat of
+      Expression -> text "argument"
+      Pattern    -> text "pattern"
     what
       | isNewDataCon con
-      = text "newtype constructor argument"
+      = text "newtype constructor" <+> arg
       | otherwise
-      = text "data constructor argument in" <+> speakNth i <+> text "position"
+      = text "data constructor" <+> arg <+> text "in" <+> speakNth i <+> text "position"
 pprFRROrigin (FRRNoBindingResArg fn i)
   = vcat [ text "Unsaturated use of a representation-polymorphic primitive function."
          , text "The" <+> speakNth i <+> text "argument of" <+> quotes (ppr $ getName fn) ]
@@ -1110,12 +1115,11 @@ pprFRROrigin (FRRBindStmt stmtOrig)
   = vcat [ text "The first argument to (>>=)" <> comma
          , text "arising from the" <+> ppr stmtOrig <> comma ]
 pprFRROrigin FRRBindStmtGuard
-  = hsep [ text "The body of the bind statement" ]
+  = sep [ text "The body of the bind statement" ]
 pprFRROrigin (FRRArrow arrowOrig)
   = pprFRRArrowOrigin arrowOrig
-pprFRROrigin (FRRWpFun wpFunOrig)
-  = hsep [ text "The function argument"
-         , pprWpFunOrigin wpFunOrig ]
+pprFRROrigin (FRRExpectedFunTy funTyOrig zero_indexed_arg)
+  = pprExpectedFunTyOrigin funTyOrig (zero_indexed_arg + 1)
 
 instance Outputable FRROrigin where
   ppr = pprFRROrigin
@@ -1166,6 +1170,15 @@ data FRRArrowOrigin
   -- Test cases: none.
   | ArrowCmdLam !Int
 
+  -- | The scrutinee type in an arrow command case or lambda-case
+  -- statement does not have a fixed runtime representation.
+  --
+  -- Test cases: none.
+  | ArrowCmdCase { isCmdLamCase :: Bool
+                    -- ^ Whether this is a lambda-case (True)
+                    -- or a normal case (False)
+                 }
+
   -- | The overall type of an arrow proc expression does not have
   -- a fixed runtime representation.
   --
@@ -1181,12 +1194,19 @@ pprFRRArrowOrigin (ArrowCmdApp fun arg)
          , text "to"
          , nest 2 (quotes (ppr arg)) ]
 pprFRRArrowOrigin (ArrowCmdArrApp fun arg ho_app)
-  = vcat [ text "The function un the" <+> pprHsArrType ho_app <+> text "of"
+  = vcat [ text "The function in the" <+> pprHsArrType ho_app <+> text "of"
          , nest 2 (quotes (ppr fun))
          , text "to"
          , nest 2 (quotes (ppr arg)) ]
 pprFRRArrowOrigin (ArrowCmdLam i)
   = vcat [ text "The" <+> speakNth i <+> text "pattern of the arrow command abstraction" ]
+pprFRRArrowOrigin (ArrowCmdCase { isCmdLamCase = is_lam_case })
+  = text "The scrutinee of the arrow" <+> what <+> text "command"
+  where
+    what :: SDoc
+    what = if is_lam_case
+           then text "lambda-case"
+           else text "case"
 pprFRRArrowOrigin (ArrowFun fun)
   = vcat [ text "The return type of the arrow function"
          , nest 2 (quotes (ppr fun)) ]
@@ -1196,33 +1216,87 @@ instance Outputable FRRArrowOrigin where
 
 {- *********************************************************************
 *                                                                      *
-              FixedRuntimeRep: HsWrapper WpFun origin
+              FixedRuntimeRep: ExpectedFunTy origin
 *                                                                      *
 ********************************************************************* -}
 
--- | While typechecking a 'WpFun' 'HsWrapper', in which context
--- did a representation polymorphism check arise?
+-- | In what context are we calling 'matchExpectedFunTys'
+-- or 'matchActualFunTySigma'?
 --
--- See 'FRROrigin' for more general origins of representation polymorphism checks.
-data WpFunOrigin
-  = WpFunSyntaxOp !CtOrigin
-  | WpFunViewPat  !(HsExpr GhcRn)
-  | WpFunFunTy    !Type
-  | WpFunFunExpTy !ExpType
-
-pprWpFunOrigin :: WpFunOrigin -> SDoc
-pprWpFunOrigin (WpFunSyntaxOp orig)
-  = vcat [ text "of a rebindable syntax operator arising from"
-         , nest 2 (ppr orig) ]
-pprWpFunOrigin (WpFunViewPat expr)
-  = vcat [ text "of the view pattern function"
-         , nest 2 (ppr expr) ]
-pprWpFunOrigin (WpFunFunTy fun_ty)
-  = vcat [ text "of the inferred argument type of a function with type"
-         , nest 2 (ppr fun_ty) ]
-pprWpFunOrigin (WpFunFunExpTy fun_ty)
-  = vcat [ text "of the inferred argument type of a function with expected type"
-         , nest 2 (ppr fun_ty) ]
-
-instance Outputable WpFunOrigin where
-  ppr = pprWpFunOrigin
+-- Used for two things:
+--
+--  1. Reporting error messages which explain that a function has been
+--     given an unexpected number of arguments.
+--     Uses 'pprExpectedFunTyHerald'.
+--     See Note [Herald for matchExpectedFunTys] in GHC.Tc.Utils.Unify.
+--
+--  2. Reporting representation-polymorphism errors when a function argument
+--     doesn't have a fixed RuntimeRep as per Note [Fixed RuntimeRep]
+--     in GHC.Tc.Utils.Concrete.
+--     Uses 'pprExpectedFunTyOrigin'.
+--     See 'FRROrigin' for more general origins of representation polymorphism checks.
+data ExpectedFunTyOrigin
+  = ExpectedFunTySyntaxOp !CtOrigin !(HsExpr GhcRn)
+  | ExpectedFunTyViewPat  !(HsExpr GhcRn)
+  | forall (p :: Pass)
+      . (OutputableBndrId p)
+      => ExpectedFunTyArg
+          !TypedThing
+            -- ^ function
+          !(HsExpr (GhcPass p))
+            -- ^ argument
+  | ExpectedFunTyMatches  !TypedThing !(MatchGroup GhcRn (LHsExpr GhcRn))
+  | ExpectedFunTyLam      !(MatchGroup GhcRn (LHsExpr GhcRn))
+  | ExpectedFunTyLamCase  !(HsExpr GhcRn)
+
+pprExpectedFunTyOrigin :: ExpectedFunTyOrigin
+                       -> Int -- ^ argument position (starting at 1)
+                       -> SDoc
+pprExpectedFunTyOrigin funTy_origin i =
+  case funTy_origin of
+    ExpectedFunTySyntaxOp orig op ->
+      vcat [ sep [ the_arg_of
+                 , text "the rebindable syntax operator"
+                 , quotes (ppr op) ]
+           , nest 2 (ppr orig) ]
+    ExpectedFunTyViewPat expr ->
+      vcat [ the_arg_of <+> text "the view pattern"
+           , nest 2 (ppr expr) ]
+    ExpectedFunTyArg fun arg ->
+      sep [ text "The argument"
+          , quotes (ppr arg)
+          , text "of"
+          , quotes (ppr fun) ]
+    ExpectedFunTyMatches fun (MG { mg_alts = L _ alts })
+      | null alts
+      -> the_arg_of <+> quotes (ppr fun)
+      | otherwise
+      -> text "The" <+> speakNth i <+> text "pattern in the equation" <> plural alts
+     <+> text "for" <+> quotes (ppr fun)
+    ExpectedFunTyLam {} ->
+      text "The binder of the lambda expression"
+    ExpectedFunTyLamCase {} ->
+      text "The binder of the lambda-case expression"
+  where
+    the_arg_of :: SDoc
+    the_arg_of = text "The" <+> speakNth i <+> text "argument of"
+
+pprExpectedFunTyHerald :: ExpectedFunTyOrigin -> SDoc
+pprExpectedFunTyHerald (ExpectedFunTySyntaxOp {})
+  = text "This rebindable syntax expects a function with"
+pprExpectedFunTyHerald (ExpectedFunTyViewPat {})
+  = text "A view pattern expression expects"
+pprExpectedFunTyHerald (ExpectedFunTyArg fun _)
+  = sep [ text "The function" <+> quotes (ppr fun)
+        , text "is applied to" ]
+pprExpectedFunTyHerald (ExpectedFunTyMatches fun (MG { mg_alts = L _ alts }))
+  = text "The equation" <> plural alts <+> text "for" <+> quotes (ppr fun) <+> hasOrHave alts
+pprExpectedFunTyHerald (ExpectedFunTyLam match)
+  = sep [ text "The lambda expression" <+>
+                   quotes (pprSetDepth (PartWay 1) $
+                           pprMatches match)
+        -- The pprSetDepth makes the lambda abstraction print briefly
+        , text "has" ]
+pprExpectedFunTyHerald (ExpectedFunTyLamCase expr)
+  = sep [ text "The function" <+> quotes (ppr expr)
+        , text "requires" ]
diff --git a/compiler/GHC/Tc/Utils/Concrete.hs b/compiler/GHC/Tc/Utils/Concrete.hs
index dbf379479d..22ba6b45e3 100644
--- a/compiler/GHC/Tc/Utils/Concrete.hs
+++ b/compiler/GHC/Tc/Utils/Concrete.hs
@@ -8,8 +8,6 @@ module GHC.Tc.Utils.Concrete
   ( -- * Ensuring that a type has a fixed runtime representation
     hasFixedRuntimeRep
   , hasFixedRuntimeRep_MustBeRefl
-    -- * HsWrapper: checking for representation-polymorphism
-  , mkWpFun
   )
  where
 
@@ -17,17 +15,15 @@ import GHC.Prelude
 
 import GHC.Builtin.Types       ( unliftedTypeKindTyCon, liftedTypeKindTyCon )
 
-import GHC.Core.Coercion       ( Role(..), multToCo )
+import GHC.Core.Coercion       ( Role(..) )
 import GHC.Core.Predicate      ( mkIsReflPrimPred )
-import GHC.Core.TyCo.Rep       ( Type(TyConApp), Scaled(..)
-                               , mkTyVarTy, scaledThing )
+import GHC.Core.TyCo.Rep       ( Type(TyConApp), mkTyVarTy )
 import GHC.Core.Type           ( isConcrete, typeKind )
 
 import GHC.Tc.Types            ( TcM, ThStage(Brack), PendingStuff(TcPending) )
 import GHC.Tc.Types.Constraint ( mkNonCanonical )
-import GHC.Tc.Types.Evidence   ( TcCoercion, HsWrapper(..)
-                               , mkTcFunCo, mkTcRepReflCo, mkTcSymCo )
-import GHC.Tc.Types.Origin     ( CtOrigin(..), FRROrigin(..), WpFunOrigin(..) )
+import GHC.Tc.Types.Evidence   ( TcCoercion )
+import GHC.Tc.Types.Origin     ( CtOrigin(..), FRROrigin(..) )
 import GHC.Tc.Utils.Monad      ( emitSimple, getStage )
 import GHC.Tc.Utils.TcType     ( TcType, TcKind, TcTyVar, MetaInfo(ConcreteTv) )
 import GHC.Tc.Utils.TcMType    ( newAnonMetaTyVar, newWanted, emitWantedEq )
@@ -471,31 +467,3 @@ emitNewConcreteWantedEq_maybe orig ty
   where
     ki :: TcKind
     ki = typeKind ty
-
-{-***********************************************************************
-*                                                                       *
-                 HsWrapper
-*                                                                       *
-***********************************************************************-}
-
--- | Smart constructor to create a 'WpFun' 'HsWrapper'.
---
--- Might emit new Wanted constraints to check for representation polymorphism.
--- This is necessary, as 'WpFun' will desugar to a lambda abstraction,
--- whose binder must have a fixed runtime representation.
-mkWpFun :: HsWrapper -> HsWrapper
-        -> Scaled TcType -- ^ the "from" type of the first wrapper
-        -> TcType        -- ^ either type of the second wrapper (used only when the
-                         -- second wrapper is the identity)
-        -> WpFunOrigin   -- ^ what caused you to want a WpFun?
-        -> TcM HsWrapper
-mkWpFun WpHole       WpHole       _             _  _ = return $ WpHole
-mkWpFun WpHole       (WpCast co2) (Scaled w t1) _  _ = return $ WpCast (mkTcFunCo Representational (multToCo w) (mkTcRepReflCo t1) co2)
-mkWpFun (WpCast co1) WpHole       (Scaled w _)  t2 _ = return $ WpCast (mkTcFunCo Representational (multToCo w) (mkTcSymCo co1) (mkTcRepReflCo t2))
-mkWpFun (WpCast co1) (WpCast co2) (Scaled w _)  _  _ = return $ WpCast (mkTcFunCo Representational (multToCo w) (mkTcSymCo co1) co2)
-mkWpFun co1          co2          t1            _  wpFunOrig
-  = do { hasFixedRuntimeRep_MustBeRefl (FRRWpFun wpFunOrig) (scaledThing t1)
-       ; return $ WpFun co1 co2 t1 }
-
-  -- NB: feel free to move this function elsewhere if you find a better place
-  -- for it (which doesn't create any cyclic imports).
diff --git a/compiler/GHC/Tc/Utils/TcType.hs b/compiler/GHC/Tc/Utils/TcType.hs
index d538638279..090415b16d 100644
--- a/compiler/GHC/Tc/Utils/TcType.hs
+++ b/compiler/GHC/Tc/Utils/TcType.hs
@@ -22,12 +22,16 @@
 module GHC.Tc.Utils.TcType (
   --------------------------------
   -- Types
-  TcType, TcSigmaType, TcRhoType, TcTauType, TcPredType, TcThetaType,
+  TcType, TcSigmaType, TcSigmaTypeFRR,
+  TcRhoType, TcTauType, TcPredType, TcThetaType,
   TcTyVar, TcTyVarSet, TcDTyVarSet, TcTyCoVarSet, TcDTyCoVarSet,
   TcKind, TcCoVar, TcTyCoVar, TcTyVarBinder, TcInvisTVBinder, TcReqTVBinder,
   TcTyCon, MonoTcTyCon, PolyTcTyCon, TcTyConBinder, KnotTied,
 
-  ExpType(..), InferResult(..), ExpSigmaType, ExpRhoType, mkCheckExpType,
+  ExpType(..), InferResult(..),
+  ExpSigmaType, ExpSigmaTypeFRR,
+  ExpRhoType,
+  mkCheckExpType,
 
   SyntaxOpType(..), synKnownType, mkSynFunTys,
 
@@ -354,6 +358,19 @@ type TcTyConBinder = TyConBinder -- With skolem TcTyVars
 type TcPredType     = PredType
 type TcThetaType    = ThetaType
 type TcSigmaType    = TcType
+
+-- | A 'TcSigmaTypeFRR' is a 'TcSigmaType' which has a fixed 'RuntimeRep'
+-- in the sense of Note [Fixed RuntimeRep] in GHC.Tc.Utils.Concrete.
+--
+-- In particular, this means that:
+--
+-- - 'GHC.Types.RepType.typePrimRep' does not panic,
+-- - 'GHC.Core.typeLevity_maybe' does not return 'Nothing'.
+--
+-- This property is important in functions such as 'matchExpectedFunTys', where
+-- we want to provide argument types which have a known runtime representation.
+-- See Note [Return arguments with a fixed RuntimeRep.
+type TcSigmaTypeFRR = TcSigmaType
 type TcRhoType      = TcType  -- Note [TcRhoType]
 type TcTauType      = TcType
 type TcKind         = Kind
@@ -427,8 +444,10 @@ data InferResult
          -- The type that fills in this hole should be a Type,
          -- that is, its kind should be (TYPE rr) for some rr
 
-type ExpSigmaType = ExpType
-type ExpRhoType   = ExpType
+type ExpSigmaType    = ExpType
+-- | Like 'TcSigmaTypeFRR', but for an expected type.
+type ExpSigmaTypeFRR = ExpType
+type ExpRhoType      = ExpType
 
 instance Outputable ExpType where
   ppr (Check ty) = text "Check" <> braces (ppr ty)
diff --git a/compiler/GHC/Tc/Utils/Unify.hs b/compiler/GHC/Tc/Utils/Unify.hs
index 7bd489dc50..c19b592765 100644
--- a/compiler/GHC/Tc/Utils/Unify.hs
+++ b/compiler/GHC/Tc/Utils/Unify.hs
@@ -44,14 +44,13 @@ import GHC.Prelude
 import GHC.Hs
 import GHC.Core.TyCo.Rep
 import GHC.Core.TyCo.Ppr( debugPprType )
-import GHC.Tc.Utils.Concrete ( mkWpFun )
+import GHC.Tc.Utils.Concrete ( hasFixedRuntimeRep_MustBeRefl )
 import GHC.Tc.Utils.Env
 import GHC.Tc.Utils.Instantiate
 import GHC.Tc.Utils.Monad
 import GHC.Tc.Utils.TcMType
 import GHC.Tc.Utils.TcType
 
-
 import GHC.Core.Type
 import GHC.Core.Coercion
 import GHC.Core.Multiplicity
@@ -86,19 +85,29 @@ import qualified Data.Semigroup as S ( (<>) )
 *                                                                      *
 ********************************************************************* -}
 
--- | matchActualFunTySigma does looks for just one function arrow
---   returning an uninstantiated sigma-type
+-- | 'matchActualFunTySigma' looks for just one function arrow,
+-- returning an uninstantiated sigma-type.
+--
+-- Invariant: the returned argument type has a fixed RuntimeRep
+-- as per Note [Fixed RuntimeRep] in GHC.Tc.Utils.Concrete.
+-- See Note [Return arguments with a fixed RuntimeRep].
 matchActualFunTySigma
-  :: SDoc -- See Note [Herald for matchExpectedFunTys]
-  -> Maybe TypedThing             -- The thing with type TcSigmaType
-  -> (Arity, [Scaled TcSigmaType]) -- Total number of value args in the call, and
-                                   -- types of values args to which function has
-                                   --   been applied already (reversed)
-                                   -- Both are used only for error messages)
-  -> TcRhoType                     -- Type to analyse: a TcRhoType
-  -> TcM (HsWrapper, Scaled TcSigmaType, TcSigmaType)
--- The /argument/ is a RhoType
--- The /result/   is an (uninstantiated) SigmaType
+  :: ExpectedFunTyOrigin
+      -- ^ See Note [Herald for matchExpectedFunTys]
+  -> Maybe TypedThing
+      -- ^ The thing with type TcSigmaType
+  -> (Arity, [Scaled TcSigmaType])
+      -- ^ Total number of value args in the call, and
+      -- types of values args to which function has
+      --   been applied already (reversed)
+      -- Both are used only for error messages)
+  -> TcRhoType
+      -- ^ Type to analyse: a TcRhoType
+  -> TcM (HsWrapper, Scaled TcSigmaTypeFRR, TcSigmaType)
+-- This function takes in a type to analyse (a RhoType) and returns
+-- an argument type and a result type (splitting apart a function arrow).
+-- The returned argument type is a SigmaType with a fixed RuntimeRep;
+-- as explained in Note [Return arguments with a fixed RuntimeRep].
 --
 -- See Note [matchActualFunTy error handling] for the first three arguments
 
@@ -118,12 +127,13 @@ matchActualFunTySigma herald mb_thing err_info fun_ty
     -- hide the forall inside a meta-variable
     go :: TcRhoType   -- The type we're processing, perhaps after
                       -- expanding any type synonym
-       -> TcM (HsWrapper, Scaled TcSigmaType, TcSigmaType)
+       -> TcM (HsWrapper, Scaled TcSigmaTypeFRR, TcSigmaType)
     go ty | Just ty' <- tcView ty = go ty'
 
     go (FunTy { ft_af = af, ft_mult = w, ft_arg = arg_ty, ft_res = res_ty })
       = assert (af == VisArg) $
-        return (idHsWrapper, Scaled w arg_ty, res_ty)
+      do { hasFixedRuntimeRep_MustBeRefl (FRRExpectedFunTy herald 0) arg_ty
+         ; return (idHsWrapper, Scaled w arg_ty, res_ty) }
 
     go ty@(TyVarTy tv)
       | isMetaTyVar tv
@@ -156,6 +166,7 @@ matchActualFunTySigma herald mb_thing err_info fun_ty
            ; mult <- newFlexiTyVarTy multiplicityTy
            ; let unif_fun_ty = mkVisFunTy mult arg_ty res_ty
            ; co <- unifyType mb_thing fun_ty unif_fun_ty
+           ; hasFixedRuntimeRep_MustBeRefl (FRRExpectedFunTy herald 0) arg_ty
            ; return (mkWpCastN co, Scaled mult arg_ty, res_ty) }
 
     ------------
@@ -187,14 +198,18 @@ in the error message.
 Ugh!
 -}
 
--- Like 'matchExpectedFunTys', but used when you have an "actual" type,
--- for example in function application
-matchActualFunTysRho :: SDoc   -- See Note [Herald for matchExpectedFunTys]
+-- | Like 'matchExpectedFunTys', but used when you have an "actual" type,
+-- for example in function application.
+--
+-- INVARIANT: the returned arguemnt types all have a fixed RuntimeRep
+-- in the sense of Note [Fixed RuntimeRep] in GHC.Tc.Utils.Concrete.
+-- See Note [Return arguments with a fixed RuntimeRep].
+matchActualFunTysRho :: ExpectedFunTyOrigin -- ^ See Note [Herald for matchExpectedFunTys]
                      -> CtOrigin
-                     -> Maybe TypedThing -- the thing with type TcSigmaType
+                     -> Maybe TypedThing -- ^ the thing with type TcSigmaType
                      -> Arity
                      -> TcSigmaType
-                     -> TcM (HsWrapper, [Scaled TcSigmaType], TcRhoType)
+                     -> TcM (HsWrapper, [Scaled TcSigmaTypeFRR], TcRhoType)
 -- If    matchActualFunTysRho n ty = (wrap, [t1,..,tn], res_ty)
 -- then  wrap : ty ~> (t1 -> ... -> tn -> res_ty)
 --       and res_ty is a RhoType
@@ -216,7 +231,9 @@ matchActualFunTysRho herald ct_orig mb_thing n_val_args_wanted fun_ty
                                                  (n_val_args_wanted, so_far)
                                                  fun_ty
            ; (wrap_res, arg_tys, res_ty)   <- go (n-1) (arg_ty1:so_far) res_ty1
-           ; wrap_fun2 <- mkWpFun idHsWrapper wrap_res arg_ty1 res_ty (WpFunFunTy fun_ty)
+           ; let wrap_fun2 = mkWpFun idHsWrapper wrap_res arg_ty1 res_ty
+           -- NB: arg_ty1 comes from matchActualFunTySigma, so it has
+           -- a fixed RuntimeRep as neede to call mkWpFun.
            ; return (wrap_fun2 <.> wrap_fun1, arg_ty1:arg_tys, res_ty) }
 
 {-
@@ -281,16 +298,73 @@ This function must be written CPS'd because it needs to fill in the
 ExpTypes produced for arguments before it can fill in the ExpType
 passed in.
 
+Note [Return arguments with a fixed RuntimeRep]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The functions
+
+  - matchExpectedFunTys,
+  - matchActualFunTySigma,
+  - matchActualFunTysRho,
+
+peel off argument types, as explained in Note [matchExpectedFunTys].
+It's important that these functions return argument types that have
+a fixed runtime representation, otherwise we would be in violation
+of the representation-polymorphism invariants of
+Note [Representation polymorphism invariants] in GHC.Core.
+
+This is why all these functions have an additional invariant,
+that the argument types they return all have a fixed RuntimeRep,
+in the sense of Note [Fixed RuntimeRep] in GHC.Tc.Utils.Concrete.
+
+Example:
+
+  Suppose we have
+
+    type F :: Type -> RuntimeRep
+    type family F a where { F Int = LiftedRep }
+
+    type Dual :: Type -> Type
+    type family Dual a where
+      Dual a = a -> ()
+
+    f :: forall (a :: TYPE (F Int)). Dual a
+    f = \ x -> ()
+
+  The body of `f` is a lambda abstraction, so we must be able to split off
+  one argument type from its type. This is handled by `matchExpectedFunTys`
+  (see 'GHC.Tc.Gen.Match.tcMatchLambda'). We end up with desugared Core that
+  looks like this:
+
+    f :: forall (a :: TYPE (F Int)). Dual (a |> (TYPE F[0]))
+    f = \ @(a :: TYPE (F Int)) ->
+          (\ (x :: (a |> (TYPE F[0]))) -> ())
+          `cast`
+          (Sub (Sym (Dual[0] <(a |> (TYPE F[0]))>)))
+
+  Two important transformations took place:
+
+    1. We inserted casts around the argument type to ensure that it has
+       a fixed runtime representation, as required by invariant (I1) from
+       Note [Representation polymorphism invariants] in GHC.Core.
+    2. We inserted a cast around the whole lambda to make everything line up
+       with the type signature.
 -}
 
--- Use this one when you have an "expected" type.
+-- | Use this function to split off arguments types when you have an
+-- \"expected\" type.
+--
 -- This function skolemises at each polytype.
+--
+-- Invariant: this function only applies the provided function
+-- to a list of argument types which all have a fixed RuntimeRep
+-- in the sense of Note [Fixed RuntimeRep] in GHC.Tc.Utils.Concrete.
+-- See Note [Return arguments with a fixed RuntimeRep].
 matchExpectedFunTys :: forall a.
-                       SDoc   -- See Note [Herald for matchExpectedFunTys]
+                       ExpectedFunTyOrigin -- See Note [Herald for matchExpectedFunTys]
                     -> UserTypeCtxt
                     -> Arity
                     -> ExpRhoType      -- Skolemised
-                    -> ([Scaled ExpSigmaType] -> ExpRhoType -> TcM a)
+                    -> ([Scaled ExpSigmaTypeFRR] -> ExpRhoType -> TcM a)
                     -> TcM (HsWrapper, a)
 -- If    matchExpectedFunTys n ty = (_, wrap)
 -- then  wrap : (t1 -> ... -> tn -> ty_r) ~> ty,
@@ -320,9 +394,13 @@ matchExpectedFunTys herald ctx arity orig_ty thing_inside
 
     go acc_arg_tys n (FunTy { ft_mult = mult, ft_af = af, ft_arg = arg_ty, ft_res = res_ty })
       = assert (af == VisArg) $
-        do { (wrap_res, result) <- go ((Scaled mult $ mkCheckExpType arg_ty) : acc_arg_tys)
+        do { let arg_pos = length acc_arg_tys -- for error messages only
+           ; hasFixedRuntimeRep_MustBeRefl (FRRExpectedFunTy herald arg_pos) arg_ty
+           ; (wrap_res, result) <- go ((Scaled mult $ mkCheckExpType arg_ty) : acc_arg_tys)
                                       (n-1) res_ty
-           ; fun_wrap <- mkWpFun idHsWrapper wrap_res (Scaled mult arg_ty) res_ty (WpFunFunExpTy orig_ty)
+           ; let fun_wrap = mkWpFun idHsWrapper wrap_res (Scaled mult arg_ty) res_ty
+             -- NB: we are ensuring that arg_ty has a fixed RuntimeRep,
+             -- so we satisfy the precondition that mkWpFun requires.
            ; return ( fun_wrap, result ) }
 
     go acc_arg_tys n ty@(TyVarTy tv)
@@ -351,12 +429,17 @@ matchExpectedFunTys herald ctx arity orig_ty thing_inside
                           defer acc_arg_tys n (mkCheckExpType ty)
 
     ------------
-    defer :: [Scaled ExpSigmaType] -> Arity -> ExpRhoType -> TcM (HsWrapper, a)
+    defer :: [Scaled ExpSigmaTypeFRR] -> Arity -> ExpRhoType -> TcM (HsWrapper, a)
     defer acc_arg_tys n fun_ty
       = do { more_arg_tys <- replicateM n (mkScaled <$> newFlexiTyVarTy multiplicityTy <*> newInferExpType)
            ; res_ty       <- newInferExpType
            ; result       <- thing_inside (reverse acc_arg_tys ++ more_arg_tys) res_ty
            ; more_arg_tys <- mapM (\(Scaled m t) -> Scaled m <$> readExpType t) more_arg_tys
+           ; zipWithM_
+               ( \ i (Scaled _ arg_ty) ->
+                 hasFixedRuntimeRep_MustBeRefl (FRRExpectedFunTy herald i) arg_ty )
+               [0..]
+               more_arg_tys
            ; res_ty       <- readExpType res_ty
            ; let unif_fun_ty = mkVisFunTys more_arg_tys res_ty
            ; wrap <- tcSubType AppOrigin ctx unif_fun_ty fun_ty
@@ -364,7 +447,7 @@ matchExpectedFunTys herald ctx arity orig_ty thing_inside
            ; return (wrap, result) }
 
     ------------
-    mk_ctxt :: [Scaled ExpSigmaType] -> TcType -> TidyEnv -> TcM (TidyEnv, SDoc)
+    mk_ctxt :: [Scaled ExpSigmaTypeFRR] -> TcType -> TidyEnv -> TcM (TidyEnv, SDoc)
     mk_ctxt arg_tys res_ty env
       = mkFunTysMsg env herald arg_tys' res_ty arity
       where
@@ -372,7 +455,9 @@ matchExpectedFunTys herald ctx arity orig_ty thing_inside
                    reverse arg_tys
             -- this is safe b/c we're called from "go"
 
-mkFunTysMsg :: TidyEnv -> SDoc -> [Scaled TcType] -> TcType -> Arity
+mkFunTysMsg :: TidyEnv
+            -> ExpectedFunTyOrigin
+            -> [Scaled TcType] -> TcType -> Arity
             -> TcM (TidyEnv, SDoc)
 mkFunTysMsg env herald arg_tys res_ty n_val_args_in_call
   = do { (env', fun_rho) <- zonkTidyTcType env $
@@ -391,7 +476,8 @@ mkFunTysMsg env herald arg_tys res_ty n_val_args_in_call
 
        ; return (env', msg) }
  where
-  full_herald = herald <+> speakNOf n_val_args_in_call (text "value argument")
+  full_herald = pprExpectedFunTyHerald herald
+            <+> speakNOf n_val_args_in_call (text "value argument")
 
 ----------------------
 matchExpectedListTy :: TcRhoType -> TcM (TcCoercionN, TcRhoType)