Note [Possible fast path for equality constraints]
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
- Let-bound skolems GHC.Tc.Solver.InertSet
Referenced by 1
- GHC.Tc.Utils.Instantiate call site