Introduce ConcreteTv metavariables

  This patch introduces a new kind of metavariable, by adding the
  constructor `ConcreteTv` to `MetaInfo`. A metavariable with
  `ConcreteTv` `MetaInfo`, henceforth a concrete metavariable, can only
  be unified with a type that is concrete (that is, a type that answers
  `True` to `GHC.Core.Type.isConcrete`).

  This solves the problem of dangling metavariables in `Concrete#`
  constraints: instead of emitting `Concrete# ty`, which contains a
  secret existential metavariable, we simply emit a primitive equality
  constraint `ty ~# concrete_tv` where `concrete_tv` is a fresh concrete
  metavariable.

  This means we can avoid all the complexity of canonicalising
  `Concrete#` constraints, as we can just re-use the existing machinery
  for `~#`.

  To finish things up, this patch then removes the `Concrete#` special
  predicate, and instead introduces the special predicate `IsRefl#`
  which enforces that a coercion is reflexive.
  Such a constraint is needed because the canonicaliser is quite happy
  to rewrite an equality constraint such as `ty ~# concrete_tv`, but
  such a rewriting is not handled by the rest of the compiler currently,
  as we need to make use of the resulting coercion, as outlined in the
  FixedRuntimeRep plan.

  The big upside of this approach (on top of simplifying the code)
  is that we can now selectively implement PHASE 2 of FixedRuntimeRep,
  by changing individual calls of `hasFixedRuntimeRep_MustBeRefl` to
  `hasFixedRuntimeRep` and making use of the obtained coercion.

6 files changed, 310 insertions, 274 deletions

