`LFunc.concreteEval` has type `... → Option LExpr`, so Lean only verifies that it returns an `Option LExpr` — it does not verify that the produced expression is well-typed in the Lambda/Core type system. This means annotations on `.op` nodes, argument counts, and return types inside `concreteEval` are unchecked metadata that can silently be wrong.
A recent example: `mkModeBoolFunc` in `PyFactory.lean` annotated the `.op` node for `Str.InRegEx` with `mty[bool]` (the return type) instead of `mty[string → (regex → bool)]` (the full function type). This was only caught in code review, not by the compiler. See #699.
Proposed fix: After `concreteEval` produces an `LExpr`, run it through the Lambda type checker and assert that its type matches `LFunc.output`. This would catch:
- Wrong `.op` type annotations
- Argument count mismatches in `mkApp`
- Return type mismatches
This check could be done at factory registration time or at the call site in the verifier pipeline, whichever is more practical.
`LFunc.concreteEval` has type `... → Option LExpr`, so Lean only verifies that it returns an `Option LExpr` — it does not verify that the produced expression is well-typed in the Lambda/Core type system. This means annotations on `.op` nodes, argument counts, and return types inside `concreteEval` are unchecked metadata that can silently be wrong.
A recent example: `mkModeBoolFunc` in `PyFactory.lean` annotated the `.op` node for `Str.InRegEx` with `mty[bool]` (the return type) instead of `mty[string → (regex → bool)]` (the full function type). This was only caught in code review, not by the compiler. See #699.
Proposed fix: After `concreteEval` produces an `LExpr`, run it through the Lambda type checker and assert that its type matches `LFunc.output`. This would catch:
This check could be done at factory registration time or at the call site in the verifier pipeline, whichever is more practical.