Never kick out Given Nominal equalities
In other explorations (#17323 and friends) Simon and I determined that a Given Nominal equality should never be kicked out. Why? Because the mutable update of a unification variable should really behave just like a given nominal equality (really, the solver should be pure, but that would be inefficient). Mutable variable updates can't get revisited (i.e. kicked out), so neither should given nominal equalities. And we almost have this property. Here is the relevant text:
Lemma: Nominal Given equalities are never kicked out. Proof: Let a -fw-> t
be a work item and b -G/N-> s
be an inert equality. We must show that, regardless of a
, t
, b
, and s
, condition K from the Note always hold. (Condition K is the "keep" condition.)
K0 is true when fw /= G/N
. If K0 is true, then K is true, and we are done. So, we assume that fw = G/N
.
We must show all of K1-K3.
K1: not (a = b)
. This must be true, because if a = b
, then a
would have been rewritten during canonicalization. This is the case because G/N >= G/N
.
K2: not (G/N >= G/N) OR G/N >= G/N OR ...
. True by the law of the excluded middle.
K3: Actually, only K3a applies, because the role is nominal: s /= a
. Actually, we might indeed have s = a
. But we still shouldn't kick out; see Note [K3: completeness of solving], which makes this clear. So, Action Item: modify the kick-out conditions so that this proof holds.
QED.
We think the new keep condition should be s /= a && t /= b
. This ticket is to double-check this intuition and execute.
We believe that there is no loop or other misbehavior here. It's just good hygiene to have given nominals and metavar unifications to be treated identically within the solver. And less kicking out is good, all else being equal.