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
-------------------------

6 files changed, 634 insertions, 95 deletions

diff --git a/compiler/GHC/Tc/Utils/Concrete.hs b/compiler/GHC/Tc/Utils/Concrete.hs
new file mode 100644
index 0000000000..0b20a1af9d
--- /dev/null
+++ b/compiler/GHC/Tc/Utils/Concrete.hs
@@ -0,0 +1,521 @@
+{-# LANGUAGE MultiWayIf #-}
+
+module GHC.Tc.Utils.Concrete
+  ( -- * Creating/emitting 'Concrete#' constraints
+    hasFixedRuntimeRep
+  , newConcretePrimWanted
+    -- * HsWrapper: checking for representation-polymorphism
+  , mkWpFun
+  )
+ where
+
+import GHC.Prelude
+
+import GHC.Core.Coercion
+import GHC.Core.TyCo.Rep
+
+import GHC.Tc.Utils.Monad
+import GHC.Tc.Utils.TcType  ( TcType, mkTyConApp )
+import GHC.Tc.Utils.TcMType ( newCoercionHole, newFlexiTyVarTy )
+import GHC.Tc.Types.Constraint
+import GHC.Tc.Types.Evidence
+import GHC.Tc.Types.Origin ( CtOrigin(..), FRROrigin(..), WpFunOrigin(..) )
+
+import GHC.Builtin.Types      ( unliftedTypeKindTyCon, liftedTypeKindTyCon )
+import GHC.Builtin.Types.Prim ( concretePrimTyCon )
+
+import GHC.Types.Basic      ( TypeOrKind(KindLevel) )
+
+import GHC.Core.Type  ( isConcrete, typeKind )
+
+{- Note [Concrete overview]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Special predicates of the form `Concrete# ty` are used
+to check, in the typechecker, that certain types have a fixed runtime representation.
+We give here an overview of the various moving parts, to serve
+as a central point of reference for this topic.
+
+  * Representation polymorphism
+    Note [Representation polymorphism invariants] in GHC.Core
+    Note [Representation polymorphism checking]
+
+    The first note explains why we require that certain types have
+    a fixed runtime representation.
+
+    The second note details why we sometimes need a constraint to
+    perform such checks in the typechecker: we might not know immediately
+    whether a type has a fixed runtime representation. For example, we might
+    need further unification to take place before being able to decide.
+    So, instead of checking immediately, we emit a constraint.
+
+  * What does it mean for a type to be concrete?
+    Note [Concrete types]
+    Note [The Concrete mechanism]
+
+    The predicate 'Concrete# ty' is satisfied when we can produce
+    a coercion
+
+      co :: ty ~ concrete_ty
+
+    where 'concrete_ty' consists only of concrete types (no type variables,
+    no type families).
+
+    The first note explains more precisely what it means for a type to be concrete.
+    The second note explains how this relates to the `Concrete#` predicate,
+    and explains that the implementation is happening in two phases (PHASE 1 and PHASE 2).
+    In PHASE 1 (the current implementation) we only allow trivial evidence
+    of the form `co = Refl`.
+
+  * Fixed runtime representation vs fixed RuntimeRep
+    Note [Fixed RuntimeRep]
+
+    We currently enforce the representation-polymorphism invariants by checking
+    that binders and function arguments have a "fixed RuntimeRep".
+    That is, `ty :: ki` has a "fixed RuntimeRep" if we can solve `Concrete# ki`.
+
+    This is slightly less general than we might like, as this rules out
+    types with kind `TYPE (BoxedRep l)`: we know that this will be represented
+    by a pointer, which should be enough to go on in many situations.
+
+  * When do we emit 'Concrete#' constraints?
+    Note [hasFixedRuntimeRep]
+
+    We introduce 'Concrete#' constraints to satisfy the representation-polymorphism
+    invariants outlined in Note [Representation polymorphism invariants] in GHC.Core,
+    which mostly amounts to the following two cases:
+
+      - checking that a binder has a fixed runtime representation,
+      - checking that a function argument has a fixed runtime representation.
+
+    The note explains precisely how we emit these 'Concrete#' constraints.
+
+  * How do we solve Concrete# constraints?
+    Note [Solving Concrete# constraints] in GHC.Tc.Instance.Class
+
+    Concrete# constraints are solved through two mechanisms,
+    which are both explained further in the note:
+
+      - by decomposing them, e.g. `Concrete# (TYPE r)` is turned
+        into `Concrete# r` (canonicalisation of `Concrete#` constraints),
+      - by using 'Concrete' instances (top-level interactions).
+        The note explains that the evidence we get from using such 'Concrete'
+        instances can only ever be Refl, even in PHASE 2.
+
+  * Reporting unsolved Concrete# constraints
+    Note [Reporting representation-polymorphism errors] in GHC.Tc.Types.Origin
+
+    When we emit a 'Concrete#' constraint, we also provide a 'FRROrigin'
+    which gives context about the check being done. This origin gets reported
+    to the user if we end up with an unsolved Wanted 'Concrete#' constraint.
+
+Note [Representation polymorphism checking]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+According to the "Levity Polymorphism" paper (PLDI '17),
+there are two places in which we must know that a type has a
+fixed runtime representation, as explained in
+  Note [Representation polymorphism invariants] in GHC.Core:
+
+  I1. the type of a bound term-level variable,
+  I2. the type of an argument to a function.
+
+The paper explains the restrictions more fully, but briefly:
+expressions in these contexts need to be stored in registers, and it's
+hard (read: impossible) to store something that does not have a
+fixed runtime representation.
+
+In practice, we enforce these types to have a /fixed RuntimeRep/, which is slightly
+stronger, as explained in Note [Fixed RuntimeRep].
+
+There are two different ways we check whether a given type
+has a fixed runtime representation, both in the typechecker:
+
+  1. When typechecking type declarations (e.g. datatypes, typeclass, pattern synonyms),
+     under the GHC.Tc.TyCl module hierarchy.
+     In these situations, we can immediately reject bad representation polymorphism.
+
+     For instance, the following datatype declaration
+
+       data Foo (r :: RuntimeRep) (a :: TYPE r) = Foo a
+
+     is rejected in GHC.Tc.TyCl.checkValidDataCon upon seeing that the type 'a'
+     is representation-polymorphic.
+
+     Such checks are done using `GHC.Tc.Utils.TcMType.checkTypeHasFixedRuntimeRep`,
+     with `GHC.Tc.Errors.Types.FixedRuntimeRepProvenance` describing the different
+     contexts in which bad representation polymorphism can occur while validity checking.
+
+  2. When typechecking value-level declarations (functions, expressions, patterns, ...),
+     under the GHC.Tc.Gen module hierarchy.
+     In these situations, the typechecker might need to do some work to figure out
+     whether a type has a fixed runtime representation or not. For instance,
+     GHC might introduce a metavariable (rr :: RuntimeRep), which is only later
+     (through constraint solving) discovered to be equal to FloatRep.
+
+     This is handled by the Concrete mechanism outlined in
+     Note [The Concrete mechanism] in GHC.Tc.Utils.Concrete.
+     See Note [Concrete overview] in GHC.Tc.Utils.Concrete for an overview
+     of the various moving parts.
+
+     The idea is that, to guarantee that a type (rr :: RuntimeRep) is
+     representation-monomorphic, we emit a 'Concrete# rr' Wanted constraint.
+     If GHC can solve this constraint, it means 'rr' is monomorphic, and we
+     are OK to proceed. Otherwise, we report this unsolved Wanted in the form
+     of a representation-polymorphism error. The different contexts in which
+     such constraints arise are enumerated in 'FRROrigin'.
+
+Note [Concrete types]
+~~~~~~~~~~~~~~~~~~~~~
+Definition: a type is /concrete/
+            iff it consists of a tree of concrete type constructors
+            See GHC.Core.Type.isConcrete
+
+Definition: a /concrete type constructor/ is defined by
+            - a promoted data constructor
+            - a class, data type or newtype
+            - a primitive type like Array# or Int#
+            - an abstract type as defined in a Backpack signature file
+              (see Note [Synonyms implement abstract data] in GHC.Tc.Module)
+            In particular, type and data families are not concrete.
+            See GHC.Core.TyCon.isConcreteTyCon.
+
+Examples of concrete types:
+   Lifted, BoxedRep Lifted, TYPE (BoxedRep Lifted) are all concrete
+Examples of non-concrete types
+   F Int, TYPE (F Int), TYPE r, a Int
+   NB: (F Int) is not concrete because F is a type function
+
+Note [The Concrete mechanism]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+As explained in (2) in Note [Representation polymorphism checking],
+to check (ty :: ki) has a fixed runtime representation,
+we emit a `Concrete# ki` constraint, where
+
+  Concrete# :: forall k. k -> TupleRep '[]
+
+Such constraints get solved by decomposition, as per
+  Note [Canonical Concrete# constraints] in GHC.Tc.Solver.Canonical.
+When unsolved Wanted `Concrete#` constraints remain after typechecking,
+we report them as representation-polymorphism errors, using `GHC.Tc.Types.Origin.FRROrigin`
+to inform the user of the context in which a fixed-runtime-rep check arose.
+
+--------------
+-- EVIDENCE --
+--------------
+
+The evidence for a 'Concrete# ty' constraint is a nominal coercion
+
+  co :: ty ~# concrete_ty
+
+where 'concrete_ty' consists only of (non-synonym) type constructors and applications
+(after expanding any vanilla type synonyms).
+
+  OK:
+
+    TYPE FloatRep
+    TYPE (BoxedRep Lifted)
+    Type
+    TYPE (TupleRep '[ FloatRep, SumRep '[ IntRep, IntRep ] ])
+
+  Not OK:
+
+    Type variables:
+
+      ty
+      TYPE r
+      TYPE (BoxedRep l)
+
+    Type family applications:
+
+      TYPE (Id FloatRep)
+
+This is so that we can compute the 'PrimRep's needed to represent the type
+using 'runtimeRepPrimRep', which expects to be able to read off the 'RuntimeRep',
+as per Note [Getting from RuntimeRep to PrimRep] in GHC.Types.RepType.
+
+Note that the evidence for a `Concrete#` constraint isn't a typeclass dictionary:
+like with `(~#)`, the evidence is an (unlifted) nominal coercion, which justifies defining
+
+  Concrete# :: forall k. k -> TYPE (TupleRep '[])
+
+We still need a constraint that users can write in their own programs,
+so much like `(~#)` and `(~)` we also define:
+
+  Concrete :: forall k. k -> Constraint
+
+The need for user-facing 'Concrete' constraints is detailed in
+  Note [Concrete and Concrete#] in GHC.Builtin.Types.
+
+-------------------------
+-- PHASE 1 and PHASE 2 --
+-------------------------
+
+The Concrete mechanism is being implemented in two separate phases.
+
+In PHASE 1 (currently implemented), we never allow a 'Concrete#' constraint
+to be rewritten (see e.g. GHC.Tc.Solver.Canonical.canConcretePrim).
+The only allowable evidence term is Refl, which forbids any program
+that requires type family evaluation in order to determine that a 'RuntimeRep' is fixed.
+N.B.: we do not currently check that this invariant is upheld: as we are discarding the
+evidence in PHASE 1, we no longer have access to the coercion after constraint solving
+(which is the point at which we would want to check that the filled in evidence is Refl).
+
+In PHASE 2 (future work), we lift this restriction. To illustrate what this entails,
+recall that the code generator needs to be able to compute 'PrimRep's, so that it
+can put function arguments in the correct registers, etc.
+As a result, we must insert additional casts in Core to ensure that no type family
+reduction is needed to be able to compute 'PrimRep's. For example, the Core
+
+  f = /\ ( a :: F Int ). \ ( x :: a ). some_expression
+
+is problematic when 'F' is a type family: we don't know what runtime representation to use
+for 'x', so we can't compile this function (we can't evaluate type family applications
+after we are done with typechecking). Instead, we ensure the 'RuntimeRep' is always
+explicitly visible:
+
+  f = /\ ( a :: F Int ). \ ( x :: ( a |> kco ) ). some_expression
+
+where 'kco' is the evidence for `Concrete# (F Int)`, for example if `F Int = TYPE Int#`
+this would be:
+
+  kco :: F Int ~# TYPE Int#
+
+As `( a |> kco ) :: TYPE Int#`, the code generator knows to use a machine-sized
+integer register for `x`, and all is good again.
+
+Example test cases that require PHASE 2: T13105, T17021, T20363b.
+
+Note [Fixed RuntimeRep]
+~~~~~~~~~~~~~~~~~~~~~~~
+Definition:
+  a type `ty :: ki` has a /fixed RuntimeRep/
+  iff we can solve `Concrete# ki`
+
+In PHASE 1 (see Note [The Concrete mechanism]), this is equivalent to:
+
+  a type `ty :: ki` has a /fixed RuntimeRep/
+  iff `ki` is a concrete type (in the sense of Note [Concrete types]).
+
+This definition is crafted to be useful to satisfy the invariants of
+Core; see Note [Representation polymorphism invariants] in GHC.Core.
+
+Notice that "fixed RuntimeRep" means (for now anyway) that
+  * we know the runtime representation, and
+  * we know the levity.
+
+For example (ty :: TYPE (BoxedRep l)), where `l` is a levity variable
+is /not/ "fixed RuntimeRep", even though it is always represented by
+a heap pointer, because we don't know the levity.  In due course we
+will want to make finer distinctions, as explained in the paper
+Kinds are Calling Conventions [ICFP'20], but this suffices for now.
+
+Note [hasFixedRuntimeRep]
+~~~~~~~~~~~~~~~~~~~~~~~~~
+The 'hasFixedRuntimeRep' function is responsible for taking a type 'ty'
+and emitting a 'Concrete#' constraint to ensure that 'ty' has a fixed `RuntimeRep`,
+as outlined in Note [The Concrete mechanism].
+
+To do so, we compute the kind 'ki' of 'ty' and emit a 'Concrete# ki' constraint,
+which will only be solved if we can prove that 'ty' indeed has a fixed RuntimeRep.
+
+  [Wrinkle: Typed Template Haskell]
+    We don't perform any checks when type-checking a typed Template Haskell quote:
+    we want to allow representation polymorphic quotes, as long as they are
+    monomorphised at splice site.
+
+    Example:
+
+      Module1
+
+        repPolyId :: forall r (a :: TYPE r). CodeQ (a -> a)
+        repPolyId = [|| \ x -> x ||]
+
+      Module2
+
+        import Module1
+
+        id1 :: Int -> Int
+        id1 = $$repPolyId
+
+        id2 :: Int# -> Int#
+        id2 = $$repPolyId
+
+    We implement this skip by inspecting the TH stage in `hasFixedRuntimeRep`.
+
+    A better solution would be to use 'CodeC' constraints, as in the paper
+      "Staging With Class", POPL 2022
+        by Ningning Xie, Matthew Pickering, Andres Löh, Nicolas Wu, Jeremy Yallop, Meng Wang
+    but for the moment, as we will typecheck again when splicing,
+    this shouldn't cause any problems in practice.  See ticket #18170.
+
+    Test case: rep-poly/T18170a.
+
+Note [Solving Concrete# constraints]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The representation polymorphism checks emit 'Concrete# ty' constraints,
+as explained in Note [hasFixedRuntimeRep] in GHC.Tc.Utils.Concrete.
+
+The main mechanism through which a `Concrete# ty` constraint is solved
+is to directly inspect 'ty' to check that it is a concrete type
+such as 'TYPE IntRep' or `TYPE (TupleRep '[ TupleRep '[], FloatRep ])`,
+and not, e.g., a skolem type variable.
+
+There are, however, some interactions to take into account:
+
+  1. Decomposition.
+
+      The solving of `Concrete#` constraints works recursively.
+      For example, to solve a Wanted `Concrete# (TYPE r)` constraint,
+      we decompose it, emitting a new `Concrete# @RuntimeRep r` Wanted constraint,
+      and use it to solve the original `Concrete# (TYPE r)` constraint.
+      This happens in the canonicaliser -- see GHC.Tc.Solver.Canonical.canDecomposableConcretePrim.
+
+      Note that Decomposition fully solves `Concrete# ty` whenever `ty` is a
+      concrete type.   For example:
+
+          Concrete# (TYPE (BoxedRep Lifted))
+          ==> (decompose)
+          Concrete# (BoxedRep Lifted)
+          ==> (decompose)
+          Concrete# Lifted
+          ==> (decompose)
+          <nothing, since Lifted is nullary>
+
+  2. Rewriting.
+
+      In PHASE 1 (as per Note [The Concrete mechanism] in GHC.Tc.Utils.Concrete),
+      we don't have to worry about a 'Concrete#' constraint being rewritten.
+      We only need to zonk: if e.g. a metavariable, `alpha`, gets unified with `IntRep`,
+      we should be able to solve `Concrete# alpha`.
+
+      In PHASE 2, we will need to proceed as in GHC.Tc.Solver.Canonical.canClass:
+      if we have a constraint `Concrete# (F ty1)` and a coercion witnessing the reduction of
+      `F`, say `co :: F ty1 ~# ty2`, then we will solve `Concrete# (F ty1)` in terms of `Concrete# ty2`,
+      by rewriting the evidence for `Concrete# ty2` using `co` (see GHC.Tc.Solver.Canonical.rewriteEvidence).
+
+  3. Backpack
+
+      Abstract 'TyCon's in Backpack signature files are always considered to be concrete.
+      This is because of the strong restrictions around how abstract types are allowed
+      to be implemented, as laid out in Note [Synonyms implement abstract data] in GHC.Tc.Module.
+      In particular, no variables or type family applications are allowed.
+
+      Examples: backpack/should_run/T13955.bkp, rep-poly/RepPolyBackpack2.
+-}
+
+-- | A coercion hole used to store evidence for `Concrete#` constraints.
+--
+-- See Note [The Concrete mechanism].
+type ConcreteHole = CoercionHole
+
+-- | Evidence for a `Concrete#` constraint:
+-- essentially a 'ConcreteHole' (a coercion hole) that will be filled later,
+-- except:
+--
+--   - we might already have the evidence now; no point in creating a coercion hole
+--     in that case;
+--   - we sometimes skip the check entirely, e.g. in Typed Template Haskell
+--     (see [Wrinkle: Typed Template Haskell] in Note [hasFixedRuntimeRep]).
+data ConcreteEvidence
+  = ConcreteReflEvidence
+    -- ^ We have evidence right now: don't bother creating a 'ConcreteHole'.
+  | ConcreteTypedTHNoEvidence
+    -- ^ We don't emit 'Concrete#' constraints in Typed Template Haskell.
+    -- See [Wrinkle: Typed Template Haskell] in Note [hasFixedRuntimeRep].
+  | ConcreteHoleEvidence ConcreteHole
+    -- ^ The general form of evidence: a 'ConcreteHole' that should be
+    -- filled in later by the constraint solver, as per
+    -- Note [Solving Concrete# constraints].
+
+-- | Check that the kind of the provided type is of the form
+-- @TYPE rep@ for a __fixed__ 'RuntimeRep' @rep@.
+--
+-- If this isn't immediately obvious, for instance if the 'RuntimeRep'
+-- is hidden under a type-family application such as
+--
+-- > ty :: TYPE (F x)
+--
+-- this function will emit a new Wanted 'Concrete#' constraint.
+hasFixedRuntimeRep :: FRROrigin -> Type -> TcM ConcreteEvidence
+hasFixedRuntimeRep frrOrig ty
+
+  -- Shortcut: check for 'Type' and 'UnliftedType' type synonyms.
+  | TyConApp tc [] <- ki
+  , tc == liftedTypeKindTyCon || tc == unliftedTypeKindTyCon
+  = return ConcreteReflEvidence
+
+  | otherwise
+  = do { th_stage <- getStage
+       ; if
+          -- We have evidence for 'Concrete# ty' right now:
+          -- no need to emit a constraint/create an evidence hole.
+          | isConcrete ki
+          -> return ConcreteReflEvidence
+
+          -- See [Wrinkle: Typed Template Haskell] in Note [hasFixedRuntimeRep].
+          | Brack _ (TcPending {}) <- th_stage
+          -> return ConcreteTypedTHNoEvidence
+
+          -- Create a new Wanted 'Concrete#' constraint and emit it.
+          | otherwise
+          -> do { loc <- getCtLocM (FixedRuntimeRepOrigin ty frrOrig) (Just KindLevel)
+                ; (hole, ct_ev) <- newConcretePrimWanted loc ki
+                ; emitSimple $ mkNonCanonical ct_ev
+                ; return $ ConcreteHoleEvidence hole } }
+  where
+    ki :: Kind
+    ki = typeKind ty
+
+-- | Create a new (initially unfilled) coercion hole,
+-- to hold evidence for a @'Concrete#' (ty :: ki)@ constraint.
+newConcreteHole :: Kind -- ^ Kind of the thing we want to ensure is concrete (e.g. 'runtimeRepTy')
+                -> Type -- ^ Thing we want to ensure is concrete (e.g. some 'RuntimeRep')
+                -> TcM ConcreteHole
+newConcreteHole ki ty
+  = do { concrete_ty <- newFlexiTyVarTy ki
+       ; let co_ty = mkHeteroPrimEqPred ki ki ty concrete_ty
+       ; newCoercionHole co_ty }
+
+-- | Create a new 'Concrete#' constraint.
+newConcretePrimWanted :: CtLoc -> Type -> TcM (ConcreteHole, CtEvidence)
+newConcretePrimWanted loc ty
+  = do { let
+           ki :: Kind
+           ki = typeKind ty
+       ; hole <- newConcreteHole ki ty
+       ; let
+           wantedCtEv :: CtEvidence
+           wantedCtEv =
+             CtWanted
+               { ctev_dest = HoleDest hole
+               , ctev_pred = mkTyConApp concretePrimTyCon [ki, ty]
+               , ctev_nosh = WOnly -- WOnly, because Derived Concrete# constraints
+                                   -- aren't useful: solving a Concrete# constraint
+                                   -- can't cause any unification to take place.
+               , ctev_loc  = loc
+               }
+        ; return (hole, wantedCtEv) }
+
+{-***********************************************************************
+*                                                                       *
+                 HsWrapper
+*                                                                       *
+***********************************************************************-}
+
+-- | Smart constructor to create a 'WpFun' 'HsWrapper'.
+--
+-- Might emit a 'Concrete#' constraint, 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 { _concrete_ev <- hasFixedRuntimeRep (FRRWpFun wpFunOrig) (scaledThing t1)
+       ; return $ WpFun co1 co2 t1 }
diff --git a/compiler/GHC/Tc/Utils/Instantiate.hs b/compiler/GHC/Tc/Utils/Instantiate.hs
index 6977dcf105..dace3d08f6 100644
--- a/compiler/GHC/Tc/Utils/Instantiate.hs
+++ b/compiler/GHC/Tc/Utils/Instantiate.hs
@@ -69,12 +69,13 @@ import GHC.Tc.Types.Origin
 import GHC.Tc.Utils.Env
 import GHC.Tc.Types.Evidence
 import GHC.Tc.Instance.FunDeps
+import GHC.Tc.Utils.Concrete
 import GHC.Tc.Utils.TcMType
 import GHC.Tc.Utils.TcType
 import GHC.Tc.Errors.Types
 
 import GHC.Types.Id.Make( mkDictFunId )
-import GHC.Types.Basic ( TypeOrKind(..) )
+import GHC.Types.Basic ( TypeOrKind(..), Arity )
 import GHC.Types.Error
 import GHC.Types.SourceText
 import GHC.Types.SrcLoc as SrcLoc
@@ -95,7 +96,7 @@ import GHC.Unit.External
 
 import Data.List ( mapAccumL )
 import qualified Data.List.NonEmpty as NE
-import Control.Monad( unless )
+import Control.Monad( when, unless, void )
 import Data.Function ( on )
 
 {-
@@ -740,10 +741,10 @@ just use the expression inline.
 -}
 
 tcSyntaxName :: CtOrigin
-             -> TcType                 -- ^ Type to instantiate it at
-             -> (Name, HsExpr GhcRn)   -- ^ (Standard name, user name)
+             -> TcType                  -- ^ Type to instantiate it at
+             -> (Name, HsExpr GhcRn)    -- ^ (Standard name, user name)
              -> TcM (Name, HsExpr GhcTc)
-                                       -- ^ (Standard name, suitable expression)
+                                        -- ^ (Standard name, suitable expression)
 -- USED ONLY FOR CmdTop (sigh) ***
 -- See Note [CmdSyntaxTable] in "GHC.Hs.Expr"
 
@@ -755,31 +756,65 @@ tcSyntaxName orig ty (std_nm, HsVar _ (L _ user_nm))
 tcSyntaxName orig ty (std_nm, user_nm_expr) = do
     std_id <- tcLookupId std_nm
     let
-        -- C.f. newMethodAtLoc
         ([tv], _, tau) = tcSplitSigmaTy (idType std_id)
         sigma1         = substTyWith [tv] [ty] tau
         -- Actually, the "tau-type" might be a sigma-type in the
         -- case of locally-polymorphic methods.
 
-    addErrCtxtM (syntaxNameCtxt user_nm_expr orig sigma1) $ do
+    span <- getSrcSpanM
+    addErrCtxtM (syntaxNameCtxt user_nm_expr orig sigma1 span) $ do
 
         -- Check that the user-supplied thing has the
         -- same type as the standard one.
         -- Tiresome jiggling because tcCheckSigma takes a located expression
-     span <- getSrcSpanM
      expr <- tcCheckPolyExpr (L (noAnnSrcSpan span) user_nm_expr) sigma1
+     hasFixedRuntimeRepRes std_nm user_nm_expr sigma1
      return (std_nm, unLoc expr)
 
-syntaxNameCtxt :: HsExpr GhcRn -> CtOrigin -> Type -> TidyEnv
+syntaxNameCtxt :: HsExpr GhcRn -> CtOrigin -> Type -> SrcSpan -> TidyEnv
                -> TcRn (TidyEnv, SDoc)
-syntaxNameCtxt name orig ty tidy_env
-  = do { inst_loc <- getCtLocM orig (Just TypeLevel)
-       ; let msg = vcat [ text "When checking that" <+> quotes (ppr name)
+syntaxNameCtxt name orig ty loc tidy_env = return (tidy_env, msg)
+  where
+    msg = vcat [ text "When checking that" <+> quotes (ppr name)
                           <+> text "(needed by a syntactic construct)"
-                        , nest 2 (text "has the required type:"
-                                  <+> ppr (tidyType tidy_env ty))
-                        , nest 2 (pprCtLoc inst_loc) ]
-       ; return (tidy_env, msg) }
+               , nest 2 (text "has the required type:"
+                         <+> ppr (tidyType tidy_env ty))
+               , nest 2 (sep [ppr orig, text "at" <+> ppr loc])]
+
+{-
+************************************************************************
+*                                                                      *
+                FixedRuntimeRep
+*                                                                      *
+************************************************************************
+-}
+
+-- | Check that the result type of an expression has a fixed runtime representation.
+--
+-- Used only for arrow operations such as 'arr', 'first', etc.
+hasFixedRuntimeRepRes :: Name -> HsExpr GhcRn -> TcSigmaType -> TcM ()
+hasFixedRuntimeRepRes std_nm user_expr ty = mapM_ do_check mb_arity
+  where
+   do_check :: Arity -> TcM ()
+   do_check arity =
+     let res_ty = nTimes arity (snd . splitPiTy) ty
+     in void $ hasFixedRuntimeRep (FRRArrow $ ArrowFun user_expr) res_ty
+   mb_arity :: Maybe Arity
+   mb_arity -- arity of the arrow operation, counting type-level arguments
+     | std_nm == arrAName     -- result used as an argument in, e.g., do_premap
+     = Just 3
+     | std_nm == composeAName -- result used as an argument in, e.g., dsCmdStmt/BodyStmt
+     = Just 5
+     | std_nm == firstAName   -- result used as an argument in, e.g., dsCmdStmt/BodyStmt
+     = Just 4
+     | std_nm == appAName     -- result used as an argument in, e.g., dsCmd/HsCmdArrApp/HsHigherOrderApp
+     = Just 2
+     | std_nm == choiceAName  -- result used as an argument in, e.g., HsCmdIf
+     = Just 5
+     | std_nm == loopAName    -- result used as an argument in, e.g., HsCmdIf
+     = Just 4
+     | otherwise
+     = Nothing
 
 {-
 ************************************************************************
@@ -827,7 +862,8 @@ newClsInst overlap_mode dfun_name tvs theta clas tys
 
        ; oflag <- getOverlapFlag overlap_mode
        ; let inst = mkLocalInstance dfun oflag tvs' clas tys'
-       ; warnIf (isOrphan (is_orphan inst)) (TcRnOrphanInstance inst)
+       ; when (isOrphan (is_orphan inst)) $
+          addDiagnostic (TcRnOrphanInstance inst)
        ; return inst }
 
 tcExtendLocalInstEnv :: [ClsInst] -> TcM a -> TcM a
diff --git a/compiler/GHC/Tc/Utils/TcMType.hs b/compiler/GHC/Tc/Utils/TcMType.hs
index 1a008bbff0..7be996a789 100644
--- a/compiler/GHC/Tc/Utils/TcMType.hs
+++ b/compiler/GHC/Tc/Utils/TcMType.hs
@@ -66,7 +66,7 @@ module GHC.Tc.Utils.TcMType (
 
   --------------------------------
   -- Zonking and tidying
-  zonkTidyTcType, zonkTidyTcTypes, zonkTidyOrigin,
+  zonkTidyTcType, zonkTidyTcTypes, zonkTidyOrigin, zonkTidyOrigins,
   tidyEvVar, tidyCt, tidyHole, tidySkolemInfo,
     zonkTcTyVar, zonkTcTyVars,
   zonkTcTyVarToTyVar, zonkInvisTVBinder,
@@ -93,7 +93,7 @@ module GHC.Tc.Utils.TcMType (
 
   ------------------------------
   -- Representation polymorphism
-  ensureNotLevPoly, checkForLevPoly, checkForLevPolyX,
+  checkTypeHasFixedRuntimeRep,
   ) where
 
 import GHC.Prelude
@@ -116,6 +116,7 @@ import GHC.Core.TyCon
 import GHC.Core.Coercion
 import GHC.Core.Class
 import GHC.Core.Predicate
+import GHC.Core.InstEnv (ClsInst(is_tys))
 
 import GHC.Types.Var
 import GHC.Types.Id as Id
@@ -203,7 +204,7 @@ newWanteds orig = mapM (newWanted orig Nothing)
 
 cloneWanted :: Ct -> TcM Ct
 cloneWanted ct
-  | ev@(CtWanted { ctev_pred = pty }) <- ctEvidence ct
+  | ev@(CtWanted { ctev_pred = pty, ctev_dest = HoleDest _ }) <- ctEvidence ct
   = do { co_hole <- newCoercionHole pty
        ; return (mkNonCanonical (ev { ctev_dest = HoleDest co_hole })) }
   | otherwise
@@ -307,6 +308,9 @@ predTypeOccName ty = case classifyPredType ty of
     EqPred {}       -> mkVarOccFS (fsLit "co")
     IrredPred {}    -> mkVarOccFS (fsLit "irred")
     ForAllPred {}   -> mkVarOccFS (fsLit "df")
+    SpecialPred special_pred _ ->
+      case special_pred of
+        ConcretePrimPred -> mkVarOccFS (fsLit "concr")
 
 -- | Create a new 'Implication' with as many sensible defaults for its fields
 -- as possible. Note that the 'ic_tclvl', 'ic_binds', and 'ic_info' fields do
@@ -2550,8 +2554,20 @@ zonkTidyOrigin env (FunDepOrigin2 p1 o1 p2 l2)
        ; (env2, p2') <- zonkTidyTcType env1 p2
        ; (env3, o1') <- zonkTidyOrigin env2 o1
        ; return (env3, FunDepOrigin2 p1' o1' p2' l2) }
+zonkTidyOrigin env (CycleBreakerOrigin orig)
+  = do { (env1, orig') <- zonkTidyOrigin env orig
+       ; return (env1, CycleBreakerOrigin orig') }
+zonkTidyOrigin env (InstProvidedOrigin mod cls_inst)
+  = do { (env1, is_tys') <- mapAccumLM zonkTidyTcType env (is_tys cls_inst)
+       ; return (env1, InstProvidedOrigin mod (cls_inst {is_tys = is_tys'})) }
+zonkTidyOrigin env (FixedRuntimeRepOrigin ty frr_orig)
+  = do { (env1, ty') <- zonkTidyTcType env ty
+       ; return (env1, FixedRuntimeRepOrigin ty' frr_orig)}
 zonkTidyOrigin env orig = return (env, orig)
 
+zonkTidyOrigins :: TidyEnv -> [CtOrigin] -> TcM (TidyEnv, [CtOrigin])
+zonkTidyOrigins = mapAccumLM zonkTidyOrigin
+
 ----------------
 tidyCt :: TidyEnv -> Ct -> Ct
 -- Used only in error reporting
@@ -2614,43 +2630,22 @@ tidySigSkol env cx ty tv_prs
 %*                                                                      *
              Representation polymorphism checks
 *                                                                       *
-*************************************************************************
-
-See Note [Representation polymorphism checking] in GHC.HsToCore.Monad
-
--}
+***********************************************************************-}
 
--- | According to the rules around representation polymorphism
--- (see https://gitlab.haskell.org/ghc/ghc/wikis/no-sub-kinds), no binder
--- can have a representation-polymorphic type. This check ensures
--- that we respect this rule. It is a bit regrettable that this error
--- occurs in zonking, after which we should have reported all errors.
--- But it's hard to see where else to do it, because this can be discovered
--- only after all solving is done. And, perhaps most importantly, this
--- isn't really a compositional property of a type system, so it's
--- not a terrible surprise that the check has to go in an awkward spot.
-ensureNotLevPoly :: Type  -- its zonked type
-                 -> LevityCheckProvenance  -- where this happened
-                 -> TcM ()
-ensureNotLevPoly ty provenance
-  = whenNoErrs $   -- sometimes we end up zonking bogus definitions of type
-                   -- forall a. a. See, for example, test ghci/scripts/T9140
-    checkForLevPoly provenance ty
-
-  -- See Note [Representation polymorphism checking] in GHC.HsToCore.Monad
-checkForLevPoly :: LevityCheckProvenance -> Type -> TcM ()
-checkForLevPoly = checkForLevPolyX (\ty -> addDetailedDiagnostic . TcLevityPolyInType ty)
-
-checkForLevPolyX :: Monad m
-                 => (Type -> LevityCheckProvenance -> m ())  -- how to report an error
-                 -> LevityCheckProvenance
-                 -> Type
-                 -> m ()
-checkForLevPolyX add_err provenance ty
-  | isTypeLevPoly ty
-  = add_err ty provenance
-  | otherwise
-  = return ()
+-- | Check that the specified type has a fixed runtime representation.
+--
+-- If it isn't, throw a representation-polymorphism error appropriate
+-- for the context (as specified by the 'FixedRuntimeRepProvenance').
+--
+-- Unlike the other representation polymorphism checks, which emit
+-- 'Concrete#' constraints, this function does not emit any constraints,
+-- as it has enough information to immediately make a decision.
+--
+-- See (1) in Note [Representation polymorphism checking] in GHC.Tc.Utils.Concrete
+checkTypeHasFixedRuntimeRep :: FixedRuntimeRepProvenance -> Type -> TcM ()
+checkTypeHasFixedRuntimeRep prov ty =
+  unless (typeHasFixedRuntimeRep ty)
+    (addDetailedDiagnostic $ TcRnTypeDoesNotHaveFixedRuntimeRep ty prov)
 
 {-
 %************************************************************************
diff --git a/compiler/GHC/Tc/Utils/TcType.hs b/compiler/GHC/Tc/Utils/TcType.hs
index 5313ef39d4..b79a4152e1 100644
--- a/compiler/GHC/Tc/Utils/TcType.hs
+++ b/compiler/GHC/Tc/Utils/TcType.hs
@@ -146,7 +146,7 @@ module GHC.Tc.Utils.TcType (
   isClassPred, isEqPrimPred, isIPLikePred, isEqPred, isEqPredClass,
   mkClassPred,
   tcSplitDFunTy, tcSplitDFunHead, tcSplitMethodTy,
-  isRuntimeRepVar, isKindLevPoly,
+  isRuntimeRepVar, isFixedRuntimeRepKind,
   isVisibleBinder, isInvisibleBinder,
 
   -- Type substitutions
@@ -1935,6 +1935,7 @@ isImprovementPred ty
       ClassPred cls _    -> classHasFds cls
       IrredPred {}       -> True -- Might have equalities after reduction?
       ForAllPred {}      -> False
+      SpecialPred {}     -> False
 
 {- Note [Expanding superclasses]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
diff --git a/compiler/GHC/Tc/Utils/Unify.hs b/compiler/GHC/Tc/Utils/Unify.hs
index dc1fd382d2..a0b8106a8d 100644
--- a/compiler/GHC/Tc/Utils/Unify.hs
+++ b/compiler/GHC/Tc/Utils/Unify.hs
@@ -43,18 +43,23 @@ import GHC.Prelude
 import GHC.Hs
 import GHC.Core.TyCo.Rep
 import GHC.Core.TyCo.Ppr( debugPprType )
-import GHC.Tc.Utils.TcMType
+import GHC.Tc.Utils.Concrete ( mkWpFun )
+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.Tc.Utils.Env
+
+
 import GHC.Core.Type
 import GHC.Core.Coercion
 import GHC.Core.Multiplicity
+
 import GHC.Tc.Types.Evidence
 import GHC.Tc.Types.Constraint
 import GHC.Tc.Types.Origin
 import GHC.Types.Name( isSystemName )
-import GHC.Tc.Utils.Instantiate
+
 import GHC.Core.TyCon
 import GHC.Builtin.Types
 import GHC.Types.Var as Var
@@ -210,12 +215,8 @@ 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
-           ; let wrap_fun2 = mkWpFun idHsWrapper wrap_res arg_ty1 res_ty doc
+           ; wrap_fun2 <- mkWpFun idHsWrapper wrap_res arg_ty1 res_ty (WpFunFunTy fun_ty)
            ; return (wrap_fun2 <.> wrap_fun1, arg_ty1:arg_tys, res_ty) }
-      where
-        doc = text "When inferring the argument type of a function with type" <+>
-              quotes (ppr fun_ty)
-
 
 {-
 ************************************************************************
@@ -320,11 +321,8 @@ matchExpectedFunTys herald ctx arity orig_ty thing_inside
       = assert (af == VisArg) $
         do { (wrap_res, result) <- go ((Scaled mult $ mkCheckExpType arg_ty) : acc_arg_tys)
                                       (n-1) res_ty
-           ; let fun_wrap = mkWpFun idHsWrapper wrap_res (Scaled mult arg_ty) res_ty doc
+           ; fun_wrap <- mkWpFun idHsWrapper wrap_res (Scaled mult arg_ty) res_ty (WpFunFunExpTy orig_ty)
            ; return ( fun_wrap, result ) }
-      where
-        doc = text "When inferring the argument type of a function with type" <+>
-              quotes (ppr orig_ty)
 
     go acc_arg_tys n ty@(TyVarTy tv)
       | isMetaTyVar tv
@@ -779,7 +777,7 @@ There is no notion of multiplicity coercion in Core, therefore the wrapper
 returned by tcSubMult (and derived functions such as tcCheckUsage and
 checkManyPattern) is quite unlike any other wrapper: it checks whether the
 coercion produced by the constraint solver is trivial, producing a type error
-is it is not. This is implemented via the WpMultCoercion wrapper, as desugared
+if it is not. This is implemented via the WpMultCoercion wrapper, as desugared
 by GHC.HsToCore.Binds.dsHsWrapper, which does the reflexivity check.
 
 This wrapper needs to be placed in the term; otherwise, checking of the
@@ -788,11 +786,14 @@ anywhere, since it doesn't affect the desugared code.
 
 Why do we check this in the desugarer? It's a convenient place, since it's
 right after all the constraints are solved. We need the constraints to be
-solved to check whether they are trivial or not. Plus there is precedent for
-type errors during desuraging (such as the representation polymorphism
-restriction). An alternative would be to have a kind of constraint which can
-only produce trivial evidence, then this check would happen in the constraint
-solver (#18756).
+solved to check whether they are trivial or not.
+
+An alternative would be to have a kind of constraint which can
+only produce trivial evidence. This would allow such checks to happen
+in the constraint solver (#18756).
+This would be similar to the existing setup for Concrete, see
+  Note [The Concrete mechanism] in GHC.Tc.Utils.Concrete
+    (PHASE 1 in particular).
 -}
 
 tcSubMult :: CtOrigin -> Mult -> Mult -> TcM HsWrapper
diff --git a/compiler/GHC/Tc/Utils/Zonk.hs b/compiler/GHC/Tc/Utils/Zonk.hs
index 963fe9f9b1..3ac4b13582 100644
--- a/compiler/GHC/Tc/Utils/Zonk.hs
+++ b/compiler/GHC/Tc/Utils/Zonk.hs
@@ -49,7 +49,6 @@ import GHC.Builtin.Names
 
 import GHC.Hs
 
-import GHC.Tc.Errors.Types ( LevityCheckProvenance(..) )
 import {-# SOURCE #-} GHC.Tc.Gen.Splice (runTopSplice)
 import GHC.Tc.Utils.Monad
 import GHC.Tc.TyCl.Build ( TcMethInfo, MethInfo )
@@ -387,8 +386,6 @@ zonkIdOccs env ids = map (zonkIdOcc env) ids
 zonkIdBndr :: ZonkEnv -> TcId -> TcM Id
 zonkIdBndr env v
   = do Scaled w' ty' <- zonkScaledTcTypeToTypeX env (idScaledType v)
-       ensureNotLevPoly ty' (LevityCheckInBinder v)
-
        return (modifyIdInfo (`setLevityInfoWithType` ty') (setIdMult (setIdType v ty') w'))
 
 zonkIdBndrs :: ZonkEnv -> [TcId] -> TcM [Id]
@@ -1065,10 +1062,10 @@ zonkCoFn env WpHole   = return (env, WpHole)
 zonkCoFn env (WpCompose c1 c2) = do { (env1, c1') <- zonkCoFn env c1
                                     ; (env2, c2') <- zonkCoFn env1 c2
                                     ; return (env2, WpCompose c1' c2') }
-zonkCoFn env (WpFun c1 c2 t1 d) = do { (env1, c1') <- zonkCoFn env c1
-                                     ; (env2, c2') <- zonkCoFn env1 c2
-                                     ; t1'         <- zonkScaledTcTypeToTypeX env2 t1
-                                     ; return (env2, WpFun c1' c2' t1' d) }
+zonkCoFn env (WpFun c1 c2 t1)  = do { (env1, c1') <- zonkCoFn env c1
+                                    ; (env2, c2') <- zonkCoFn env1 c2
+                                    ; t1'         <- zonkScaledTcTypeToTypeX env2 t1
+                                    ; return (env2, WpFun c1' c2' t1') }
 zonkCoFn env (WpCast co) = do { co' <- zonkCoToCo env co
                               ; return (env, WpCast co') }
 zonkCoFn env (WpEvLam ev)   = do { (env', ev') <- zonkEvBndrX env ev
@@ -1348,7 +1345,6 @@ zonk_pat env (ParPat x lpar p rpar)
 
 zonk_pat env (WildPat ty)
   = do  { ty' <- zonkTcTypeToTypeX env ty
-        ; ensureNotLevPoly ty' LevityCheckInWildcardPattern
         ; return (env, WildPat ty') }
 
 zonk_pat env (VarPat x (L l v))
@@ -1389,8 +1385,7 @@ zonk_pat env (SumPat tys pat alt arity )
         ; (env', pat') <- zonkPat env pat
         ; return (env', SumPat tys' pat' alt arity) }
 
-zonk_pat env p@(ConPat { pat_con = L _ con
-                       , pat_args = args
+zonk_pat env p@(ConPat { pat_args = args
                        , pat_con_ext = p'@(ConPatTc
                          { cpt_tvs = tyvars
                          , cpt_dicts = evs
@@ -1401,16 +1396,6 @@ zonk_pat env p@(ConPat { pat_con = L _ con
                        })
   = assert (all isImmutableTyVar tyvars) $
     do  { new_tys <- mapM (zonkTcTypeToTypeX env) tys
-
-          -- an unboxed tuple pattern (but only an unboxed tuple pattern)
-          -- might have representation-polymorphic arguments.
-          -- Check for this badness.
-        ; case con of
-            RealDataCon dc
-              | isUnboxedTupleTyCon (dataConTyCon dc)
-              -> mapM_ (checkForLevPoly (LevityCheckInUnboxedTuplePattern p)) (dropRuntimeRepArgs new_tys)
-            _ -> return ()
-
         ; (env0, new_tyvars) <- zonkTyBndrsX env tyvars
           -- Must zonk the existential variables, because their
           -- /kind/ need potential zonking.