Note [Possible fast path for equality constraints]

GHC/Tc/Utils/Instantiate.hs:411 compiler

Given  f :: forall a b. (a ~ [b]) => a -> b -> blah
rather than emitting ([W] alpha ~ [beta]) we could imagine calling unifyType
right here. But note

* Often such constraints look like (F a ~ G b), in which case unification would end up
  spitting out a wanted-equality anyway.

* So perhaps the main fast-path would be where the LHS or RHS was an instantiation
  variable. But note that this could, perhaps, impact on Quick Look:

  - The first arg of `f` changes from the naked `a` to the guarded `[b]` (or would do so
    if we zonked it).  That might affect typing under Quick Look.

  - We might imagine using the let-bound skolems trick:
         g :: forall a b. (a ~ forall c. c->c) => a -> [a] -> [a]
    Here we are just using `a` as a local abreviation for (forall c. c->c)
    See Note [Let-bound skolems] in GHC.Tc.Solver.InertSet.

    If we substitute aggressively (including zonking) that abbreviation could work.  But
    again it affects what is typeable.  And we don't support equalities over polytypes,
    currently, anyway.

* There is little point in trying to optimise for
   - (s ~# t), because this has kind Constraint#, not Constraint, and so will not be
               in the theta instantiated in instCall
   - (s ~~ t), becaues heterogeneous equality is rare, and more complicated.

Anyway, for now we don't take advantage of these potential effects.

References 1

Referenced by 1