Add type unification to VCs from procedure pre/post conditions

[joscoh]

Issue #, if available: #398

Description of changes: Performs type unification on generated VCs from (already typechecked) procedure pre and post conditions, so that polymorphic type variables are instantiated before SMT encoding.

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

[joscoh]

CC: @shigoel

[joehendrix]

I asked Claude to review and it had this to say:

  1. (Correctness bug) filterMap + zip can misalign type constraints — StatementEval.lean:148-152

  This is the most important thing to check. In computeTypeSubst:

  let actual_tys := args.filterMap getExprType
  ...
  let input_constraints := actual_tys.zip input_tys

  filterMap drops any arg where getExprType returns none, shrinking the list. zip then pairs by position, so if arg i has no type, arg i+1's type gets paired with formal
  type i, producing an incorrect constraint. For example, if args = [a, b, c] and getExprType yields [some T1, none, some T3], the constraints become [(T1, input_0), (T3,
  input_1)] instead of the intended [(T1, input_0), (T3, input_2)]. The same issue applies to lhs_tys/output_constraints. A zipWith/pairwise approach that keeps index
  alignment (e.g., zip first, then filter pairs where the type is some) would be safer.

It's obvious to me why the zip is ok either.

[joehendrix]

More Claude:

 2. (Design) Silent failure on unification error — StatementEval.lean:154-156

  | .error _ => Subst.empty

  If unification fails, the code silently returns an empty substitution, meaning type variables remain uninstantiated in VCs sent to the SMT solver. Verify this is the
  desired behavior vs. propagating a diagnostic. At minimum, consider whether a warning should be emitted.

[joehendrix]

Could you add some comments about the relationships between the variables in old_var_subst , lhs and E? It's a little unclear to me which typing context the various expressions are in.

[joscoh]

Basically, we are given a term lhs := p(xs) where p takes in arguments of type input_tys and returns arguments of types output_tys. E should contain the types for the free variables in LHS (guaranteed by the StatementEval execution). I believe that old_var_subst has to do with var -> expression maps, not type substitutions. I can add a comment explaining this.

[joehendrix]

Suggested change

	private def computeTypeSubst (input_tys output_tys: List LMonoTy)
	private def computeTypeSubst (input_tys output_tys : List LMonoTy)

[joscoh]

To Joe's comments - the correctness of both of these rely on the fact that the typechecker has already run on the constituent parts so all terms are annotated with their types. The unification must succeed because we are given precondition (or postcondition) p : t1 -> ... -> tn -> t and arguments of types t1, .., tn with LHS of type t. Eventually, we will want to prove this.