Summary
A :merge action block that builds a constructor application writes a row keyed on a dangling e-class when the two colliding values are equal. The row is unextractable, prints as Unextractable, and cannot be matched by a rule — so it is unreachable but still counted.
This is in the :merge (<action>* <result-expr>) action block, which is an extension local to this repo (egglog/src/ast/parse.rs, added in 9828dbf). I checked upstream egraphs-good/egglog at c92a910 (v2.0.0): its :merge takes a single expression, so this program cannot be written there and the bug is ours, not upstream's.
Repro
(datatype Math (L))
(function Log (Math) i64 :merge (min old new))
(function Dist () i64 :merge ((set (Log (L)) old) new))
(L)
(set (Dist) 2)
(set (Dist) 2)
(print-size)
(print-function Log 10)
Output:
[ERROR] Unextractable root Value(2) with sort EqSort { name: "Math" }
((Dist 1)
(L 1)
(Log 1))
(
(Log Unextractable) -> 2
)
Log has one row, but its key is not the (L) e-class — even though (L) exists and L has a row.
It is specific to equal colliding values
Change the second (set (Dist) 2) to (set (Dist) 3) and everything is correct:
((Dist 1) (L 1) (Log 1))
(
(Log (L)) -> 2
)
Extractable, properly keyed.
The row is also unreachable by matching
(datatype Math (L) (Hit))
(function Log (Math) i64 :merge (min old new))
(function Dist () i64 :merge ((set (Log (L)) old) new))
(L)
(set (Dist) 2)
(set (Dist) 2)
(rule ((= v (Log (L)))) ((Hit)))
(run 1)
(print-size)
gives (Hit 0). So the row exists in Log and counts toward (print-size), but no rule can see it. Three symptoms, one cause: evaluating (L) inside the merge action block yields an id that is not the interned (L) e-class.
Guess at the cause
The equal-value path looks like the one that short-circuits "re-setting the same value is not a change". On that path the action block still runs, but apparently in a context where constructing (L) mints a fresh id instead of interning/looking up the existing one. The distinct-value path interns correctly.
How it was found
Differential testing of the Lean model in semantics/ against this binary. The model dedups the two identical rows, so its merge phase has no pair to fire on and it writes nothing; egglog runs the body. That disagreement is what surfaced it. Repro recorded in semantics/DiffTest.lean.
Because of this, the curated :merge-body difftest cases deliberately keep colliding values distinct — a constraint a random generator over keys and values cannot be held to, so this blocks widening the random merge stream to writing bodies.
Summary
A
:mergeaction block that builds a constructor application writes a row keyed on a dangling e-class when the two colliding values are equal. The row is unextractable, prints asUnextractable, and cannot be matched by a rule — so it is unreachable but still counted.This is in the
:merge (<action>* <result-expr>)action block, which is an extension local to this repo (egglog/src/ast/parse.rs, added in9828dbf). I checked upstreamegraphs-good/egglogatc92a910(v2.0.0): its:mergetakes a single expression, so this program cannot be written there and the bug is ours, not upstream's.Repro
Output:
Loghas one row, but its key is not the(L)e-class — even though(L)exists andLhas a row.It is specific to equal colliding values
Change the second
(set (Dist) 2)to(set (Dist) 3)and everything is correct:Extractable, properly keyed.
The row is also unreachable by matching
gives
(Hit 0). So the row exists inLogand counts toward(print-size), but no rule can see it. Three symptoms, one cause: evaluating(L)inside the merge action block yields an id that is not the interned(L)e-class.Guess at the cause
The equal-value path looks like the one that short-circuits "re-setting the same value is not a change". On that path the action block still runs, but apparently in a context where constructing
(L)mints a fresh id instead of interning/looking up the existing one. The distinct-value path interns correctly.How it was found
Differential testing of the Lean model in
semantics/against this binary. The model dedups the two identical rows, so its merge phase has no pair to fire on and it writes nothing; egglog runs the body. That disagreement is what surfaced it. Repro recorded insemantics/DiffTest.lean.Because of this, the curated
:merge-body difftest cases deliberately keep colliding values distinct — a constraint a random generator over keys and values cannot be held to, so this blocks widening the random merge stream to writing bodies.