Type soundness: if/loop guards silently refine an enclosing procedure's rigid type variable

[joscoh]

Summary

The ite and loop branches of Statement.typeCheckAux.go (in Strata/Languages/Core/StatementType.lean) do not enforce the rigid-type-variable invariant. They resolve their guards/conditions/measures/invariants via bare LExpr.resolve — which runs Constraints.unify internally and can refine a rigid type variable — then perform only a structural bool/int check and never run checkAnnotCompat. So a refinement of a procedure's rigid type parameter during guard resolution is silently accepted.

This is the direct ite/loop analogue of #1397 (which was the .call branch). Commands (init/set/assert/…) run checkAnnotCompat via Imperative.Cmd.typeCheck, and the .call branch was given the same check in #1397 — but ite/loop guards still lack it.

Minimal example

procedure Foo<a>(x : a)
spec { ensures true; }
{
  if (x && true) {     // guard forces `x : bool`, refining rigid `a := bool`
  } else {
  }
};

Core.typeCheck accepts this. The sound result is a type error:

Rigid type variable 'a' was refined to 'bool'

The directly analogous command form — assert [p]: (x && true); in the same procedure body — is correctly rejected with that error. The if/loop guard form should behave the same way.

Proposed fix

Mirror the #1397 fix: add let _ ← CmdType.checkAnnotCompat C Env in the ite and loop branches of StatementType.lean, after the guard/measure/invariant resolution and before recursing into the bodies.

Related: #1397