Note [Equality evidence in pattern synonyms]

Consider
  data X a where
     MkX :: Eq a => [a] -> X (Maybe a)
  pattern P x = MkG x

Then there is a danger that GHC will infer
  P :: forall a.  () =>
       forall b. (a ~# Maybe b, Eq b) => [b] -> X a

The 'builder' for P, which is called in user-code, will then
have type
  $bP :: forall a b. (a ~# Maybe b, Eq b) => [b] -> X a

and that is bad because (a ~# Maybe b) is not a predicate type
(see Note [Types for coercions, predicates, and evidence] in GHC.Core.Predicate
and is not implicitly instantiated.

So in mkProvEvidence we lift (a ~# b) to (a ~ b).  Tiresome, and
marginally less efficient, if the builder/matcher are not inlined.

See also Note [Lift equality constraints when quantifying] in GHC.Tc.Solver