Fix unification of ConcreteTvs, removing IsRefl#

This patch fixes the unification of concrete type variables.
The subtlety was that unifying concrete metavariables is more subtle
than other metavariables, as decomposition is possible. See the Note
[Unifying concrete metavariables], which explains how we unify a
concrete type variable with a type 'ty' by concretising 'ty', using
the function 'GHC.Tc.Utils.Concrete.concretise'.

This can be used to perform an eager syntactic check for concreteness,
allowing us to remove the IsRefl# special predicate. Instead of emitting
two constraints `rr ~# concrete_tv` and `IsRefl# rr concrete_tv`, we
instead concretise 'rr'. If this succeeds we can fill 'concrete_tv',
and otherwise we directly emit an error message to the typechecker
environment instead of deferring. We still need the error message
to be passed on (instead of directly thrown), as we might benefit from
further unification in which case we will need to zonk the stored types.
To achieve this, we change the 'wc_holes' field of 'WantedConstraints'
to 'wc_errors', which stores general delayed errors. For the moement,
a delayed error is either a hole, or a syntactic equality error.

hasFixedRuntimeRep_MustBeRefl is now hasFixedRuntimeRep_syntactic, and
hasFixedRuntimeRep has been refactored to directly return the most
useful coercion for PHASE 2 of FixedRuntimeRep.

This patch also adds a field ir_frr to the InferResult datatype,
holding a value of type Maybe FRROrigin. When this value is not
Nothing, this means that we must fill the ir_ref field with a type
which has a fixed RuntimeRep.
When it comes time to fill such an ExpType, we ensure that the type
has a fixed RuntimeRep by performing a representation-polymorphism
check with the given FRROrigin
This is similar to what we already do to ensure we fill an Infer
ExpType with a type of the correct TcLevel.
This allows us to properly perform representation-polymorphism checks
on 'Infer' 'ExpTypes'.

The fillInferResult function had to be moved to GHC.Tc.Utils.Unify
to avoid a cyclic import now that it calls hasFixedRuntimeRep.

This patch also changes the code in matchExpectedFunTys to make use
of the coercions, which is now possible thanks to the previous change.
This implements PHASE 2 of FixedRuntimeRep in some situations.
For example, the test cases T13105 and T17536b are now both accepted.

Fixes #21239 and #21325

-------------------------
Metric Decrease:
    T18223
    T5631
-------------------------

50 files changed, 373 insertions, 272 deletions

