Note [Lift equality constraints when quantifying]

GHC/Tc/Solver.hs:1979 compiler

We can't quantify over a constraint (t1 ~# t2) because that isn't a
predicate type; see Note [Types for coercions, predicates, and evidence]
in GHC.Core.Predicate

So we have to 'lift' it to (t1 ~ t2).  Similarly (~R#) must be lifted
to Coercible.

This tiresome lifting is the reason that pick_me (in
pickQuantifiablePreds) returns a Maybe rather than a Bool.

References 1

Referenced by 4