Summary
Strata/DL/Lambda/Preconditions.lean::callSiteTypeSubst (added in #1205) and Strata/DL/Lambda/Factory.lean::LFunc.computeTypeSubst perform structurally identical unification at a call site, but with the priority of inputs reversed:
LFunc.computeTypeSubst (Factory.lean:653–666) — prefers the operator's .op annotation, falls back to argument types. Used after type inference, where .op always carries the instantiated arrow type.callSiteTypeSubst (Preconditions.lean:77–90) — prefers argument types, falls back to the .op annotation. Used by PrecondElim, which runs before type checking, so the .op may still carry the generic type and argument types are the more reliable source.
Why we didn't unify them in #1205
Several proofs in Strata/DL/Lambda/Semantics.lean depend on the current computeTypeSubst shape (computeTypeSubst_of_opTypeSubst, computeTypeSubst_eraseMetadata_congr, and the callOfLFunc correctness lemmas around lines 2393–2563). Refactoring computeTypeSubst into a (preferOp : Bool)-parameterised helper requires re-establishing those proofs, which was out of scope for the bug fix.
Suggested approach
- Introduce
LFunc.computeTypeSubstWith (preferOp : Bool) in Factory.lean containing the shared unification body.
- Define
LFunc.computeTypeSubst := computeTypeSubstWith (preferOp := true) and LFunc.callSiteTypeSubst := computeTypeSubstWith (preferOp := false) (the latter currently lives in Preconditions.lean and would move to Factory.lean).
- Update
Semantics.lean proofs to unfold through the parameterised helper. The post-type-inference lemmas should still hold because they only invoke the preferOp := true instantiation.
When to do this
Naturally pairs with the next unrelated touch to Semantics.lean::computeTypeSubst_* proofs.
References
Summary
Strata/DL/Lambda/Preconditions.lean::callSiteTypeSubst(added in #1205) andStrata/DL/Lambda/Factory.lean::LFunc.computeTypeSubstperform structurally identical unification at a call site, but with the priority of inputs reversed:LFunc.computeTypeSubst(Factory.lean:653–666) — prefers the operator's.opannotation, falls back to argument types. Used after type inference, where.opalways carries the instantiated arrow type.callSiteTypeSubst(Preconditions.lean:77–90) — prefers argument types, falls back to the.opannotation. Used byPrecondElim, which runs before type checking, so the.opmay still carry the generic type and argument types are the more reliable source.Why we didn't unify them in #1205
Several proofs in
Strata/DL/Lambda/Semantics.leandepend on the currentcomputeTypeSubstshape (computeTypeSubst_of_opTypeSubst,computeTypeSubst_eraseMetadata_congr, and thecallOfLFunccorrectness lemmas around lines 2393–2563). RefactoringcomputeTypeSubstinto a(preferOp : Bool)-parameterised helper requires re-establishing those proofs, which was out of scope for the bug fix.Suggested approach
LFunc.computeTypeSubstWith (preferOp : Bool)inFactory.leancontaining the shared unification body.LFunc.computeTypeSubst := computeTypeSubstWith (preferOp := true)andLFunc.callSiteTypeSubst := computeTypeSubstWith (preferOp := false)(the latter currently lives inPreconditions.leanand would move toFactory.lean).Semantics.leanproofs to unfold through the parameterised helper. The post-type-inference lemmas should still hold because they only invoke thepreferOp := trueinstantiation.When to do this
Naturally pairs with the next unrelated touch to
Semantics.lean::computeTypeSubst_*proofs.References