diff --git a/testsuite/tests/linters/notes.stdout b/testsuite/tests/linters/notes.stdout
index 224fade77a..16fd6a02ac 100644
--- a/testsuite/tests/linters/notes.stdout
+++ b/testsuite/tests/linters/notes.stdout
@@ -83,7 +83,6 @@ ref    compiler/GHC/Tc/Instance/Family.hs:515:35:     Note [Constrained family i
 ref    compiler/GHC/Tc/Module.hs:698:15:     Note [Extra dependencies from .hs-boot files]
 ref    compiler/GHC/Tc/Module.hs:1904:19:     Note [Root-main id]
 ref    compiler/GHC/Tc/Module.hs:1974:6:     Note [Root-main id]
-ref    compiler/GHC/Tc/Solver.hs:2541:36:     Note [Kind generalisation and SigTvs]
 ref    compiler/GHC/Tc/Solver/Canonical.hs:1229:33:     Note [Canonical LHS]
 ref    compiler/GHC/Tc/Solver/Interact.hs:1638:9:     Note [No touchables as FunEq RHS]
 ref    compiler/GHC/Tc/Solver/Interact.hs:2292:12:     Note [The equality class story]
diff --git a/testsuite/tests/rep-poly/RepPolyArgument.hs b/testsuite/tests/rep-poly/RepPolyArgument.hs
new file mode 100644
index 0000000000..4f72e89e32
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyArgument.hs
@@ -0,0 +1,10 @@
+{-# LANGUAGE ExplicitForAll, PolyKinds, StandaloneKindSignatures, TypeApplications, TypeFamilies #-}
+
+module RepPolyArgument where
+
+import GHC.Exts
+
+type R :: forall k. k
+data family R
+
+foo = undefined (undefined @(R @RuntimeRep))
diff --git a/testsuite/tests/rep-poly/RepPolyArgument.stderr b/testsuite/tests/rep-poly/RepPolyArgument.stderr
new file mode 100644
index 0000000000..b5050fc6a5
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyArgument.stderr
@@ -0,0 +1,13 @@
+
+RepPolyArgument.hs:10:18: error:
+    • The argument ‘(undefined @(R @RuntimeRep))’ of ‘undefined’
+      does not have a fixed runtime representation.
+      Its type is:
+        t0 :: TYPE c0
+      Cannot unify ‘R’ with the type variable ‘c0’
+      because it is not a concrete ‘RuntimeRep’.
+    • In the first argument of ‘undefined’, namely
+        ‘(undefined @(R @RuntimeRep))’
+      In the expression: undefined (undefined @(R @RuntimeRep))
+      In an equation for ‘foo’:
+          foo = undefined (undefined @(R @RuntimeRep))
diff --git a/testsuite/tests/rep-poly/RepPolyArrowFun.stderr b/testsuite/tests/rep-poly/RepPolyArrowFun.stderr
index db14b272f3..a79570822a 100644
--- a/testsuite/tests/rep-poly/RepPolyArrowFun.stderr
+++ b/testsuite/tests/rep-poly/RepPolyArrowFun.stderr
@@ -1,34 +1,27 @@
 
-RepPolyArrowFun.hs:29:9: error:
-    • • The return type of the arrow function
-          ‘arr’
+RepPolyArrowFun.hs:29:19: error:
+    • • The function in the first order arrow application of
+          ‘undefined’
+        to
+          ‘x’
         does not have a fixed runtime representation.
         Its type is:
-          arr b c :: TYPE r
+          arr a a :: TYPE r
+      • The return type of the arrow function
+          ‘first’
+        does not have a fixed runtime representation.
+        Its type is:
+          arr (b, d) (c, d) :: TYPE r
       • The return type of the arrow function
           ‘(>>>)’
         does not have a fixed runtime representation.
         Its type is:
-          arr a1 c4 :: TYPE r
+          arr a c :: TYPE r
       • The return type of the arrow function
-          ‘first’
+          ‘arr’
         does not have a fixed runtime representation.
         Its type is:
-          arr (b1, d) (c5, d) :: TYPE r
-    • When checking that ‘arr’ (needed by a syntactic construct)
-        has the required type: forall b c. (b -> c) -> arr b c
-        arising from a proc expression at RepPolyArrowFun.hs:29:9-32
-      In the expression: proc x -> undefined -< x
-      In an equation for ‘foo’: foo _ = proc x -> undefined -< x
-
-RepPolyArrowFun.hs:29:19: error:
-    • The function in the first order arrow application of
-        ‘undefined’
-      to
-        ‘x’
-      does not have a fixed runtime representation.
-      Its type is:
-        arr a a :: TYPE r
+          arr b c :: TYPE r
     • In the command: undefined -< x
       In the expression: proc x -> undefined -< x
       In an equation for ‘foo’: foo _ = proc x -> undefined -< x
diff --git a/testsuite/tests/rep-poly/RepPolyBackpack1.stderr b/testsuite/tests/rep-poly/RepPolyBackpack1.stderr
index f521ada91c..e4a128ea4d 100644
--- a/testsuite/tests/rep-poly/RepPolyBackpack1.stderr
+++ b/testsuite/tests/rep-poly/RepPolyBackpack1.stderr
@@ -3,24 +3,7 @@
   [2 of 2] Compiling NumberStuff      ( number-unknown\NumberStuff.hs, nothing )
 
 RepPolyBackpack1.bkp:17:5: error:
-    The first pattern in the equation for ‘funcA’
+    The second pattern in the equation for ‘funcA’
     does not have a fixed runtime representation.
     Its type is:
       Number l :: TYPE (Rep l)
-
-RepPolyBackpack1.bkp:17:17: error:
-    • The argument ‘x’ of ‘plus’
-      does not have a fixed runtime representation.
-      Its type is:
-        Number l :: TYPE (Rep l)
-    • In the expression: plus x (multiply x y)
-      In an equation for ‘funcA’: funcA x y = plus x (multiply x y)
-
-RepPolyBackpack1.bkp:17:25: error:
-    • The argument ‘x’ of ‘multiply’
-      does not have a fixed runtime representation.
-      Its type is:
-        Number l :: TYPE (Rep l)
-    • In the second argument of ‘plus’, namely ‘(multiply x y)’
-      In the expression: plus x (multiply x y)
-      In an equation for ‘funcA’: funcA x y = plus x (multiply x y)
diff --git a/testsuite/tests/rep-poly/RepPolyBinder.stderr b/testsuite/tests/rep-poly/RepPolyBinder.stderr
index 33802a0621..177a4865e6 100644
--- a/testsuite/tests/rep-poly/RepPolyBinder.stderr
+++ b/testsuite/tests/rep-poly/RepPolyBinder.stderr
@@ -8,12 +8,3 @@ RepPolyBinder.hs:11:1: error:
       does not have a fixed runtime representation.
       Its type is:
         b :: TYPE rep2
-
-RepPolyBinder.hs:11:17: error:
-    • The first argument of the view pattern
-        myId
-      does not have a fixed runtime representation.
-      Its type is:
-        b :: TYPE rep2
-    • In the pattern: myId -> bndr_b
-      In an equation for ‘foo’: foo bndr_a pat@(myId -> bndr_b) = ()
diff --git a/testsuite/tests/rep-poly/RepPolyCase2.stderr b/testsuite/tests/rep-poly/RepPolyCase2.stderr
index f1f59116c9..e84b8db2ed 100644
--- a/testsuite/tests/rep-poly/RepPolyCase2.stderr
+++ b/testsuite/tests/rep-poly/RepPolyCase2.stderr
@@ -4,8 +4,5 @@ RepPolyCase2.hs:33:7: error:
       does not have a fixed runtime representation.
       Its type is:
         Unbox Int :: TYPE (Rep Int)
-      NB: GHC does not (yet) support rewriting in runtime representations.
-      Please comment on GHC ticket #13105 if this is causing you trouble.
-      <https://gitlab.haskell.org/ghc/ghc/-/issues/13105>
     • In the expression: case unbox (3 :: Int) of _ -> ()
       In an equation for ‘x’: x _ = case unbox (3 :: Int) of _ -> ()
diff --git a/testsuite/tests/rep-poly/RepPolyDoBind.stderr b/testsuite/tests/rep-poly/RepPolyDoBind.stderr
index b3541dc5d5..bc3bd34465 100644
--- a/testsuite/tests/rep-poly/RepPolyDoBind.stderr
+++ b/testsuite/tests/rep-poly/RepPolyDoBind.stderr
@@ -4,7 +4,9 @@ RepPolyDoBind.hs:26:3: error:
         arising from a do statement
       does not have a fixed runtime representation.
       Its type is:
-        ma0 :: TYPE rep
+        ma0 :: TYPE c0
+      Cannot unify ‘rep’ with the type variable ‘c0’
+      because it is not a concrete ‘RuntimeRep’.
     • In a stmt of a 'do' block: a <- undefined
       In the expression:
         do a <- undefined
@@ -13,3 +15,5 @@ RepPolyDoBind.hs:26:3: error:
           foo _
             = do a <- undefined
                  return ()
+    • Relevant bindings include
+        foo :: () -> ma (bound at RepPolyDoBind.hs:25:1)
diff --git a/testsuite/tests/rep-poly/RepPolyDoBody1.stderr b/testsuite/tests/rep-poly/RepPolyDoBody1.stderr
index f71deeb24b..e31d97891e 100644
--- a/testsuite/tests/rep-poly/RepPolyDoBody1.stderr
+++ b/testsuite/tests/rep-poly/RepPolyDoBody1.stderr
@@ -1,15 +1,12 @@
 
 RepPolyDoBody1.hs:24:3: error:
-    • • The first argument of the rebindable syntax operator ‘(>>)’
-          arising from a do statement
-        does not have a fixed runtime representation.
-        Its type is:
-          ma :: TYPE rep
-      • The first argument of the rebindable syntax operator ‘(>>)’
-          arising from a do statement
-        does not have a fixed runtime representation.
-        Its type is:
-          mb0 :: TYPE rep
+    • The first argument of the rebindable syntax operator ‘(>>)’
+        arising from a do statement
+      does not have a fixed runtime representation.
+      Its type is:
+        ma0 :: TYPE c0
+      Cannot unify ‘rep’ with the type variable ‘c0’
+      because it is not a concrete ‘RuntimeRep’.
     • In a stmt of a 'do' block: undefined :: ma
       In the expression:
         do undefined :: ma
@@ -18,3 +15,5 @@ RepPolyDoBody1.hs:24:3: error:
           foo _
             = do undefined :: ma
                return ()
+    • Relevant bindings include
+        foo :: () -> ma (bound at RepPolyDoBody1.hs:23:1)
diff --git a/testsuite/tests/rep-poly/RepPolyDoBody2.stderr b/testsuite/tests/rep-poly/RepPolyDoBody2.stderr
index 1d28c20d26..40a033a33d 100644
--- a/testsuite/tests/rep-poly/RepPolyDoBody2.stderr
+++ b/testsuite/tests/rep-poly/RepPolyDoBody2.stderr
@@ -4,7 +4,9 @@ RepPolyDoBody2.hs:23:3: error:
         arising from a do statement
       does not have a fixed runtime representation.
       Its type is:
-        mb0 :: TYPE rep
+        mb0 :: TYPE c0
+      Cannot unify ‘rep’ with the type variable ‘c0’
+      because it is not a concrete ‘RuntimeRep’.
     • In a stmt of a 'do' block: undefined :: ()
       In the expression:
         do undefined :: ()
@@ -13,3 +15,5 @@ RepPolyDoBody2.hs:23:3: error:
           foo _
             = do undefined :: ()
                return ()
+    • Relevant bindings include
+        foo :: () -> ma (bound at RepPolyDoBody2.hs:22:1)
diff --git a/testsuite/tests/rep-poly/RepPolyInferPatBind.hs b/testsuite/tests/rep-poly/RepPolyInferPatBind.hs
new file mode 100644
index 0000000000..ebf161ad60
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyInferPatBind.hs
@@ -0,0 +1,21 @@
+{-# LANGUAGE Haskell2010 #-}
+
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UnboxedTuples #-}
+
+module RepPolyInferPatBind where
+
+import Data.Kind
+import GHC.Exts
+
+type R :: RuntimeRep
+type family R where {}
+
+type T :: TYPE R
+type family T where {}
+
+(x :: T) = x
diff --git a/testsuite/tests/rep-poly/RepPolyInferPatBind.stderr b/testsuite/tests/rep-poly/RepPolyInferPatBind.stderr
new file mode 100644
index 0000000000..8e9f7fb032
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyInferPatBind.stderr
@@ -0,0 +1,14 @@
+
+RepPolyInferPatBind.hs:21:1: error:
+    The binder ‘x’ does not have a fixed runtime representation.
+    Its type is:
+      T :: TYPE R
+
+RepPolyInferPatBind.hs:21:2: error:
+    • The pattern binding does not have a fixed runtime representation.
+      Its type is:
+        T :: TYPE R
+    • When checking that the pattern signature: T
+        fits the type of its context: T
+      In the pattern: x :: T
+      In a pattern binding: (x :: T) = x
diff --git a/testsuite/tests/rep-poly/RepPolyInferPatSyn.hs b/testsuite/tests/rep-poly/RepPolyInferPatSyn.hs
new file mode 100644
index 0000000000..27ed7bfc25
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyInferPatSyn.hs
@@ -0,0 +1,22 @@
+{-# LANGUAGE Haskell2010 #-}
+
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UnboxedTuples #-}
+
+module RepPolyInferPatSyn where
+
+import Data.Kind
+import GHC.Exts
+
+type R :: RuntimeRep
+type family R where {}
+
+type T :: TYPE R
+type family T where {}
+
+pattern P a = (a :: T)
diff --git a/testsuite/tests/rep-poly/RepPolyInferPatSyn.stderr b/testsuite/tests/rep-poly/RepPolyInferPatSyn.stderr
new file mode 100644
index 0000000000..7e07ea88ca
--- /dev/null
+++ b/testsuite/tests/rep-poly/RepPolyInferPatSyn.stderr
@@ -0,0 +1,10 @@
+
+RepPolyInferPatSyn.hs:22:16: error:
+    • The pattern synonym argument pattern
+      does not have a fixed runtime representation.
+      Its type is:
+        T :: TYPE R
+    • When checking that the pattern signature: T
+        fits the type of its context: T
+      In the pattern: a :: T
+      In the declaration for pattern synonym ‘P’
diff --git a/testsuite/tests/rep-poly/RepPolyLeftSection2.stderr b/testsuite/tests/rep-poly/RepPolyLeftSection2.stderr
index fd9dbb31b1..b273475650 100644
--- a/testsuite/tests/rep-poly/RepPolyLeftSection2.stderr
+++ b/testsuite/tests/rep-poly/RepPolyLeftSection2.stderr
@@ -3,6 +3,10 @@ RepPolyLeftSection2.hs:14:11: error:
     • The argument ‘undefined’ of ‘f’
       does not have a fixed runtime representation.
       Its type is:
-        a :: TYPE r
+        a0 :: TYPE c0
+      Cannot unify ‘r’ with the type variable ‘c0’
+      because it is not a concrete ‘RuntimeRep’.
     • In the expression: undefined `f`
       In an equation for ‘test1’: test1 = (undefined `f`)
+    • Relevant bindings include
+        test1 :: a -> a (bound at RepPolyLeftSection2.hs:14:1)
diff --git a/testsuite/tests/rep-poly/RepPolyMagic.stderr b/testsuite/tests/rep-poly/RepPolyMagic.stderr
index 47e7ba81d3..f99d0c740a 100644
--- a/testsuite/tests/rep-poly/RepPolyMagic.stderr
+++ b/testsuite/tests/rep-poly/RepPolyMagic.stderr
@@ -4,15 +4,23 @@ RepPolyMagic.hs:12:7: error:
       The second argument of ‘seq’
       does not have a fixed runtime representation.
       Its type is:
-        b :: TYPE r
+        b0 :: TYPE c1
+      Cannot unify ‘r’ with the type variable ‘c1’
+      because it is not a concrete ‘RuntimeRep’.
     • In the expression: seq
       In an equation for ‘foo’: foo = seq
+    • Relevant bindings include
+        foo :: a -> b -> b (bound at RepPolyMagic.hs:12:1)
 
 RepPolyMagic.hs:15:7: error:
     • Unsaturated use of a representation-polymorphic primitive function.
       The second argument of ‘oneShot’
       does not have a fixed runtime representation.
       Its type is:
-        a :: TYPE r
+        a0 :: TYPE c0
+      Cannot unify ‘r’ with the type variable ‘c0’
+      because it is not a concrete ‘RuntimeRep’.
     • In the expression: oneShot
       In an equation for ‘bar’: bar = oneShot
+    • Relevant bindings include
+        bar :: (a -> a) -> a -> a (bound at RepPolyMagic.hs:15:1)
diff --git a/testsuite/tests/rep-poly/RepPolyMcBind.stderr b/testsuite/tests/rep-poly/RepPolyMcBind.stderr
index 647a8d625d..676bb543ac 100644
--- a/testsuite/tests/rep-poly/RepPolyMcBind.stderr
+++ b/testsuite/tests/rep-poly/RepPolyMcBind.stderr
@@ -4,7 +4,11 @@ RepPolyMcBind.hs:26:16: error:
         arising from a statement in a monad comprehension
       does not have a fixed runtime representation.
       Its type is:
-        ma :: TYPE rep
+        ma0 :: TYPE c0
+      Cannot unify ‘rep’ with the type variable ‘c0’
+      because it is not a concrete ‘RuntimeRep’.
     • In a stmt of a monad comprehension: x <- undefined :: ma
       In the expression: [() | x <- undefined :: ma]
       In an equation for ‘foo’: foo _ = [() | x <- undefined :: ma]
+    • Relevant bindings include
+        foo :: () -> ma (bound at RepPolyMcBind.hs:26:1)
diff --git a/testsuite/tests/rep-poly/RepPolyMcBody.stderr b/testsuite/tests/rep-poly/RepPolyMcBody.stderr
index de9848d4c6..93aca381ce 100644
--- a/testsuite/tests/rep-poly/RepPolyMcBody.stderr
+++ b/testsuite/tests/rep-poly/RepPolyMcBody.stderr
@@ -4,7 +4,11 @@ RepPolyMcBody.hs:30:16: error:
         arising from a statement in a monad comprehension
       does not have a fixed runtime representation.
       Its type is:
-        ma0 :: TYPE rep
+        ma0 :: TYPE c0
+      Cannot unify ‘rep’ with the type variable ‘c0’
+      because it is not a concrete ‘RuntimeRep’.
     • In a stmt of a monad comprehension: True
       In the expression: [() | True]
       In an equation for ‘foo’: foo _ = [() | True]
+    • Relevant bindings include
+        foo :: () -> ma (bound at RepPolyMcBody.hs:30:1)
diff --git a/testsuite/tests/rep-poly/RepPolyMcGuard.stderr b/testsuite/tests/rep-poly/RepPolyMcGuard.stderr
index a1a32f7a3a..a545b53c6c 100644
--- a/testsuite/tests/rep-poly/RepPolyMcGuard.stderr
+++ b/testsuite/tests/rep-poly/RepPolyMcGuard.stderr
@@ -1,15 +1,14 @@
 
 RepPolyMcGuard.hs:30:16: error:
-    • • The first argument of the rebindable syntax operator ‘(>>)’
-          arising from a statement in a monad comprehension
-        does not have a fixed runtime representation.
-        Its type is:
-          ma0 :: TYPE rep
-      • The first argument of the rebindable syntax operator ‘guard’
-          arising from a statement in a monad comprehension
-        does not have a fixed runtime representation.
-        Its type is:
-          a0 :: TYPE rep
+    • The first argument of the rebindable syntax operator ‘guard’
+        arising from a statement in a monad comprehension
+      does not have a fixed runtime representation.
+      Its type is:
+        a0 :: TYPE c0
+      Cannot unify ‘rep’ with the type variable ‘c0’
+      because it is not a concrete ‘RuntimeRep’.
     • In a stmt of a monad comprehension: undefined
       In the expression: [() | undefined]
       In an equation for ‘foo’: foo _ = [() | undefined]
+    • Relevant bindings include
+        foo :: () -> ma (bound at RepPolyMcGuard.hs:30:1)
diff --git a/testsuite/tests/rep-poly/RepPolyNPlusK.stderr b/testsuite/tests/rep-poly/RepPolyNPlusK.stderr
index c5e5f84662..80672387db 100644
--- a/testsuite/tests/rep-poly/RepPolyNPlusK.stderr
+++ b/testsuite/tests/rep-poly/RepPolyNPlusK.stderr
@@ -4,12 +4,3 @@ RepPolyNPlusK.hs:22:1: error:
     does not have a fixed runtime representation.
     Its type is:
       a :: TYPE rep1
-
-RepPolyNPlusK.hs:22:6: error:
-    • The first argument of the rebindable syntax operator ‘(>=)’
-        arising from the literal ‘2’
-      does not have a fixed runtime representation.
-      Its type is:
-        a :: TYPE rep1
-    • In the pattern: bndr_a+2
-      In an equation for ‘foo’: foo (bndr_a+2) = ()
diff --git a/testsuite/tests/rep-poly/RepPolyPatBind.stderr b/testsuite/tests/rep-poly/RepPolyPatBind.stderr
index 3914ea8e30..976e84e81e 100644
--- a/testsuite/tests/rep-poly/RepPolyPatBind.stderr
+++ b/testsuite/tests/rep-poly/RepPolyPatBind.stderr
@@ -1,8 +1,11 @@
 
 RepPolyPatBind.hs:18:5: error:
-    • The binder ‘x’ does not have a fixed runtime representation.
-      Its type is:
-        a :: TYPE rep
+    • • The binder ‘y’ does not have a fixed runtime representation.
+        Its type is:
+          a :: TYPE rep
+      • The binder ‘x’ does not have a fixed runtime representation.
+        Its type is:
+          a :: TYPE rep
     • In the expression:
         let
           x, y :: a
diff --git a/testsuite/tests/rep-poly/RepPolyRecordPattern.stderr b/testsuite/tests/rep-poly/RepPolyRecordPattern.stderr
index 085e2da393..11602f0285 100644
--- a/testsuite/tests/rep-poly/RepPolyRecordPattern.stderr
+++ b/testsuite/tests/rep-poly/RepPolyRecordPattern.stderr
@@ -4,10 +4,14 @@ RepPolyRecordPattern.hs:7:35: error:
       does not have a fixed runtime representation.
       Its type is:
         a :: TYPE rep
-    • The first pattern in the equation for ‘fld’
-      does not have a fixed runtime representation.
-      Its type is:
-        X a :: TYPE rep
+    • In the pattern: MkX {fld = fld}
+      In an equation for ‘fld’: fld MkX {fld = fld} = fld
+
+RepPolyRecordPattern.hs:7:35: error:
+    The first pattern in the equation for ‘fld’
+    does not have a fixed runtime representation.
+    Its type is:
+      X a :: TYPE rep
 
 RepPolyRecordPattern.hs:13:1: error:
     The first pattern in the equation for ‘upd’
diff --git a/testsuite/tests/rep-poly/RepPolyRecordUpdate.stderr b/testsuite/tests/rep-poly/RepPolyRecordUpdate.stderr
index 5cdc9205f0..157c0403bc 100644
--- a/testsuite/tests/rep-poly/RepPolyRecordUpdate.stderr
+++ b/testsuite/tests/rep-poly/RepPolyRecordUpdate.stderr
@@ -4,16 +4,23 @@ RepPolyRecordUpdate.hs:7:35: error:
       does not have a fixed runtime representation.
       Its type is:
         a :: TYPE rep
-    • The first pattern in the equation for ‘fld’
-      does not have a fixed runtime representation.
-      Its type is:
-        X a :: TYPE rep
+    • In the pattern: MkX {fld = fld}
+      In an equation for ‘fld’: fld MkX {fld = fld} = fld
+
+RepPolyRecordUpdate.hs:7:35: error:
+    The first pattern in the equation for ‘fld’
+    does not have a fixed runtime representation.
+    Its type is:
+      X a :: TYPE rep
 
 RepPolyRecordUpdate.hs:13:9: error:
     • The record update at field ‘fld’
       does not have a fixed runtime representation.
       Its type is:
-        a :: TYPE rep
-    • In the ‘fld’ field of a record
-      In the expression: x {fld = meth ()}
+        a0 :: TYPE c1
+      Cannot unify ‘rep’ with the type variable ‘c1’
+      because it is not a concrete ‘RuntimeRep’.
+    • In the expression: x {fld = meth ()}
       In an equation for ‘upd’: upd x = x {fld = meth ()}
+    • Relevant bindings include
+        upd :: X b -> X a (bound at RepPolyRecordUpdate.hs:13:1)
diff --git a/testsuite/tests/rep-poly/RepPolyRightSection.stderr b/testsuite/tests/rep-poly/RepPolyRightSection.stderr
index 62c0bdcd8d..fdc7a399fa 100644
--- a/testsuite/tests/rep-poly/RepPolyRightSection.stderr
+++ b/testsuite/tests/rep-poly/RepPolyRightSection.stderr
@@ -4,6 +4,10 @@ RepPolyRightSection.hs:14:11: error:
       The third argument of ‘rightSection’
       does not have a fixed runtime representation.
       Its type is:
-        a :: TYPE r
+        a :: TYPE c0
+      Cannot unify ‘r’ with the type variable ‘c0’
+      because it is not a concrete ‘RuntimeRep’.
     • In the expression: `g` undefined
       In an equation for ‘test2’: test2 = (`g` undefined)
+    • Relevant bindings include
+        test2 :: a -> a (bound at RepPolyRightSection.hs:14:1)
diff --git a/testsuite/tests/rep-poly/RepPolyRule1.stderr b/testsuite/tests/rep-poly/RepPolyRule1.stderr
index f2fcb378da..6250ddb098 100644
--- a/testsuite/tests/rep-poly/RepPolyRule1.stderr
+++ b/testsuite/tests/rep-poly/RepPolyRule1.stderr
@@ -1,8 +1,25 @@
 
-RepPolyRule1.hs:11:49: error:
+RepPolyRule1.hs:11:51: error:
     • The argument ‘x’ of ‘f’
       does not have a fixed runtime representation.
       Its type is:
-        a :: TYPE rep
-    • In the expression: f x
+        a1 :: TYPE c0
+      Cannot unify ‘rep’ with the type variable ‘c0’
+      because it is not a concrete ‘RuntimeRep’.
+    • In the first argument of ‘f’, namely ‘x’
+      In the expression: f x
       When checking the rewrite rule "f_id"
+    • Relevant bindings include
+        x :: a2 (bound at RepPolyRule1.hs:11:26)
+
+RepPolyRule1.hs:11:55: error:
+    • The argument ‘x’ of ‘f’
+      does not have a fixed runtime representation.
+      Its type is:
+        a1 :: TYPE c0
+      Cannot unify ‘rep’ with the type variable ‘c0’
+      because it is not a concrete ‘RuntimeRep’.
+    • In the expression: x
+      When checking the rewrite rule "f_id"
+    • Relevant bindings include
+        x :: a2 (bound at RepPolyRule1.hs:11:26)
diff --git a/testsuite/tests/rep-poly/RepPolyRule3.stderr b/testsuite/tests/rep-poly/RepPolyRule3.stderr
index cdbfcdb66b..695a4985bf 100644
--- a/testsuite/tests/rep-poly/RepPolyRule3.stderr
+++ b/testsuite/tests/rep-poly/RepPolyRule3.stderr
@@ -5,9 +5,6 @@ RepPolyRule3.hs:17:57: error:
       Its kind is:
         TYPE (F 'WordRep)
       (Use -fprint-explicit-coercions to see the full type.)
-      NB: GHC does not (yet) support rewriting in runtime representations.
-      Please comment on GHC ticket #13105 if this is causing you trouble.
-      <https://gitlab.haskell.org/ghc/ghc/-/issues/13105>
     • In the expression: g x
       When checking the rewrite rule "g_id"
 
@@ -17,8 +14,5 @@ RepPolyRule3.hs:23:52: error:
       Its kind is:
         TYPE (F 'WordRep)
       (Use -fprint-explicit-coercions to see the full type.)
-      NB: GHC does not (yet) support rewriting in runtime representations.
-      Please comment on GHC ticket #13105 if this is causing you trouble.
-      <https://gitlab.haskell.org/ghc/ghc/-/issues/13105>
     • In the expression: h x
       When checking the rewrite rule "h_id"
diff --git a/testsuite/tests/rep-poly/RepPolyTuple.stderr b/testsuite/tests/rep-poly/RepPolyTuple.stderr
index e651dca0fd..f9c1275976 100644
--- a/testsuite/tests/rep-poly/RepPolyTuple.stderr
+++ b/testsuite/tests/rep-poly/RepPolyTuple.stderr
@@ -1,9 +1,17 @@
 
 RepPolyTuple.hs:11:9: error:
-    • The tuple argument in first position
-      does not have a fixed runtime representation.
-      Its type is:
-        a :: TYPE r
+    • • The tuple argument in third position
+        does not have a fixed runtime representation.
+        Its type is:
+          a :: TYPE r
+      • The tuple argument in second position
+        does not have a fixed runtime representation.
+        Its type is:
+          a :: TYPE r
+      • The tuple argument in first position
+        does not have a fixed runtime representation.
+        Its type is:
+          a :: TYPE r
     • In the expression: (# bar (), bar (), bar () #)
       In an equation for ‘foo’:
           foo _
diff --git a/testsuite/tests/rep-poly/RepPolyTupleSection.stderr b/testsuite/tests/rep-poly/RepPolyTupleSection.stderr
index b2569ecfd6..fa2ddf93cb 100644
--- a/testsuite/tests/rep-poly/RepPolyTupleSection.stderr
+++ b/testsuite/tests/rep-poly/RepPolyTupleSection.stderr
@@ -3,6 +3,10 @@ RepPolyTupleSection.hs:11:7: error:
     • The second component of the tuple section
       does not have a fixed runtime representation.
       Its type is:
-        a :: TYPE r
+        t0 :: TYPE c0
+      Cannot unify ‘r’ with the type variable ‘c0’
+      because it is not a concrete ‘RuntimeRep’.
     • In the expression: (# 3#, #)
       In an equation for ‘foo’: foo = (# 3#, #)
+    • Relevant bindings include
+        foo :: a -> (# Int#, a #) (bound at RepPolyTupleSection.hs:11:1)
diff --git a/testsuite/tests/rep-poly/T11473.stderr b/testsuite/tests/rep-poly/T11473.stderr
index 411e074c0e..8e7b81f3e9 100644
--- a/testsuite/tests/rep-poly/T11473.stderr
+++ b/testsuite/tests/rep-poly/T11473.stderr
@@ -4,11 +4,3 @@ T11473.hs:19:1: error:
     does not have a fixed runtime representation.
     Its type is:
       a :: TYPE r
-
-T11473.hs:19:11: error:
-    • The argument ‘x’ of ‘boxed’
-      does not have a fixed runtime representation.
-      Its type is:
-        a :: TYPE r
-    • In the expression: boxed x
-      In an equation for ‘hello’: hello x = boxed x
diff --git a/testsuite/tests/rep-poly/T12709.stderr b/testsuite/tests/rep-poly/T12709.stderr
index 782f995942..d96ec57896 100644
--- a/testsuite/tests/rep-poly/T12709.stderr
+++ b/testsuite/tests/rep-poly/T12709.stderr
@@ -1,9 +1,11 @@
 
 T12709.hs:28:13: error:
-    • The argument ‘1 + 2 + 3’ of ‘(+)’
+    • The argument ‘1’ of ‘(+)’
       does not have a fixed runtime representation.
       Its type is:
-        a :: TYPE rep
+        a0 :: TYPE c0
+      Cannot unify ‘rep’ with the type variable ‘c0’
+      because it is not a concrete ‘RuntimeRep’.
     • In the expression: 1 + 2 + 3 + 4
       In an equation for ‘u’: u = 1 + 2 + 3 + 4
       In the expression:
@@ -11,3 +13,4 @@ T12709.hs:28:13: error:
           u :: Num (a :: TYPE rep) => a
           u = 1 + 2 + 3 + 4
         in BUB u u
+    • Relevant bindings include u :: a (bound at T12709.hs:28:9)
diff --git a/testsuite/tests/rep-poly/T12973.stderr b/testsuite/tests/rep-poly/T12973.stderr
index 7a70b92859..b328176c1d 100644
--- a/testsuite/tests/rep-poly/T12973.stderr
+++ b/testsuite/tests/rep-poly/T12973.stderr
@@ -3,6 +3,9 @@ T12973.hs:13:7: error:
     • The argument ‘3’ of ‘(+)’
       does not have a fixed runtime representation.
       Its type is:
-        a :: TYPE r
+        a0 :: TYPE c0
+      Cannot unify ‘r’ with the type variable ‘c0’
+      because it is not a concrete ‘RuntimeRep’.
     • In the expression: 3 + 4
       In an equation for ‘foo’: foo = 3 + 4
+    • Relevant bindings include foo :: a (bound at T12973.hs:13:1)
diff --git a/testsuite/tests/rep-poly/T13105.stderr b/testsuite/tests/rep-poly/T13105.stderr
deleted file mode 100644
index e5eaafa03a..0000000000
--- a/testsuite/tests/rep-poly/T13105.stderr
+++ /dev/null
@@ -1,10 +0,0 @@
-
-T13105.hs:22:3: error:
-    • The first pattern in the equation for ‘abst’
-      does not have a fixed runtime representation.
-      Its type is:
-        Rep Int :: TYPE (RepRep Int)
-      NB: GHC does not (yet) support rewriting in runtime representations.
-      Please comment on GHC ticket #13105 if this is causing you trouble.
-      <https://gitlab.haskell.org/ghc/ghc/-/issues/13105>
-    • In the instance declaration for ‘HasRep Int’
diff --git a/testsuite/tests/rep-poly/T13233.stderr b/testsuite/tests/rep-poly/T13233.stderr
index 614aa7b796..5b083ea6c7 100644
--- a/testsuite/tests/rep-poly/T13233.stderr
+++ b/testsuite/tests/rep-poly/T13233.stderr
@@ -1,22 +1,24 @@
 
 T13233.hs:14:11: error:
-    • The data constructor argument in first position
+    • The data constructor argument in second position
       does not have a fixed runtime representation.
       Its type is:
-        a :: TYPE rep
+        b1 :: TYPE c3
+      Cannot unify ‘rep’ with the type variable ‘c3’
+      because it is not a concrete ‘RuntimeRep’.
     • In the first argument of ‘bar’, namely ‘(#,#)’
       In the expression: bar (#,#)
       In an equation for ‘baz’: baz = bar (#,#)
+    • Relevant bindings include
+        baz :: a -> a -> (# a, a #) (bound at T13233.hs:14:1)
 
 T13233.hs:22:16: error:
-    • • The data constructor argument in first position
-        does not have a fixed runtime representation.
-        Its type is:
-          a :: TYPE rep1
-      • The data constructor argument in second position
-        does not have a fixed runtime representation.
-        Its type is:
-          b :: TYPE rep2
+    • The data constructor argument in second position
+      does not have a fixed runtime representation.
+      Its type is:
+        b0 :: TYPE c1
+      Cannot unify ‘rep2’ with the type variable ‘c1’
+      because it is not a concrete ‘RuntimeRep’.
     • In the first argument of ‘obscure’, namely ‘(#,#)’
       In the expression: obscure (#,#)
       In an equation for ‘quux’: quux = obscure (#,#)
diff --git a/testsuite/tests/rep-poly/T13929.stderr b/testsuite/tests/rep-poly/T13929.stderr
index 23f0005172..5365f7d6b0 100644
--- a/testsuite/tests/rep-poly/T13929.stderr
+++ b/testsuite/tests/rep-poly/T13929.stderr
@@ -1,32 +1,28 @@
 
 T13929.hs:29:24: error:
-    • • The tuple argument in first position
-        does not have a fixed runtime representation.
-        Its type is:
-          GUnboxed f rf :: TYPE rf
-      • The tuple argument in second position
-        does not have a fixed runtime representation.
-        Its type is:
-          GUnboxed g rg :: TYPE rg
+    • The tuple argument in first position
+      does not have a fixed runtime representation.
+      Its type is:
+        a0 :: TYPE c1
+      Cannot unify ‘rf’ with the type variable ‘c1’
+      because it is not a concrete ‘RuntimeRep’.
     • In the expression: (# gunbox x, gunbox y #)
       In an equation for ‘gunbox’:
           gunbox (x :*: y) = (# gunbox x, gunbox y #)
       In the instance declaration for
         ‘GUnbox (f :*: g) ('TupleRep '[rf, rg])’
-
-T13929.hs:33:21: error:
-    • The unboxed sum does not have a fixed runtime representation.
-      Its type is:
-        GUnboxed (f :+: g) ('SumRep '[rf, rg]) :: TYPE ('SumRep '[rf, rg])
-    • In the expression: (# gunbox l | #)
-      In an equation for ‘gunbox’: gunbox (L1 l) = (# gunbox l | #)
-      In the instance declaration for
-        ‘GUnbox (f :+: g) ('SumRep '[rf, rg])’
+    • Relevant bindings include
+        x :: f p (bound at T13929.hs:29:13)
+        gunbox :: (:*:) f g p -> GUnboxed (f :*: g) ('TupleRep '[rf, rg])
+          (bound at T13929.hs:29:5)
 
 T13929.hs:34:21: error:
-    • The unboxed sum does not have a fixed runtime representation.
-      Its type is:
-        GUnboxed (f :+: g) ('SumRep '[rf, rg]) :: TYPE ('SumRep '[rf, rg])
+    • • The unboxed sum does not have a fixed runtime representation.
+        Its type is:
+          GUnboxed (f :+: g) ('SumRep '[rf, rg]) :: TYPE ('SumRep '[rf, rg])
+      • The unboxed sum does not have a fixed runtime representation.
+        Its type is:
+          GUnboxed (f :+: g) ('SumRep '[rf, rg]) :: TYPE ('SumRep '[rf, rg])
     • In the expression: (# | gunbox r #)
       In an equation for ‘gunbox’: gunbox (R1 r) = (# | gunbox r #)
       In the instance declaration for
diff --git a/testsuite/tests/rep-poly/T14561.stderr b/testsuite/tests/rep-poly/T14561.stderr
index 3c372e689c..8f102143eb 100644
--- a/testsuite/tests/rep-poly/T14561.stderr
+++ b/testsuite/tests/rep-poly/T14561.stderr
@@ -4,6 +4,10 @@ T14561.hs:12:9: error:
       The first argument of ‘unsafeCoerce#’
       does not have a fixed runtime representation.
       Its type is:
-        a :: TYPE r
+        a0 :: TYPE c0
+      Cannot unify ‘r’ with the type variable ‘c0’
+      because it is not a concrete ‘RuntimeRep’.
     • In the expression: unsafeCoerce#
       In an equation for ‘badId’: badId = unsafeCoerce#
+    • Relevant bindings include
+        badId :: a -> a (bound at T14561.hs:12:1)
diff --git a/testsuite/tests/rep-poly/T14561b.stderr b/testsuite/tests/rep-poly/T14561b.stderr
index 7af3b05511..bbc72d01d8 100644
--- a/testsuite/tests/rep-poly/T14561b.stderr
+++ b/testsuite/tests/rep-poly/T14561b.stderr
@@ -4,6 +4,10 @@ T14561b.hs:12:9: error:
       The first argument of ‘coerce’
       does not have a fixed runtime representation.
       Its type is:
-        a :: TYPE r
+        a0 :: TYPE c0
+      Cannot unify ‘r’ with the type variable ‘c0’
+      because it is not a concrete ‘RuntimeRep’.
     • In the expression: coerce
       In an equation for ‘badId’: badId = coerce
+    • Relevant bindings include
+        badId :: a -> a (bound at T14561b.hs:12:1)
diff --git a/testsuite/tests/rep-poly/T17021.stderr b/testsuite/tests/rep-poly/T17021.stderr
index 0521ed1259..39f907b40c 100644
--- a/testsuite/tests/rep-poly/T17021.stderr
+++ b/testsuite/tests/rep-poly/T17021.stderr
@@ -5,8 +5,5 @@ T17021.hs:18:5: error:
       Its kind is:
         TYPE (Id LiftedRep)
       (Use -fprint-explicit-coercions to see the full type.)
-      NB: GHC does not (yet) support rewriting in runtime representations.
-      Please comment on GHC ticket #13105 if this is causing you trouble.
-      <https://gitlab.haskell.org/ghc/ghc/-/issues/13105>
     • In the expression: MkT 42
       In an equation for ‘f’: f = MkT 42
diff --git a/testsuite/tests/rep-poly/T17536b.stderr b/testsuite/tests/rep-poly/T17536b.stderr
deleted file mode 100644
index a2d161038a..0000000000
--- a/testsuite/tests/rep-poly/T17536b.stderr
+++ /dev/null
@@ -1,22 +0,0 @@
-
-T17536b.hs:19:7: error:
-    • The binder of the lambda expression
-      does not have a fixed runtime representation.
-      Its type is:
-        a :: TYPE r
-      NB: GHC does not (yet) support rewriting in runtime representations.
-      Please comment on GHC ticket #13105 if this is causing you trouble.
-      <https://gitlab.haskell.org/ghc/ghc/-/issues/13105>
-    • In the expression: \ _ -> 0
-      In an equation for ‘g’: g L = \ _ -> 0
-
-T17536b.hs:20:7: error:
-    • The binder of the lambda expression
-      does not have a fixed runtime representation.
-      Its type is:
-        a :: TYPE r
-      NB: GHC does not (yet) support rewriting in runtime representations.
-      Please comment on GHC ticket #13105 if this is causing you trouble.
-      <https://gitlab.haskell.org/ghc/ghc/-/issues/13105>
-    • In the expression: \ _ -> 3#
-      In an equation for ‘g’: g U = \ _ -> 3#
diff --git a/testsuite/tests/rep-poly/T17817.stderr b/testsuite/tests/rep-poly/T17817.stderr
index 7acdec120a..4fb45622bc 100644
--- a/testsuite/tests/rep-poly/T17817.stderr
+++ b/testsuite/tests/rep-poly/T17817.stderr
@@ -4,6 +4,15 @@ T17817.hs:16:10: error:
       The first argument of ‘mkWeak#’
       does not have a fixed runtime representation.
       Its type is:
-        a :: TYPE ('BoxedRep l)
+        a0 :: TYPE ('BoxedRep c0)
+      Cannot unify ‘l’ with the type variable ‘c0’
+      because it is not a concrete ‘Levity’.
     • In the expression: mkWeak#
       In an equation for ‘primop’: primop = mkWeak#
+    • Relevant bindings include
+        primop :: a
+                  -> b
+                  -> (State# RealWorld -> (# State# RealWorld, c #))
+                  -> State# RealWorld
+                  -> (# State# RealWorld, Weak# b #)
+          (bound at T17817.hs:16:1)
diff --git a/testsuite/tests/rep-poly/T19615.stderr b/testsuite/tests/rep-poly/T19615.stderr
index 873b3816f9..f0d3d8297d 100644
--- a/testsuite/tests/rep-poly/T19615.stderr
+++ b/testsuite/tests/rep-poly/T19615.stderr
@@ -1,9 +1,14 @@
 
-T19615.hs:17:14: error:
+T19615.hs:17:21: error:
     • The argument ‘(f x)’ of ‘lift'’
       does not have a fixed runtime representation.
       Its type is:
-        b :: TYPE r'
-    • In the expression: lift' (f x) id
+        a0 :: TYPE c0
+      Cannot unify ‘r'’ with the type variable ‘c0’
+      because it is not a concrete ‘RuntimeRep’.
+    • In the first argument of ‘lift'’, namely ‘(f x)’
+      In the expression: lift' (f x) id
       In an equation for ‘mapF’: mapF f x = lift' (f x) id
-      In the instance declaration for ‘Call LiftedRep’
+    • Relevant bindings include
+        f :: a -> b (bound at T19615.hs:17:8)
+        mapF :: (a -> b) -> Lev a -> Lev b (bound at T19615.hs:17:3)
diff --git a/testsuite/tests/rep-poly/T19709b.stderr b/testsuite/tests/rep-poly/T19709b.stderr
index 6592f2d67f..a236ea99e2 100644
--- a/testsuite/tests/rep-poly/T19709b.stderr
+++ b/testsuite/tests/rep-poly/T19709b.stderr
@@ -1,13 +1,11 @@
 
-T19709b.hs:11:7: error:
+T19709b.hs:11:15: error:
     • The argument ‘(error @Any "e2")’ of ‘levfun’
       does not have a fixed runtime representation.
       Its type is:
-        a0 :: TYPE Any
-    • In the first argument of ‘seq’, namely ‘levfun (error @Any "e2")’
+        a1 :: TYPE c0
+      Cannot unify ‘Any’ with the type variable ‘c0’
+      because it is not a concrete ‘RuntimeRep’.
+    • In the first argument of ‘levfun’, namely ‘(error @Any "e2")’
+      In the first argument of ‘seq’, namely ‘levfun (error @Any "e2")’
       In the expression: levfun (error @Any "e2") `seq` return []
-      In the expression:
-        let
-          levfun :: forall (r :: RuntimeRep) (a :: TYPE r). a -> ()
-          levfun = error "e1"
-        in levfun (error @Any "e2") `seq` return []
diff --git a/testsuite/tests/rep-poly/T20113.stderr b/testsuite/tests/rep-poly/T20113.stderr
index 2e51b23d85..a941c709de 100644
--- a/testsuite/tests/rep-poly/T20113.stderr
+++ b/testsuite/tests/rep-poly/T20113.stderr
@@ -4,7 +4,12 @@ T20113.hs:7:35: error:
       does not have a fixed runtime representation.
       Its type is:
         a :: TYPE rep
-    • The first pattern in the equation for ‘$sel:y_fld:MkY’
-      does not have a fixed runtime representation.
-      Its type is:
-        Y a :: TYPE rep
+    • In the pattern: MkY {y_fld = $sel:y_fld:MkY}
+      In an equation for ‘T20113.$sel:y_fld:MkY’:
+          T20113.$sel:y_fld:MkY MkY {y_fld = $sel:y_fld:MkY} = $sel:y_fld:MkY
+
+T20113.hs:7:35: error:
+    The first pattern in the equation for ‘$sel:y_fld:MkY’
+    does not have a fixed runtime representation.
+    Its type is:
+      Y a :: TYPE rep
diff --git a/testsuite/tests/rep-poly/T20363.stderr b/testsuite/tests/rep-poly/T20363.stderr
index fdc6f94db6..cf719e3176 100644
--- a/testsuite/tests/rep-poly/T20363.stderr
+++ b/testsuite/tests/rep-poly/T20363.stderr
@@ -5,8 +5,5 @@ T20363.hs:23:10: error:
       Its kind is:
         TYPE NilRep
       (Use -fprint-explicit-coercions to see the full type.)
-      NB: GHC does not (yet) support rewriting in runtime representations.
-      Please comment on GHC ticket #13105 if this is causing you trouble.
-      <https://gitlab.haskell.org/ghc/ghc/-/issues/13105>
     • In the pattern: MkNT (##)
       In an equation for ‘test1b’: test1b (MkNT (##)) = 0
diff --git a/testsuite/tests/rep-poly/T20363_show_co.stderr b/testsuite/tests/rep-poly/T20363_show_co.stderr
index 6b18496208..69fa078718 100644
--- a/testsuite/tests/rep-poly/T20363_show_co.stderr
+++ b/testsuite/tests/rep-poly/T20363_show_co.stderr
@@ -5,8 +5,5 @@ T20363_show_co.hs:23:10: error:
       Its type is:
         ((# #) |> (TYPE (Sym (T20363_show_co.D:R:NilRep[0])))_N) :: TYPE
                                                                       NilRep
-      NB: GHC does not (yet) support rewriting in runtime representations.
-      Please comment on GHC ticket #13105 if this is causing you trouble.
-      <https://gitlab.haskell.org/ghc/ghc/-/issues/13105>
     • In the pattern: MkNT (##)
       In an equation for ‘test1b’: test1b (MkNT (##)) = 0
diff --git a/testsuite/tests/rep-poly/T20363b.stderr b/testsuite/tests/rep-poly/T20363b.stderr
index 8d2251390f..7651077162 100644
--- a/testsuite/tests/rep-poly/T20363b.stderr
+++ b/testsuite/tests/rep-poly/T20363b.stderr
@@ -1,50 +1,22 @@
 
-T20363b.hs:45:10: error:
-    • The newtype constructor pattern
-      does not have a fixed runtime representation.
-      Its type is:
-        NestedTuple 'Zero Addr# :: TYPE (NestedTupleRep 'Zero 'AddrRep)
-      NB: GHC does not (yet) support rewriting in runtime representations.
-      Please comment on GHC ticket #13105 if this is causing you trouble.
-      <https://gitlab.haskell.org/ghc/ghc/-/issues/13105>
-    • In the pattern: MkNT (##)
-      In an equation for ‘test1b’: test1b (MkNT (##)) = 0
-
 T20363b.hs:48:10: error:
-    • The newtype constructor pattern
-      does not have a fixed runtime representation.
-      Its type is:
-        NestedTuple ('Suc 'Zero) Addr# :: TYPE
-                                            (NestedTupleRep ('Suc 'Zero) 'AddrRep)
-      NB: GHC does not (yet) support rewriting in runtime representations.
-      Please comment on GHC ticket #13105 if this is causing you trouble.
-      <https://gitlab.haskell.org/ghc/ghc/-/issues/13105>
+    • • The newtype constructor pattern
+        does not have a fixed runtime representation.
+        Its type is:
+          NestedTuple ('Suc 'Zero) Addr# :: TYPE
+                                              (NestedTupleRep ('Suc 'Zero) 'AddrRep)
+      • The argument ‘(# nullAddr#, (##) #)’ of ‘MkNT’
+        does not have a fixed runtime representation.
+        Its type is:
+          NestedTuple ('Suc 'Zero) Addr# :: TYPE
+                                              (NestedTupleRep ('Suc 'Zero) 'AddrRep)
+      • The newtype constructor pattern
+        does not have a fixed runtime representation.
+        Its type is:
+          NestedTuple 'Zero Addr# :: TYPE (NestedTupleRep 'Zero 'AddrRep)
+      • The argument ‘(##)’ of ‘MkNT’
+        does not have a fixed runtime representation.
+        Its type is:
+          NestedTuple 'Zero Addr# :: TYPE (NestedTupleRep 'Zero 'AddrRep)
     • In the pattern: MkNT (# i, (##) #)
       In an equation for ‘test2b’: test2b (MkNT (# i, (##) #)) = i
-
-T20363b.hs:51:19: error:
-    • The argument ‘(##)’ of ‘MkNT’
-      does not have a fixed runtime representation.
-      Its type is:
-        NestedTuple 'Zero Addr# :: TYPE (NestedTupleRep 'Zero 'AddrRep)
-      NB: GHC does not (yet) support rewriting in runtime representations.
-      Please comment on GHC ticket #13105 if this is causing you trouble.
-      <https://gitlab.haskell.org/ghc/ghc/-/issues/13105>
-    • In the first argument of ‘test1b’, namely ‘(MkNT (##))’
-      In the expression: test1b (MkNT (##))
-      In an equation for ‘test1c’: test1c = test1b (MkNT (##))
-
-T20363b.hs:54:21: error:
-    • The argument ‘(# nullAddr#, (##) #)’ of ‘MkNT’
-      does not have a fixed runtime representation.
-      Its type is:
-        NestedTuple ('Suc 'Zero) Addr# :: TYPE
-                                            (NestedTupleRep ('Suc 'Zero) 'AddrRep)
-      NB: GHC does not (yet) support rewriting in runtime representations.
-      Please comment on GHC ticket #13105 if this is causing you trouble.
-      <https://gitlab.haskell.org/ghc/ghc/-/issues/13105>
-    • In the first argument of ‘test2b’, namely
-        ‘(MkNT (# nullAddr#, (##) #))’
-      In the expression: test2b (MkNT (# nullAddr#, (##) #))
-      In an equation for ‘test2c’:
-          test2c _ = test2b (MkNT (# nullAddr#, (##) #))
diff --git a/testsuite/tests/rep-poly/T21239.hs b/testsuite/tests/rep-poly/T21239.hs
new file mode 100644
index 0000000000..9ca1961114
--- /dev/null
+++ b/testsuite/tests/rep-poly/T21239.hs
@@ -0,0 +1,19 @@
+
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE UnboxedTuples #-}
+
+module T21239 where
+
+import GHC.Exts
+
+-- This test goes wrong if we don't properly decompose
+-- when unifying ConcreteTv metavariables.
+
+atomicModifyMutVar#
+  :: MutVar# s a
+  -> (a -> b)
+  -> State# s
+  -> (# State# s, c #)
+atomicModifyMutVar# mv f s =
+  case unsafeCoerce# (atomicModifyMutVar2# mv f s) of
+    (# s', _, ~(_, res) #) -> (# s', res #)
diff --git a/testsuite/tests/rep-poly/UnliftedNewtypesCoerceFail.stderr b/testsuite/tests/rep-poly/UnliftedNewtypesCoerceFail.stderr
index ba92961bcb..db08ac81d8 100644
--- a/testsuite/tests/rep-poly/UnliftedNewtypesCoerceFail.stderr
+++ b/testsuite/tests/rep-poly/UnliftedNewtypesCoerceFail.stderr
@@ -4,6 +4,10 @@ UnliftedNewtypesCoerceFail.hs:15:8: error:
       The first argument of ‘coerce’
       does not have a fixed runtime representation.
       Its type is:
-        x :: TYPE rep
+        a0 :: TYPE c0
+      Cannot unify ‘rep’ with the type variable ‘c0’
+      because it is not a concrete ‘RuntimeRep’.
     • In the expression: coerce
       In an equation for ‘goof’: goof = coerce
+    • Relevant bindings include
+        goof :: x -> y (bound at UnliftedNewtypesCoerceFail.hs:15:1)
diff --git a/testsuite/tests/rep-poly/UnliftedNewtypesLevityBinder.stderr b/testsuite/tests/rep-poly/UnliftedNewtypesLevityBinder.stderr
index f4e7c62b46..41dbd44d3f 100644
--- a/testsuite/tests/rep-poly/UnliftedNewtypesLevityBinder.stderr
+++ b/testsuite/tests/rep-poly/UnliftedNewtypesLevityBinder.stderr
@@ -3,6 +3,10 @@ UnliftedNewtypesLevityBinder.hs:16:7: error:
     • The newtype constructor argument
       does not have a fixed runtime representation.
       Its type is:
-        a :: TYPE r
+        a0 :: TYPE c0
+      Cannot unify ‘r’ with the type variable ‘c0’
+      because it is not a concrete ‘RuntimeRep’.
     • In the expression: IdentC
       In an equation for ‘bad’: bad = IdentC
+    • Relevant bindings include
+        bad :: a -> Ident a (bound at UnliftedNewtypesLevityBinder.hs:16:1)
diff --git a/testsuite/tests/rep-poly/all.T b/testsuite/tests/rep-poly/all.T
index 140076e598..c7f4859272 100644
--- a/testsuite/tests/rep-poly/all.T
+++ b/testsuite/tests/rep-poly/all.T
@@ -27,10 +27,12 @@ test('T20330b', normal, compile, [''])
 test('T20423', normal, compile_fail, [''])
 test('T20423b', normal, compile_fail, [''])
 test('T20426', normal, compile_fail, [''])
+test('T21239', normal, compile, [''])
 
 test('LevPolyLet', normal, compile_fail, [''])
 test('PandocArrowCmd', normal, compile, [''])
 test('RepPolyApp', normal, compile_fail, [''])
+test('RepPolyArgument', normal, compile_fail, [''])
 test('RepPolyArrowCmd', normal, compile_fail, [''])
 test('RepPolyArrowFun', normal, compile_fail, [''])
 test('RepPolyBackpack1', normal, backpack_compile_fail, [''])
@@ -48,6 +50,8 @@ test('RepPolyDoBody2', normal, compile_fail, [''])
 test('RepPolyDoReturn', normal, compile, [''])
 test('RepPolyFFI', normal, compile, [''])
 test('RepPolyLambda', normal, compile_fail, [''])
+test('RepPolyInferPatBind', normal, compile_fail, [''])
+test('RepPolyInferPatSyn', normal, compile_fail, [''])
 test('RepPolyLeftSection1', normal, compile, [''])
 test('RepPolyLeftSection2', normal, compile_fail, [''])
 test('RepPolyMagic', normal, compile_fail, [''])
@@ -83,12 +87,17 @@ test('UnliftedNewtypesLevityBinder', normal, compile_fail, [''])
 ## The following tests require rewriting in RuntimeReps,            ##
 ## i.e. PHASE 2 of the FixedRuntimeRep plan.                        ##
 ##                                                                  ##
+## These tests work!                                                ##
+                                                                    ##
+test('T13105', normal, compile, [''])                               ##
+test('T17536b', normal, compile, [''])                              ##
+                                                                    ##
+## These don't!                                                     ##
 ## For the moment, we check that we get the expected error message, ##
 ## as we want to reject these in the typechecker instead of getting ##
 ## a compiler crash.                                                ##
-test('T13105', normal, compile_fail, [''])                          ##
+                                                                    ##
 test('T17021', normal, compile_fail, [''])                          ##
-test('T17536b', normal, compile_fail, [''])                         ##
 test('T20363', normal, compile_fail, [''])                          ##
 test('T20363_show_co', normal, compile_fail                         ##
     , ['-fprint-explicit-coercions'])                               ##
diff --git a/testsuite/tests/typecheck/should_fail/T7869.stderr b/testsuite/tests/typecheck/should_fail/T7869.stderr
index 15e9cc4658..c599b276d9 100644
--- a/testsuite/tests/typecheck/should_fail/T7869.stderr
+++ b/testsuite/tests/typecheck/should_fail/T7869.stderr
@@ -1,16 +1,18 @@
 
 T7869.hs:3:12: error:
-    • Couldn't match type ‘b1’ with ‘b’
+    • Couldn't match type ‘a1’ with ‘a’
       Expected: [a1] -> b1
         Actual: [a] -> b
-      ‘b1’ is a rigid type variable bound by
+      ‘a1’ is a rigid type variable bound by
         an expression type signature:
           forall a1 b1. [a1] -> b1
         at T7869.hs:3:20-27
-      ‘b’ is a rigid type variable bound by
+      ‘a’ is a rigid type variable bound by
         the inferred type of f :: [a] -> b
         at T7869.hs:3:1-27
     • In the expression: f x
       In the expression: (\ x -> f x) :: [a] -> b
       In an equation for ‘f’: f = (\ x -> f x) :: [a] -> b
-    • Relevant bindings include f :: [a] -> b (bound at T7869.hs:3:1)
+    • Relevant bindings include
+        x :: [a1] (bound at T7869.hs:3:7)
+        f :: [a] -> b (bound at T7869.hs:3:1)