Z3: HOF inlining + let-binding shadowing breaks evalComputeScore-style functions

[sunholo-voight-kampff]

Background

While shipping M-SMT-CROSS-MODULE-TYPES (PR / commits 116f94fa..72902b2f), one acceptance criterion — evalComputeScore in docparse services/eval.ail should VERIFY — was deferred because the breakage turned out to NOT be Issue 6 (cross-record field-name collision, which would need qualified accessor names). It's a separate concern that should be tracked independently.

Symptom

Running ailang verify docparse/services/eval.ail against the AILANG repo at dev (commit 72902b2f):

! ERROR evalComputeScore
  Z3 error: (error "line 8 column 263: unknown constant applicable (Int)
  declared: (declare-fun applicable (CheckResult) Bool)")
  ...
  (define-fun _filter_spec_evalComputeScore_0 ((x!0 (Seq Int))) (Seq Int)
    (as seq.empty (Seq Int)))

Root cause (two separate bugs)

1. HOF inliner emits the wrong type signature. _filter_spec_evalComputeScore_0 is generated as (Seq Int) -> (Seq Int) even though the input list is (Seq CheckResult). The HOF specialiser is not threading the element type through correctly.
2. let binding name applicable shadows the record accessor function. The body has let ((applicable (...))) (let ((passed (...))) ...) — the inner applicable is bound to a Seq length (Int), but Z3 already has (declare-fun applicable (CheckResult) Bool) from the record declaration. Z3's "unknown constant applicable (Int)" comes from this shadow.

Both are independent of the cross-module record-alias / recursive-ADT work that landed in v0.14.3.

Why this is NOT Issue 6 from M-SMT-CROSS-MODULE-TYPES

Issue 6 was "two record types in the same module share a field name (e.g., applicable on both CheckResult and MetaAccum)". The current docparse eval.ail does not actually have a MetaAccum record — only CheckResult. The cross-record collision M3b would have addressed is not present here.

Suggested fix shape

For the HOF inliner: when specialising filter / map / foldl against a literal lambda, propagate the element type from the list-typed argument into the synthetic _filter_spec_* definitions. Look at internal/smt/hof_specialize.go.

For let-shadow vs accessor: either (a) prefix let-bound variables in encoded bodies (similar to the \$p_ parameter prefix from M3a), or (b) rename let bindings whose names collide with declared record accessors. Either fix needs the encoder to know the active accessor names — which activeRecordTypes already tracks.

Reference

• Sprint: M-SMT-CROSS-MODULE-TYPES (v0.14.3)
• Design doc: design_docs/implemented/v0_14_3/m-smt-cross-module-types.md (see "M3b deferred" note)
• Failing file: docparse/services/eval.ail in https://github.com/sunholo-data/ailang-parse
• Eval report: .ailang/state/evaluations/eval_M-SMT-CROSS-MODULE-TYPES_round_1.json flag Add repository-wide AGENT guidelines #1