Lambda type aliases: report arity mismatch instead of silent fallthrough

[MikaelMayer]

Fixes #1239

Summary

aliasDef? and tconsAlias now report a clear arity mismatch error when a type constructor name matches a registered alias but with the wrong number of type arguments. Previously, this case was silently treated as "no matching alias" and the original unresolved type was returned, leading to confusing downstream type errors.

Approach

Added LMonoTy.checkAliasArity which looks up aliases by name only and checks arity. It's called in tconsAlias (in the none branch, after the name+arity find fails) and in aliasDef? (before calling tconsAliasSimple). The pure tconsAliasSimple and resolveAliases functions are unchanged to minimize proof impact.

Testing

Existing tests pass. Updated one test that was demonstrating the bug (silently returning the unresolved type on arity mismatch) to expect the new error. Added a new test exercising the arity mismatch scenario from the issue.

[MikaelMayer]

🤖⛏️

Design decisions:

• The arity check is added to tconsAlias and aliasDef? (the two functions mentioned in the issue title) but not to resolveAliases directly. resolveAliases calls tconsAliasSimple (a pure function) and is referenced by ~10 proofs that reason about its computational structure. Adding the check there would require updating all those proofs. Since resolveAliases is always called through aliasDef? or directly from ProgramType.lean (which wraps errors with .mapError), the arity check in aliasDef? covers the main entry point. The resolveAliases path from ProgramType.lean won't get the check — this could be addressed in a follow-up if needed.

• The existing test at line 72 was demonstrating the bug (calling myInt with 0 args when the alias expects 1, silently returning myInt). Updated it to expect the new error message since this is the intended behavior change.

[MikaelMayer]

🤖🔍 Clean, well-scoped PR. The checkAliasArity helper is a good design choice — it's pure, reusable across both aliasDef? and tconsAlias, and the proof adaptations are minimal and correct. The updated test legitimately demonstrates the bug fix (silent fallthrough → clear error), and the new test covers the scenario from the issue.

One observation: LMonoTy.resolveAliases still uses tconsAliasSimple directly without the arity check. The PR description explicitly states this is intentional to minimize proof impact, which is reasonable given the heavy proof machinery around resolveAliases. Worth noting for future work if users hit the same silent fallthrough via that path.

[MikaelMayer]

🤖🔍 Nit: find? returns the first alias matching by name. If the alias list ever contains multiple entries with the same name but different arities (e.g., overloaded aliases), the error message will report the arity of whichever appears first, which may not be the one the user intended. Consider whether the error message should list all registered arities for that name (e.g., "expected 1 or 3 type argument(s)").

Context

This is a minor edge case — if aliases are unique by name (which seems likely given the AliasesWF invariant), this is a non-issue. But if overloading by arity is ever supported, this would produce a confusing message.

[MikaelMayer]

🤖 Good observation. As you noted, aliases are unique by name in the current system — TContext.AliasesWF ensures per-alias well-formedness, and the alias registration path does not allow duplicate names. The tconsAlias function already matches by name+arity, so checkAliasArity is only reached when no exact match exists. If overloading by arity is ever supported, we would need to revisit this, but for now the single-arity message is correct.