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.