# 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