Deduction terms have two encodings for a nullary constant, so rule patterns cannot mention one

[aaronstevenwhite]

The defect

A nullary constant has two incompatible encodings depending on where it appears.

In a rule pattern, _convert_pattern tags it (src/quivers/dsl/compiler/deductions.py:432):

if name in atoms_set:
    return ("atom", name)

In a lexicon LF, the let-expression compiler emits a bare 1-tuple (src/quivers/dsl/compiler/programs.py:3059):

if name in constructors:
    return (name,)

So the chart holds

('span', 1, 2, ('atom', 'N'), ('Lam', ('#v1',), ('App', ('dog_p',), ('Var', ('#v1',)))))
                ^^^^^^^^^^^^ category: tagged      ^^^^^^^^^ LF: bare

A rule pattern that mentions a constant inside an LF, say Claim(App(forall_t, X)), compiles forall_t to ('atom', 'forall_t'), which can never match the ('forall_t',) sitting in the chart. The rule is well-formed, compiles clean, and silently never fires.

Constructor applications already agree: _convert_pattern's ObjectEffectApply branch returns (effect, *args), and the LF evaluator builds (func, *args). Only the zero-argument case diverges. And the grammar's _object_expr requires at least one argument, so forall_t() cannot be written to force the application form.

Why it is not a one-line fix

_convert_pattern cannot tell a category position from an LF position. In rule fwd_app : span(I, K, Fwd(X, Y), F), ... |- span(I, J, Y, App(F, A)), the category Fwd(X, Y) and the LF F are both just arguments of span. There is no type information at that point to dispatch on.

I tried the narrow unification, changing programs.py:3059 to ("atom", name) so LFs match patterns. It silently breaks binders. With binders Lam, _normalise_binders matches a bound-variable occurrence by tuple head; under the tagged encoding the head becomes the literal "atom", so occurrences stop being renamed while binders still are:

# before
('Lam', ('#v1',), ('App', ('dog_p',),        ('Var', ('#v1',))))     # bound
# after
('Lam', ('#v1',), ('App', ('atom','dog_p'), ('Var', ('atom','x')))) # body is free

The lambda binds #v1 and its body references x. The term is still well-formed, the chart still parses, and the entire suite stayed green (43 passed, only an encoding assertion in test_subst_capture_avoiding failed). Nothing detected that every lambda in the gallery had come unbound.

A regression test now pins a binder to its occurrences (test_lambda_body_occurrence_matches_its_binder), so a future attempt fails loudly instead.

Extra constraints on a real fix

1. ("atom", name) is public. Users seed charts with it: D([(("atom", "NP"), torch.tensor(0.0))]) in tests/test_structural.py. Unifying changes the axiom-seeding API and every chart-inspection call site.
2. _category_depth dispatches on the "atom" head (deductions.py:166) to gate rules that would otherwise rewrite A into Dia(A) forever. Under a bare-tuple encoding, depth 0 becomes len(term) == 1.
3. The tagged form is ambiguous as a term algebra. ('atom', 'dog_p') is indistinguishable from a binary constructor named atom applied to one argument.
4. The bare form is ambiguous too. A nullary constant ('dog_p',) and a canonical bound variable ('#v1',) have the same shape, which is exactly why the alpha-renamer confuses them.

Both encodings are therefore wrong on their own terms; a fix should pick one discriminated representation and carry it through categories, LFs, patterns, _normalise_binders, _category_depth, goal matching, and the public chart API together.

Impact today

docs/examples/source/montague_nli.qvr pays for this directly. Its prover cannot write a rule over forall_t / implies_t, so quantificational force has to ride on the determiner's category (DetEvery / DetSome) rather than on a constant in the LF, costing one category per determiner where a single Det plus Quant(every_t, P, Q) would do.