Question: given a homogeneous equality (alpha ~# ty), when is it OK to
unify alpha := ty?
(This note only applies to /homogeneous/ equalities, in which both
sides have the same kind.)
There are five reasons not to unify:
1. (SKOL-ESC) Skolem-escape
Consider the constraint
forall[2] a[2]. alpha[1] ~ Maybe a[2]
If we unify alpha := Maybe a, the skolem 'a' may escape its scope.
The level alpha[1] says that alpha may be used outside this constraint,
where 'a' is not in scope at all. So we must not unify.
Bottom line: when looking at a constraint alpha[n] := ty, do not unify
if any free variable of 'ty' has level deeper (greater) than n
2. (UNTOUCHABLE) Untouchable unification variables
Consider the constraint
forall[2] a[2]. b[1] ~ Int => alpha[1] ~ Int
There is no (SKOL-ESC) problem with unifying alpha := Int, but it might
not be the principal solution. Perhaps the "right" solution is alpha := b.
We simply can't tell. See "OutsideIn(X): modular type inference with local
assumptions", section 2.2. We say that alpha[1] is "untouchable" inside
this implication.
Bottom line: at ambient level 'l', when looking at a constraint
alpha[n] ~ ty, do not unify alpha := ty if there are any given equalities
between levels 'n' and 'l'.
Exactly what is a "given equality" for the purpose of (UNTOUCHABLE)?
Answer: see Note [Tracking Given equalities] in GHC.Tc.Solver.InertSet
3. (TYVAR-TV) Unifying TyVarTvs and CycleBreakerTvs
This precondition looks at the MetaInfo of the unification variable:
* TyVarTv: When considering alpha{tyv} ~ ty, if alpha{tyv} is a
TyVarTv it can only unify with a type variable, not with a
structured type. So if 'ty' is a structured type, such as (Maybe x),
don't unify.
* CycleBreakerTv: never unified, except by restoreTyVarCycles.
4. (CONCRETE) A ConcreteTv can only unify with a concrete type,
by definition.
That is, if we have `rr[conc] ~ F Int`, we can't unify
`rr` with `F Int`, so we hold off on unifying.
Note however that the equality might get rewritten; for instance
if we can rewrite `F Int` to a concrete type, say `FloatRep`,
then we will have `rr[conc] ~ FloatRep` and we can unify `rr ~ FloatRep`.
Note that we can still make progress on unification even if
we can't fully solve an equality, e.g.
alpha[conc] ~# TupleRep '[ beta[tau], F gamma[tau] ]
we can fill beta[tau] := beta[conc]. This is why we call
'makeTypeConcrete' in startSolvingByUnification.
5. (REWRITERS) the equality does not have any unsolved equalities in its rewriter
set. If those other equalities have not been solved, unifying this equality
will propagate strange-looking errors elswhere. That is the whole point of
rewriter sets. Suppose our equality is
[W] co1 {rew = {cok}} (alpha :: k) ~ (Int |> {cok})
where co :: Type ~ k is an unsolved wanted. Note that this equality
is homogeneous; both sides have kind k. We refrain from unifying
here, because of `cok` in its rewriter set. See
Note [Unify only if the rewriter set is empty] in GHC.Solver.Equality.
Needless to say, all there are wrinkles:
* (SKOL-ESC) Promotion. Given alpha[n] ~ ty, what if beta[k] is free
in 'ty', where beta is a unification variable, and k>n? 'beta'
stands for a monotype, and since it is part of a level-n type
(equal to alpha[n]), we must /promote/ beta to level n. Just make
up a fresh gamma[n], and unify beta[k] := gamma[n].
* (TYVAR-TV) Unification variables. Suppose alpha[tyv,n] is a level-n
TyVarTv (see Note [TyVarTv] in GHC.Tc.Types.TcMType)? Now
consider alpha[tyv,n] ~ Bool. We don't want to unify because that
would break the TyVarTv invariant.
What about alpha[tyv,n] ~ beta[tau,n], where beta is an ordinary
TauTv? Again, don't unify, because beta might later be unified
with, say Bool. (If levels permit, we reverse the orientation here;
see Note [TyVar/TyVar orientation].)
* (UNTOUCHABLE) Untouchability. When considering (alpha[n] ~ ty), how
do we know whether there are any given equalities between level n
and the ambient level? We answer in two ways:
* In the eager unifier, we only unify if l=n. If not, alpha may be
untouchable, and defer to the constraint solver. This check is
made in GHC.Tc.Utils.uUnifilledVar2, in the guard
isTouchableMetaTyVar.
* In the constraint solver, we track where Given equalities occur
and use that to guard unification in
GHC.Tc.Utils.Unify.touchabilityTest. More details in
Note [Tracking Given equalities] in GHC.Tc.Solver.InertSet
Historical note: in the olden days (pre 2021) the constraint solver
also used to unify only if l=n. Equalities were "floated" out of the
implication in a separate step, so that they would become touchable.
But the float/don't-float question turned out to be very delicate,
as you can see if you look at the long series of Notes associated with
GHC.Tc.Solver.floatEqualities, around Nov 2020. It's much easier
to unify in-place, with no floating.