Hopelessly confusing error involving runtime-reps

Consider

{-# LANGUAGE GADTs, TypeOperators, PolyKinds #-}

import GHC.Types

data a :~: b where Refl :: a :~: a

foo :: TYPE a :~: TYPE b
foo = Refl

We get

    • Couldn't match type ‘'LiftedRep’ with ‘'LiftedRep’
      ‘a’ is a rigid type variable bound by
        the type signature for:
          foo :: * :~: *
        at Repr.hs:7:1-24
      ‘b’ is a rigid type variable bound by
        the type signature for:
          foo :: * :~: *
        at Repr.hs:7:1-24

That's a ridiculous message. But if you asdd -fprint-explicit-runtime-reps we get

    • Couldn't match type ‘a’ with ‘b’
      ‘a’ is a rigid type variable bound by
        the type signature for:
          foo :: forall (a :: RuntimeRep) (b :: RuntimeRep).
                 TYPE a :~: TYPE b
        at T16050.hs:9:1-24
      ‘b’ is a rigid type variable bound by
        the type signature for:
          foo :: forall (a :: RuntimeRep) (b :: RuntimeRep).
                 TYPE a :~: TYPE b
        at T16050.hs:9:1-24
      Expected type: TYPE a :~: TYPE b
        Actual type: TYPE a :~: TYPE a
    • In the expression: Refl
      In an equation for ‘foo’: foo = Refl
    • Relevant bindings include
        foo :: TYPE a :~: TYPE b (bound at T16050.hs:10:1)

which is the right error.

Reported in #16074 (closed) of #16050