Add type checking to Laurel resolution pass

[keyboardDrummer-bot]

Summary

Adds type checking to Laurel's Resolution.lean as requested in #1120.

Changes

• resolveStmtExpr now returns ResolveM (StmtExprMd × HighTypeMd) — both the resolved expression and its synthesized type.

• Type checks added:

  • Boolean conditions in if/while/assert/assume must be TBool
  • Arithmetic/comparison operands must be numeric (TInt, TReal, TFloat64)
  • Logical operands (And, Or, Not, Implies, etc.) must be TBool
  • Static call argument types must match parameter types
  • Instance call argument types must match parameter types (skipping self)
  • Assignment value type must match target type (single-target only)
  • Functional procedure body type must match declared output type (transparent bodies only)

• Diagnostics, not hard failures — type mismatches are reported via ResolveState.errors and compilation continues.

• Cascading error prevention:

  • Unknown types are compatible with everything
  • UserDefined types skip strict assignability checks (subtype/inheritance relationships are not tracked during resolution)
  • TVoid types skip assignment/output checks (statements like return/while don't produce values in the expression sense)
  • MultiValuedExpr types skip assignability checks (arity mismatch already reported separately)
  • Kind-mismatched type references (e.g., using a variable name as a type) produce Unknown to avoid cascading

• computeExprType in LaurelTypes.lean is unchanged — it continues to work alongside the new type checking.

• Callers updated to use the returned type from resolveStmtExpr (e.g., resolveBody, resolveProcedure, resolveInstanceProcedure, resolveConstant, resolveTypeDefinition).

Testing

All existing tests pass (lake build StrataTest — 592 jobs successful).

Closes #1120"

[keyboardDrummer]

@keyboardDrummer-bot can you add a test that confirms various type checking errors are reported?

[tautschnig]

1. checkBool and checkNumeric pass-through for UserDefined (lines 381, 388). The comment says "constrained types may wrap bool / numeric", which is fair for constrained subtypes, but the check is by kind rather than by wrapped base type: a Color user type will silently pass checkBool, and Dog will silently pass checkNumeric. In practice the downstream type-erasure path may catch these later, but the point of type checking here is to catch them early. Two options, either is fine:

• Inspect the resolved UserDefined target to see whether it's .constrainedType wrapping a compatible base, and only pass it through in that case.
• Keep the current permissive behaviour but add a comment and a test that explicitly documents "Color in if pos slot silently passes — known limitation, tracked under #…".

2. checkAssignable treats any UserDefined / TCore pair as compatible (lines 399–402). This is the deliberate "subtype relationships not tracked here" trade-off, noted in the PR body. It means var x: Dog := new Cat and var x: CoreA := ∅CoreB-typed RHS both silently succeed. Worth a regression test that asserts no diagnostic is emitted for such cases, as a paper trail for the known limitation (so that when someone later does track subtyping, the test flips from "passes without complaint" to "correctly rejects").

3. Eq / Neq uses checkAssignable source rhsTy lhsTy (line 571) — asymmetric for a symmetric operator, and the resulting diagnostic reads "Type mismatch: expected '{rhsTy}', but got '{lhsTy}'" which misleadingly frames the LHS as "wrong". For 1 == "hello" the user sees "expected 'string', but got 'int'" — technically accurate under the checker's internal view but confusing. Consider either (a) dropping the check for Eq/Neq entirely and relying on the caller to ensure the operands are in the same comparable category, or (b) rewording the diagnostic message for the symmetric case: "operands of '==' have incompatible types '{lhsTy}' and '{rhsTy}'".

4. PrimitiveOp.StrConcat has no operand check (inside the match op with at around line 575). If someone writes 1 ++ "hello" it slides through. Trivial to add: for aTy in argTypes do checkAssignable source { val := .TString, source := source } aTy.

5. Quantifier body type is assumed .TBool (line 605) without a check that it actually is. forall x: int . x (body of type int) silently passes. Trivial to add: checkBool body'.source bodyTy.

6. Arity guard valueTy.val != HighType.TVoid (line 507) skips the check when the RHS is void. Correct for statement RHS like return / while, but relies on the checker never mis-tagging a value expression as void. Worth a comment spelling out why the void guard is there so a future refactor doesn't accidentally loosen it.

7. Functional procedure body-type check is isFunctional && body'.isTransparent (lines 691 and 731). The duplicated block between resolveProcedure and resolveInstanceProcedure is identical modulo the surrounding scope — easy to factor into a checkFunctionalBodyType helper.

Maintainability / refactoring:

• Repeated pattern do let (e', _) ← resolveStmtExpr a.val; pure e'. It appears at 15+ sites (invariants, decreases, preconditions, invokeOn, constant initializers, type-definition constraint/witness, field-target recursion, etc.). A one-line helper:

  private def resolveStmtExprExpr (e : StmtExprMd) : ResolveM StmtExprMd := do
    let (e', _) ← resolveStmtExpr e; pure e'

  would compress each site to a one-liner and make it obvious which callers are intentionally discarding the type. See inline on checkAssignable.

• Two test files with confusingly similar names. ResolutionTypeCheckTests.lean (9 cases) and ResolutionTypeTests.lean (1 case) both target resolution-time type checking. The naming distinction is TypeCheck vs Type which is not self-explanatory. Consider consolidating — either rename one to something unambiguous (e.g., ResolutionMultiOutputTests.lean) or merge into a single file with clearly named sections. See inline.

Test coverage gaps: the nine scenarios in ResolutionTypeCheckTests.lean cover scalar operations well. Four additions would strengthen the suite materially:

• Instance call argument mismatch. The static-call case is covered; .InstanceCall uses the same checkAssignable loop with the self parameter stripped, which is a logically distinct code path at line 611 and deserves its own test.
• Constant initializer mismatch. resolveConstant threads through the new checker at line 808 but there's no test for const x: int := true.
• User-defined type pass-through documentation. var x: Dog := new Cat should pass silently today. A test that asserts "no diagnostic emitted" pins the known limitation — when the hierarchy check lands later, this test flips and is a reminder to update.
• Assignment target-count mismatch. The arity check at line 505 was the heart of review thread #1 but there's no test like procedure multi() returns (a: int, b: int) opaque; … var x := multi() (one LHS, two RHS). Worth a fixture.

Proof-coverage suggestions. Mostly meta-code, but four invariants are worth stating:

• Soundness. If resolveStmtExpr e returns (e', τ) and no diagnostic is emitted, then e' is well-typed at τ under some formal type system. Stating this formally would require a semantic model for Laurel types; as a lighter-weight intermediate, prove type consistency: the returned τ for a LiteralInt is always .TInt, etc. — which is immediate from the code but stating it pins the correspondence.
• Cascade suppression. For every expression e, if any sub-expression has type .Unknown, then no new diagnostic is emitted at e's level due to that sub-expression. This formalises the intent of the Unknown wildcards in checkBool / checkNumeric / checkAssignable — forget one of those wildcards in a future extension and the invariant fails.
• Arity-match completeness. targets'.length != expectedOutputCount ∧ valueTy ≠ .TVoid → arity diagnostic is emitted. Test #1's concern, formalised.
• UserDefined symmetry. checkAssignable _ tyA tyB is currently not symmetric in general (normal types use highEq), but is symmetric whenever either operand is UserDefined/TCore/Unknown. A small lemma documenting when symmetry holds would make the asymmetric case in Eq/Neq (observation 3) less of a UX footgun.

Inline comments on the two highest-impact items below.

[tautschnig]

Three seams in the new type-check helpers, in decreasing severity.

(a) checkBool and checkNumeric permit .UserDefined _ unconditionally. The comment says "constrained types may wrap bool", which is right in spirit but wrong in general: a plain Color user type will pass checkBool, a Dog composite will pass checkNumeric. The "wraps bool" intuition only applies to .constrainedType whose base resolves to TBool — and for other UserDefined kinds, silently passing is a false negative.

Cheapest tightening: look up the resolved ref's kind and base type, and only fall through for .constrainedType with a compatible base. The existing getVarType / scope API already has everything you need. If that's too invasive for this PR, fine, but at minimum a test that documents the gap (if colorInstance then ... passes without diagnostic — intentional until issue #… tracks the refinement) would give the known limitation a paper trail.

(b) checkAssignable's four UserDefined/TCore wildcards (lines 399–402) are the "no subtype checks" trade-off the PR body calls out. Correct design decision, but deserves a test that asserts var x: Dog := new Cat is silently accepted today, so that when hierarchy tracking lands later, the test flips from passing-without-complaint to correctly-rejecting.

(c) Eq/Neq uses checkAssignable source rhsTy lhsTy at line 571 — asymmetric polarity for a symmetric operator. For 1 == "hello" the user sees "Type mismatch: expected 'string', but got 'int'", which misleadingly frames the LHS as wrong when both sides are symmetric. Two options:

• Drop the check for Eq/Neq (rely on later passes for the rare case someone writes truly incompatible equality).
• Keep the check, but reword the message for the symmetric case — either via a checkComparable helper that emits "operands of '==' have incompatible types '{t1}' and '{t2}'", or by parameterising checkAssignable with an optional operatorName that selects the phrasing.

Also note, as a side-effect of all three points above: since the (e', _) ← resolveStmtExpr a.val; pure e' pattern repeats 15+ times throughout this file (invariants, decreases, preconditions, invokeOn, constants, …), extracting

private def resolveStmtExprExpr (e : StmtExprMd) : ResolveM StmtExprMd := do
  let (e', _) ← resolveStmtExpr e; pure e'

would turn every repeated site into a one-liner and make it obvious which callers are intentionally throwing away the type.

[keyboardDrummer-bot]

Addressed in 2acc758:

(a) Acknowledged — checkBool/checkNumeric still permit .UserDefined _ unconditionally. Tightening this requires resolving the underlying base type of constrained types, which is more invasive than this PR warrants. The userDefinedPassThrough test now documents this gap explicitly.

(b) Added userDefinedPassThrough test that asserts var x: Dog := new Cat produces no diagnostic today. When hierarchy tracking lands, this test should flip to correctly-rejecting.

(c) Fixed. Added a checkComparable helper that emits "Operands of '==' have incompatible types '{t1}' and '{t2}'" for symmetric operators. Eq/Neq now uses this instead of the asymmetric checkAssignable.

Also extracted resolveStmtExprExpr helper — the repeated (e', _) ← resolveStmtExpr e; pure e' pattern is now a one-liner at all call sites outside resolveStmtExpr itself (the ones inside can't use it due to termination proof requirements).

[tautschnig]

Two test files with confusingly similar names for the same concern. ResolutionTypeCheckTests.lean (9 scalar-operator cases) and ResolutionTypeTests.lean (this file — 1 case on multi-output in expression position) both target resolution-time type checking. The distinction TypeCheck vs Type isn't self-explanatory and reads like two different things. Two fixes:

• Merge into one file with clearly named /-! ## … -/ sections. The multi-output test you have here fits naturally under a ## Multi-output procedures section alongside the arity cases.
• Rename this file to something unambiguous, e.g. ResolutionMultiOutputTests.lean, if the author prefers keeping them split.

Four concrete fixtures worth adding either way (see the top-level review body for rationale):

1. Instance-call argument mismatch. The static-call arg check is covered by callArgTypeMismatch in the other file; the .InstanceCall path at line 611 of Resolution.lean strips the first parameter (self) from the check loop, which is a logically distinct code path.
2. Constant initializer mismatch. resolveConstant threads through the new checker at line 808 but nothing exercises const x: int := true.
3. UserDefined pass-through documentation. A fixture that asserts var x: Dog := new Cat produces no diagnostic. Pins the "subtype relationships not tracked here" trade-off; when hierarchy tracking lands later, the test flips from passing-silently to correctly-rejecting.
4. Assignment target-count mismatch. Review thread Add an architecture doc #1's concern about LHS/RHS arity — procedure multi() returns (a: int, b: int) opaque; … var x := multi() should emit the arity-mismatch diagnostic. Worth a positive test of the fix, not just of the error messages.

Also — the processResolution helper is duplicated across both files. If you consolidate, that duplication drops out; if you keep them split, extract the helper into a shared test-util file.

[keyboardDrummer-bot]

Addressed in 2acc758:

• Merged ResolutionTypeTests.lean into ResolutionTypeCheckTests.lean with clearly named /-! ## … -/ sections. The processResolution helper duplication is eliminated.
• Added equalityTypeMismatch test (exercises the new checkComparable helper for symmetric == errors).
• Added assignTargetCountMismatch test (positive test of the LHS/RHS arity check).
• Added userDefinedPassThrough test (documents that var x: Dog := new Cat produces no diagnostic today).

Regarding the instance-call argument mismatch test: the Laurel grammar parser doesn't support dot-notation instance calls (they're only created through the AST translator from other sources). The InstanceCall code path shares the same checkAssignable logic as StaticCall, which is covered by callArgTypeMismatch.

The constant initializer type check was added to resolveConstant in the code, but can't be tested through the parser since const isn't a parseable top-level command in the grammar.

[keyboardDrummer]

@keyboardDrummer-bot please address the feedback from @tautschnig