diff --git a/compiler/GHC/Tc/Utils/Concrete.hs b/compiler/GHC/Tc/Utils/Concrete.hs
index 8ae32e5a78..dbf379479d 100644
--- a/compiler/GHC/Tc/Utils/Concrete.hs
+++ b/compiler/GHC/Tc/Utils/Concrete.hs
@@ -1,9 +1,13 @@
 {-# LANGUAGE MultiWayIf #-}
 
+-- | Checking for representation-polymorphism using the Concrete mechanism.
+--
+-- This module contains the logic for enforcing the representation-polymorphism
+-- invariants by way of emitting constraints.
 module GHC.Tc.Utils.Concrete
-  ( -- * Creating/emitting 'Concrete#' constraints
+  ( -- * Ensuring that a type has a fixed runtime representation
     hasFixedRuntimeRep
-  , newConcretePrimWanted
+  , hasFixedRuntimeRep_MustBeRefl
     -- * HsWrapper: checking for representation-polymorphism
   , mkWpFun
   )
@@ -11,28 +15,38 @@ module GHC.Tc.Utils.Concrete
 
 import GHC.Prelude
 
-import GHC.Core.Coercion   ( multToCo )
-import GHC.Core.Type       ( isConcrete, typeKind )
-import GHC.Core.TyCo.Rep
-
-import GHC.Tc.Utils.Monad
-import GHC.Tc.Utils.TcType  ( mkTyConApp )
-import GHC.Tc.Utils.TcMType
-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      ( unliftedTypeKindTyCon, liftedTypeKindTyCon )
-import GHC.Builtin.Types.Prim ( concretePrimTyCon )
+import GHC.Core.Coercion       ( Role(..), multToCo )
+import GHC.Core.Predicate      ( mkIsReflPrimPred )
+import GHC.Core.TyCo.Rep       ( Type(TyConApp), Scaled(..)
+                               , mkTyVarTy, scaledThing )
+import GHC.Core.Type           ( isConcrete, typeKind )
 
-import GHC.Types.Basic      ( TypeOrKind(KindLevel) )
+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.Utils.Monad      ( emitSimple, getStage )
+import GHC.Tc.Utils.TcType     ( TcType, TcKind, TcTyVar, MetaInfo(ConcreteTv) )
+import GHC.Tc.Utils.TcMType    ( newAnonMetaTyVar, newWanted, emitWantedEq )
 
+import GHC.Types.Basic         ( TypeOrKind(..) )
 
+import GHC.Utils.Misc          ( HasDebugCallStack )
+import GHC.Utils.Outputable
+import GHC.Utils.Panic         ( assertPpr )
 
 {- 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.
+GHC ensures that certain types have a fixed runtime representation in the
+typechecker, by emitting certain constraints.
+Emitting constraints to be solved later allows us to accept more programs:
+if we directly inspected the type (using e.g. `typePrimRep`), we might not
+have enough information available (e.g. if the type has kind `TYPE r` for
+a metavariable `r` which has not yet been filled in.)
+
 We give here an overview of the various moving parts, to serve
 as a central point of reference for this topic.
 
@@ -50,20 +64,26 @@ as a central point of reference for this topic.
     So, instead of checking immediately, we emit a constraint.
 
   * What does it mean for a type to be concrete?
-    Note [Concrete types]
+    Note [Concrete types] explains what it means for a type to be concrete.
+
+    To compute which representation to use for a type, `typePrimRep` expects
+    its kind to be concrete: something specific like `BoxedRep Lifted` or
+    `IntRep`; certainly not a type involving type variables or type families.
+
+  * What constraints do we emit?
     Note [The Concrete mechanism]
 
-    The predicate 'Concrete# ty' is satisfied when we can produce
-    a coercion
+    Instead of simply checking that a type `ty` is concrete (i.e. computing
+    'isConcrete`), we emit an equality constraint:
 
-      co :: ty ~ concrete_ty
+       co :: ty ~# concrete_ty
 
-    where 'concrete_ty' consists only of concrete types (no type variables,
-    no type families).
+    where 'concrete_ty' is a concrete metavariable: a metavariable whose 'MetaInfo'
+    is 'ConcreteTv', signifying that it can only be unified with a concrete type.
 
-    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).
+    The Note explains that this allows us to accept more programs. The Note
+    also 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`.
 
@@ -72,42 +92,29 @@ as a central point of reference for this topic.
 
     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?
+  * When do we emit these constraints?
     Note [hasFixedRuntimeRep]
 
-    We introduce 'Concrete#' constraints to satisfy the representation-polymorphism
+    We introduce 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
+    The Note explains precisely how and where these constraints are emitted.
 
-    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
+  * Reporting unsolved 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.
+    When we emit a constraint to enforce a fixed representation, 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 such an an unsolved Wanted constraint.
 
 Note [Representation polymorphism checking]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -157,17 +164,12 @@ has a fixed runtime representation, both in the typechecker:
      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
+Definition: a type is /concrete/ iff it is:
+            - a concrete type constructor (as defined below), or
+            - a concrete type variable (see Note [ConcreteTv] below), or
+            - an application of a concrete type to another concrete type
             See GHC.Core.Type.isConcrete
 
 Definition: a /concrete type constructor/ is defined by
@@ -182,69 +184,57 @@ Definition: a /concrete type constructor/ is defined by
 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
+   F Int, TYPE (F Int), TYPE r, a[sk]
    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
+The recursive definition of concreteness entails the following property:
 
-  Concrete# :: forall k. k -> TupleRep '[]
+Concrete Congruence Property (CCP)
+  All sub-trees of a concrete type tree are concrete.
 
-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.
+The following property also holds due to the invariant that the kind of a
+concrete metavariable is itself concrete (see Note [ConcreteTv]):
 
---------------
--- EVIDENCE --
---------------
+Concrete Kinds Property (CKP)
+  The kind of a concrete type is concrete.
 
-The evidence for a 'Concrete# ty' constraint is a nominal coercion
+The CCP and the CKP taken together mean that we never have to inspect
+in kinds to check concreteness.
 
-  co :: ty ~# concrete_ty
+Note [ConcreteTv]
+~~~~~~~~~~~~~~~~~
+A concrete metavariable is a metavariable whose 'MetaInfo' is 'ConcreteTv'.
+Similar to 'TyVarTv's which are type variables which can only be unified with
+other type variables, a 'ConcreteTv' type variable is a type variable which can
+only be unified with a concrete type (in the sense of Note [Concrete types]).
 
-where 'concrete_ty' consists only of (non-synonym) type constructors and applications
-(after expanding any vanilla type synonyms).
+INVARIANT: the kind of a concrete metavariable is concrete.
 
-  OK:
+This invariant is upheld at the time of creation of a new concrete metavariable.
 
-    TYPE FloatRep
-    TYPE (BoxedRep Lifted)
-    Type
-    TYPE (TupleRep '[ FloatRep, SumRep '[ IntRep, IntRep ] ])
+Concrete metavariables are useful for representation-polymorphism checks:
+they allow us to refer to a type whose representation is not yet known but will
+be figured out by the typechecker (see Note [The Concrete mechanism]).
 
-  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 [The Concrete mechanism]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+To check (ty :: ki) has a fixed runtime representation, we proceed as follows:
 
-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
+  - Create a new concrete metavariable `concrete_tv`, i.e. a metavariable
+    with 'ConcreteTv' 'MetaInfo' (see Note [ConcreteTv]).
 
-  Concrete# :: forall k. k -> TYPE (TupleRep '[])
+  - Emit an equality constraint:
 
-We still need a constraint that users can write in their own programs,
-so much like `(~#)` and `(~)` we also define:
+      ki ~# concrete_tv
 
-  Concrete :: forall k. k -> Constraint
+    The origin for such an equality constraint uses
+    `GHC.Tc.Types.Origin.FRROrigin`, so that we can report the appropriate
+    representation-polymorphism error if any such constraint goes unsolved.
 
-The need for user-facing 'Concrete' constraints is detailed in
-  Note [Concrete and Concrete#] in GHC.Builtin.Types.
+To solve `ki ~# concrete_ki`, we must unify `concrete_tv := concrete_ki`,
+where `concrete_ki` is some concrete type. We can then compute `kindPrimRep`
+on `concrete_ki` to compute the representation: this means `ty` indeed
+has a fixed runtime representation.
 
 -------------------------
 -- PHASE 1 and PHASE 2 --
@@ -252,15 +242,20 @@ The need for user-facing 'Concrete' constraints is detailed in
 
 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,
+In PHASE 1 (currently implemented), we enforce that we only solve the emitted
+constraints `co :: ki ~# concrete_tv` with `Refl`. This forbids any program
+which requires type family evaluation in order to determine that a 'RuntimeRep'
+is fixed. We do this using the `IsRefl#` special predicate (see Note [IsRefl#]);
+we only solve `IsRefl# a b` if `a` and `b` are equal (after zonking, but not rewriting).
+This means that it is safe to not use the coercion `co` anywhere in the program.
+PHASE 1 corresponds to calls to `hasFixedRuntimeRep_MustBeRefl` in the code: on top
+of emitting a constraint of the form `ki ~# concrete_tv`, we also emit
+`IsRefl# ki concrete_tv` to ensure we only solve the equality constraint using
+reflexivity.
+
+In PHASE 2, we lift this restriction. This means we replace a call to
+`hasFixedRuntimeRep_MustBeRefl` with a call to `hasFixedRuntimeRep`, and insert the
+obtained coercion in the typechecked result. 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
@@ -275,7 +270,7 @@ 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#`
+where 'kco' is the appropriate coercion; for example if `F Int = TYPE Int#`
 this would be:
 
   kco :: F Int ~# TYPE Int#
@@ -289,12 +284,9 @@ 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]).
+    <=>
+  there exists a concrete type `concrete_ty` (in the sense of Note [Concrete types])
+  such that we can solve `ki ~# concrete_ty`.
 
 This definition is crafted to be useful to satisfy the invariants of
 Core; see Note [Representation polymorphism invariants] in GHC.Core.
@@ -312,10 +304,11 @@ 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`,
+and emitting a 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,
+To do so, we compute the kind 'ki' of 'ty', create a new concrete metavariable
+`concrete_tv` of kind `ki`, and emit a constraint `ki ~# concrete_tv`,
 which will only be solved if we can prove that 'ty' indeed has a fixed RuntimeRep.
 
   [Wrinkle: Typed Template Haskell]
@@ -350,136 +343,134 @@ which will only be solved if we can prove that 'ty' indeed has a fixed RuntimeRe
 
     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:
+Note [IsRefl#]
+~~~~~~~~~~~~~~
+`IsRefl# :: forall k. k -> k -> TYPE (TupleRep '[])` is a constraint with no
+evidence. `IsRefl# a b' can be solved precisely when `a` and `b` are equal (up to zonking,
+but __without__ any rewriting).
 
-          Concrete# (TYPE (BoxedRep Lifted))
-          ==> (decompose)
-          Concrete# (BoxedRep Lifted)
-          ==> (decompose)
-          Concrete# Lifted
-          ==> (decompose)
-          <nothing, since Lifted is nullary>
+That is, if we have a type family `F` with `F Int` reducing to `Int`, we __cannot__ solve
+`IsRefl# (F Int) Int`.
 
-  2. Rewriting.
+What is the point of such a constraint? As outlined in Note [The Concrete mechanism],
+to check `ty :: ki` has a fixed RuntimeRep we create a concrete metavariable `concrete_tv`
+and emit a Wanted equality constraint
 
-      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`.
+  {co_hole} :: ki ~# concrete_tv
 
-      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.
+Then, when we fill in the coercion hole with a coercion `co`, we must make use of it
+(as that Note explains). If we don't, then we can only safely discard it if it is
+reflexive. Therefore, whenever we perform a representation polymorphism check but also
+discard the resulting coercion, we also emit a special constraint `IsRefl# ki concrete_tv`.
+See 'hasFixedRuntimeRep_MustBeRefl', which calls 'hasFixedRuntimeRep', and thenemits
+an 'IsRefl#' constraint to ensure that discarding the coercion is safe.
 -}
 
--- | Evidence for a `Concrete#` constraint:
--- essentially a 'ConcreteHole' (a coercion hole) that will be filled later,
--- except:
+-- | Like 'hasFixedRuntimeRep', but we insist that the obtained coercion must be 'Refl'.
 --
---   - 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@.
+-- This is useful if we are not actually going to use the coercion returned
+-- from 'hasFixedRuntimeRep'; it would generally be unsound to allow a non-reflexive
+-- coercion but not actually make use of it in a cast. See Note [IsRefl#].
 --
--- If this isn't immediately obvious, for instance if the 'RuntimeRep'
--- is hidden under a type-family application such as
+-- The goal is to eliminate all uses of this function and replace them with
+-- 'hasFixedRuntimeRep', making use of the returned coercion.
+hasFixedRuntimeRep_MustBeRefl :: FRROrigin -> TcType -> TcM ()
+hasFixedRuntimeRep_MustBeRefl frr_orig ty
+  = do { -- STEP 1: check that the type has a fixed 'RuntimeRep'.
+         mb_co <- hasFixedRuntimeRep frr_orig ty
+         -- STEP 2: ensure that we only solve using a reflexive coercion.
+       ; case mb_co of
+           -- If the coercion is immediately reflexive: we're OK.
+       { Nothing -> return ()
+           -- Otherwise: emit an @IsRefl#@ constraint.
+           -- This means we are free to discard the coercion.
+       ; Just (ki, _co, concrete_kv) ->
+    do { isRefl_ctev <- newWanted (FixedRuntimeRepOrigin ty frr_orig)
+                                  (Just KindLevel) $
+                          mkIsReflPrimPred ki (mkTyVarTy concrete_kv)
+       ; emitSimple $ mkNonCanonical isRefl_ctev } } }
+
+-- | Given a type @ty :: ki@, this function ensures that @ty@
+-- has a __fixed__ 'RuntimeRep', by emitting a new equality constraint
+-- @ki ~ concrete_tv@ for a concrete metavariable @concrete_tv@.
 --
--- > 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
+-- Returns a coercion @co :: ki ~# concrete_tv@ as evidence.
+-- If @ty@ obviously has a fixed 'RuntimeRep', e.g @ki = IntRep@,
+-- then this function immediately returns 'Nothing'
+-- instead of emitting a new constraint.
+hasFixedRuntimeRep :: FRROrigin -- ^ Context to be reported to the user
+                                -- if the type ends up not having a fixed
+                                -- 'RuntimeRep' (unsolved Wanted constraint).
+                   -> TcType    -- ^ The type to check (we only look at its kind).
+                   -> TcM (Maybe (TcType, TcCoercion, TcTyVar) )
+                        -- ^ @Just ( ki, co, concrete_tv )@
+                        -- where @co :: ki ~# concrete_ty@ is evidence that
+                        -- the type @ty :: ki@ has a fixed 'RuntimeRep',
+                        -- or 'Nothing' if 'ki' responds 'True' to 'isConcrete',
+                        -- (i.e. we can take @co = Refl@).
+hasFixedRuntimeRep frr_orig ty
   = 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
+          -- Shortcut: check for 'Type' and 'UnliftedType' type synonyms.
+          | TyConApp tc [] <- ki
+          , tc == liftedTypeKindTyCon || tc == unliftedTypeKindTyCon
+          -> return Nothing
 
           -- See [Wrinkle: Typed Template Haskell] in Note [hasFixedRuntimeRep].
           | Brack _ (TcPending {}) <- th_stage
-          -> return ConcreteTypedTHNoEvidence
+          -> return Nothing
 
-          -- 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 } }
+          -- Ensure that the kind 'ki' of 'ty' is concrete.
+          -> emitNewConcreteWantedEq_maybe orig ki
+              -- NB: the kind of 'ki' is 'Data.Kind.Type', which is concrete.
+              -- This means that the invariant required to call
+              -- 'newConcreteTyVar' is satisfied.
+       }
   where
-    ki :: Kind
+    ki :: TcKind
     ki = typeKind ty
+    orig :: CtOrigin
+    orig = FixedRuntimeRepOrigin ty frr_orig
 
--- | Create a new 'Concrete#' constraint.
--- Returns the evidence, a metavariable which will be filled in with a
--- guaranteed-concrete type, and a Wanted CtEvidence
-newConcretePrimWanted :: CtLoc -> Type -> TcM (ConcreteHole, TcType, CtEvidence)
-newConcretePrimWanted loc ty
-  = do { let
-           ki :: Kind
-           ki = typeKind ty
-       ; (hole, concrete_ty) <- newConcreteHole ki ty
-       ; let
-           wantedCtEv :: CtEvidence
-           wantedCtEv =
-             CtWanted
-               { ctev_dest = HoleDest hole
-               , ctev_pred = mkTyConApp concretePrimTyCon [ki, ty]
-               , ctev_rewriters = emptyRewriterSet
-               , ctev_loc  = loc
-               }
-        ; return (hole, concrete_ty, wantedCtEv) }
+-- | Create a new metavariable, of the given kind, which can only be unified
+-- with a concrete type.
+--
+-- Invariant: the kind must be concrete, as per Note [ConcreteTv].
+-- This is checked with an assertion.
+newConcreteTyVar :: HasDebugCallStack => TcKind -> TcM TcTyVar
+newConcreteTyVar kind =
+  assertPpr (isConcrete kind)
+    (text "newConcreteTyVar: non-concrete kind" <+> ppr kind)
+  $ newAnonMetaTyVar ConcreteTv kind
+
+-- | Create a new concrete metavariable @concrete_tv@ and emit a new non-canonical Wanted
+-- equality constraint @ty ~# concrete_tv@ with the given 'CtOrigin'.
+--
+-- Short-cut: if the type responds 'True' to 'isConcrete', then
+-- we already know it is concrete, so don't emit any new constraints,
+-- and return 'Nothing'.
+--
+-- Invariant: the kind of the supplied type must be concrete.
+--
+-- We also assume the provided type is already at the kind-level.
+--(This only matters for error messages.)
+emitNewConcreteWantedEq_maybe :: CtOrigin -> TcType -> TcM (Maybe (TcType, TcCoercion, TcTyVar))
+emitNewConcreteWantedEq_maybe orig ty
+  -- The input type is already concrete: no need to do anything.
+  -- Return 'Nothing', indicating that reflexivity is valid evidence.
+  | isConcrete ty
+  = return Nothing
+  -- Otherwise: create a new concrete metavariable and emit a new Wanted equality constraint.
+  | otherwise
+  = do { concrete_tv <- newConcreteTyVar ki
+       ; co <- emitWantedEq orig KindLevel Nominal ty (mkTyVarTy concrete_tv)
+                        --       ^^^^^^^^^ we assume 'ty' is at the kind level.
+                        -- (For representation polymorphism checks, we are always checking a kind.)
+       ; return $ Just (ty, co, concrete_tv) }
+  where
+    ki :: TcKind
+    ki = typeKind ty
 
 {-***********************************************************************
 *                                                                       *
@@ -489,9 +480,9 @@ newConcretePrimWanted loc ty
 
 -- | 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.
+-- 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
@@ -503,5 +494,8 @@ mkWpFun WpHole       (WpCast co2) (Scaled w t1) _  _ = return $ WpCast (mkTcFunC
 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)
+  = 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/Instantiate.hs b/compiler/GHC/Tc/Utils/Instantiate.hs
index 4193514665..78c7ad4c12 100644
--- a/compiler/GHC/Tc/Utils/Instantiate.hs
+++ b/compiler/GHC/Tc/Utils/Instantiate.hs
@@ -97,7 +97,7 @@ import GHC.Unit.External
 
 import Data.List ( mapAccumL )
 import qualified Data.List.NonEmpty as NE
-import Control.Monad( when, unless, void )
+import Control.Monad( when, unless )
 import Data.Function ( on )
 
 {-
@@ -825,7 +825,7 @@ hasFixedRuntimeRepRes std_nm user_expr ty = mapM_ do_check mb_arity
    do_check :: Arity -> TcM ()
    do_check arity =
      let res_ty = nTimes arity (snd . splitPiTy) ty
-     in void $ hasFixedRuntimeRep (FRRArrow $ ArrowFun user_expr) res_ty
+     in hasFixedRuntimeRep_MustBeRefl (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
diff --git a/compiler/GHC/Tc/Utils/TcMType.hs b/compiler/GHC/Tc/Utils/TcMType.hs
index cbbdcdfb47..8c59e30d95 100644
--- a/compiler/GHC/Tc/Utils/TcMType.hs
+++ b/compiler/GHC/Tc/Utils/TcMType.hs
@@ -197,12 +197,14 @@ newEvVar ty = do { name <- newSysName (predTypeOccName ty)
 -- | Create a new Wanted constraint with the given 'CtLoc'.
 newWantedWithLoc :: CtLoc -> PredType -> TcM CtEvidence
 newWantedWithLoc loc pty
-  = do d <- case classifyPredType pty of
-              EqPred {} -> HoleDest  <$> newCoercionHole pty
-              SpecialPred ConcretePrimPred ty ->
-                HoleDest <$> (fst <$> newConcreteHole (typeKind ty) ty)
-              _ -> EvVarDest <$> newEvVar pty
-       return $ CtWanted { ctev_dest      = d
+  = do dst <- case classifyPredType pty of
+                EqPred {}
+                  -> HoleDest <$> newCoercionHole pty
+                SpecialPred s
+                  -> case s of
+                      IsReflPrimPred {} -> return NoDest
+                _ -> EvVarDest <$> newEvVar pty
+       return $ CtWanted { ctev_dest      = dst
                          , ctev_pred      = pty
                          , ctev_loc       = loc
                          , ctev_rewriters = emptyRewriterSet }
@@ -229,9 +231,6 @@ cloneWantedCtEv ctev@(CtWanted { ctev_pred = pty, ctev_dest = HoleDest _ })
   | isEqPrimPred pty
   = do { co_hole <- newCoercionHole pty
        ; return (ctev { ctev_dest = HoleDest co_hole }) }
-  | SpecialPred ConcretePrimPred ty <- classifyPredType pty
-  = do { (co_hole, _) <- newConcreteHole (typeKind ty) ty
-       ; return (ctev { ctev_dest = HoleDest co_hole }) }
   | otherwise
   = pprPanic "cloneWantedCtEv" (ppr pty)
 cloneWantedCtEv ctev = return ctev
@@ -333,9 +332,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")
+    SpecialPred s    ->
+      case s of
+        IsReflPrimPred {} -> mkVarOccFS (fsLit "rfl")
 
 -- | 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
@@ -865,6 +864,7 @@ metaInfoToTyVarName  meta_info =
        TyVarTv        -> fsLit "a"
        RuntimeUnkTv   -> fsLit "r"
        CycleBreakerTv -> fsLit "b"
+       ConcreteTv     -> fsLit "c"
 
 newAnonMetaTyVar :: MetaInfo -> Kind -> TcM TcTyVar
 newAnonMetaTyVar mi = newNamedAnonMetaTyVar (metaInfoToTyVarName mi) mi
@@ -2712,9 +2712,10 @@ tidyEvVar env var = updateIdTypeAndMult (tidyType env) var
 -- 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.
+-- Unlike the other representation polymorphism checks, which can emit
+-- new Wanted constraints to be solved by the constraint solver, this function
+-- does not emit any constraints: 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 ()
diff --git a/compiler/GHC/Tc/Utils/TcType.hs b/compiler/GHC/Tc/Utils/TcType.hs
index 807ad0ab56..b01f72b185 100644
--- a/compiler/GHC/Tc/Utils/TcType.hs
+++ b/compiler/GHC/Tc/Utils/TcType.hs
@@ -41,6 +41,7 @@ module GHC.Tc.Utils.TcType (
   MetaDetails(Flexi, Indirect), MetaInfo(..), skolemSkolInfo,
   isImmutableTyVar, isSkolemTyVar, isMetaTyVar,  isMetaTyVarTy, isTyVarTy,
   tcIsTcTyVar, isTyVarTyVar, isOverlappableTyVar,  isTyConableTyVar,
+  isConcreteTyVar,
   isAmbiguousTyVar, isCycleBreakerTyVar, metaTyVarRef, metaTyVarInfo,
   isFlexi, isIndirect, isRuntimeUnkSkol,
   metaTyVarTcLevel, setMetaTyVarTcLevel, metaTyVarTcLevel_maybe,
@@ -566,21 +567,27 @@ data MetaDetails
   | Indirect TcType
 
 data MetaInfo
-   = TauTv         -- This MetaTv is an ordinary unification variable
+   = TauTv         -- ^ This MetaTv is an ordinary unification variable
                    -- A TauTv is always filled in with a tau-type, which
                    -- never contains any ForAlls.
 
-   | TyVarTv       -- A variant of TauTv, except that it should not be
+   | TyVarTv       -- ^ A variant of TauTv, except that it should not be
                    --   unified with a type, only with a type variable
                    -- See Note [TyVarTv] in GHC.Tc.Utils.TcMType
 
-   | RuntimeUnkTv  -- A unification variable used in the GHCi debugger.
+   | RuntimeUnkTv  -- ^ A unification variable used in the GHCi debugger.
                    -- It /is/ allowed to unify with a polytype, unlike TauTv
 
    | CycleBreakerTv  -- Used to fix occurs-check problems in Givens
                      -- See Note [Type variable cycles] in
                      -- GHC.Tc.Solver.Canonical
 
+   | ConcreteTv
+        -- ^ A unification variable that can only be unified
+        -- with a concrete type, in the sense of
+        -- Note [Concrete types] in GHC.Tc.Utils.Concrete.
+        -- See Note [ConcreteTv] in GHC.Tc.Utils.Concrete.
+
 instance Outputable MetaDetails where
   ppr Flexi         = text "Flexi"
   ppr (Indirect ty) = text "Indirect" <+> ppr ty
@@ -590,6 +597,7 @@ instance Outputable MetaInfo where
   ppr TyVarTv        = text "tyv"
   ppr RuntimeUnkTv   = text "rutv"
   ppr CycleBreakerTv = text "cbv"
+  ppr ConcreteTv     = text "conc"
 
 {- *********************************************************************
 *                                                                      *
@@ -1081,6 +1089,18 @@ isCycleBreakerTyVar tv
   | otherwise
   = False
 
+-- | Is this type variable a concrete type variable, i.e.
+-- it is a metavariable with 'ConcreteTv' 'MetaInfo'?
+--
+-- Works with both 'TyVar' and 'TcTyVar'.
+isConcreteTyVar :: TcTyVar -> Bool
+isConcreteTyVar tv
+  | isTcTyVar tv
+  , MetaTv { mtv_info = ConcreteTv } <- tcTyVarDetails tv
+  = True
+  | otherwise
+  = False
+
 isMetaTyVarTy :: TcType -> Bool
 isMetaTyVarTy (TyVarTy tv) = isMetaTyVar tv
 isMetaTyVarTy _            = False
@@ -1892,7 +1912,9 @@ isImprovementPred ty
       ClassPred cls _    -> classHasFds cls
       IrredPred {}       -> True -- Might have equalities after reduction?
       ForAllPred {}      -> False
-      SpecialPred {}     -> False
+      SpecialPred s      ->
+        case s of
+          IsReflPrimPred {} -> False
 
 {- Note [Expanding superclasses]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
diff --git a/compiler/GHC/Tc/Utils/TcType.hs-boot b/compiler/GHC/Tc/Utils/TcType.hs-boot
index 08602fa5ac..4d09c1e7e1 100644
--- a/compiler/GHC/Tc/Utils/TcType.hs-boot
+++ b/compiler/GHC/Tc/Utils/TcType.hs-boot
@@ -13,6 +13,7 @@ pprTcTyVarDetails :: TcTyVarDetails -> SDoc
 vanillaSkolemTvUnk :: HasCallStack => TcTyVarDetails
 isMetaTyVar :: TcTyVar -> Bool
 isTyConableTyVar :: TcTyVar -> Bool
+isConcreteTyVar :: TcTyVar -> Bool
 
 tcEqType :: HasDebugCallStack => Type -> Type -> Bool
 
diff --git a/compiler/GHC/Tc/Utils/Unify.hs b/compiler/GHC/Tc/Utils/Unify.hs
index 4a5ef151b7..7bd489dc50 100644
--- a/compiler/GHC/Tc/Utils/Unify.hs
+++ b/compiler/GHC/Tc/Utils/Unify.hs
@@ -1479,9 +1479,9 @@ uUnfilledVar2 origin t_or_k swapped tv1 ty2
 
     defer = unSwap swapped (uType_defer t_or_k origin) ty1 ty2
 
--- | Checks (TYVAR-TV) and (COERCION-HOLE) of Note [Unification preconditions];
--- returns True if these conditions are satisfied. But see the Note for other
--- preconditions, too.
+-- | Checks (TYVAR-TV), (COERCION-HOLE) and (CONCRETE) of
+-- Note [Unification preconditions]; returns True if these conditions
+-- are satisfied. But see the Note for other preconditions, too.
 canSolveByUnification :: MetaInfo -> TcType  -- zonked
                       -> Bool
 canSolveByUnification _    xi
@@ -1490,15 +1490,18 @@ canSolveByUnification _    xi
 canSolveByUnification info xi
   = case info of
       CycleBreakerTv -> False
-      TyVarTv -> case tcGetTyVar_maybe xi of
-                   Nothing -> False
-                   Just tv -> case tcTyVarDetails tv of -- (TYVAR-TV) wrinkle
-                                 MetaTv { mtv_info = info }
-                                            -> case info of
-                                                 TyVarTv -> True
-                                                 _       -> False
-                                 SkolemTv {} -> True
-                                 RuntimeUnk  -> True
+      ConcreteTv     -> isConcrete xi -- (CONCRETE) check
+      TyVarTv ->
+        case tcGetTyVar_maybe xi of
+           Nothing -> False
+           Just tv ->
+             case tcTyVarDetails tv of -- (TYVAR-TV) wrinkle
+                SkolemTv {} -> True
+                RuntimeUnk  -> True
+                MetaTv { mtv_info = info } ->
+                  case info of
+                    TyVarTv -> True
+                    _       -> False
       _ -> True
 
 swapOverTyVars :: Bool -> TcTyVar -> TcTyVar -> Bool
@@ -1541,8 +1544,9 @@ lhsPriority tv
       MetaTv { mtv_info = info } -> case info of
                                      CycleBreakerTv -> 0
                                      TyVarTv        -> 1
-                                     TauTv          -> 2
-                                     RuntimeUnkTv   -> 3
+                                     ConcreteTv     -> 2
+                                     TauTv          -> 3
+                                     RuntimeUnkTv   -> 4
 
 {- Note [Unification preconditions]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1552,7 +1556,7 @@ unify alpha := ty?
 This note only applied to /homogeneous/ equalities, in which both
 sides have the same kind.
 
-There are four reasons not to unify:
+There are five reasons not to unify:
 
 1. (SKOL-ESC) Skolem-escape
    Consider the constraint
@@ -1590,7 +1594,16 @@ There are four reasons not to unify:
 
    * CycleBreakerTv: never unified, except by restoreTyVarCycles.
 
-4. (COERCION-HOLE) Confusing coercion holes
+4. (CONCRETE) A ConcreteTv can only unify with a concrete type,
+    by definition.
+
+    That is, if we have `rr[conc] ~ F Int`, we can't unify
+    `rr` with `F Int`, so we hold off on unifying.
+    Note however that the equality might get rewritten; for instance
+    if we can rewrite `F Int` to a concrete type, say `FloatRep`,
+    then we will have `rr[conc] ~ FloatRep` and we can unify `rr ~ FloatRep`.
+
+5. (COERCION-HOLE) Confusing coercion holes
    Suppose our equality is
      (alpha :: k) ~ (Int |> {co})
    where co :: Type ~ k is an unsolved wanted. Note that this
@@ -1605,6 +1618,7 @@ There are four reasons not to unify:
    This is expanded as Wrinkle (2) in Note [Equalities with incompatible kinds]
    in GHC.Tc.Solver.Canonical.
 
+
 Needless to say, all there are wrinkles:
 
 * (SKOL-ESC) Promotion.  Given alpha[n] ~ ty, what if beta[k] is free
@@ -1678,12 +1692,16 @@ So we look for a positive reason to swap, using a three-step test:
        a TyVarTv with a TauTv, because then the TyVarTv could (transitively)
        get a non-tyvar type. So give these a low priority: 1.
 
+  - ConcreteTv: These are like TauTv, except they can only unify with
+    a concrete type. So we want to be able to write to them, but not quite
+    as much as TauTvs: 2.
+
   - TauTv: This is the common case; we want these on the left so that they
-       can be written to: 2.
+       can be written to: 3.
 
   - RuntimeUnkTv: These aren't really meta-variables used in type inference,
        but just a convenience in the implementation of the GHCi debugger.
-       Eagerly write to these: 3. See Note [RuntimeUnkTv] in
+       Eagerly write to these: 4. See Note [RuntimeUnkTv] in
        GHC.Runtime.Heap.Inspect.
 
 * Names. If the level and priority comparisons are all