Add an inference-idempotence test group (infer ∘ infer ≡ infer)

[joshsh]

Inference/elaboration in hydra.inference maps terms to their elaborated System F form, inserting explicit type applications (e⟨τ⟩) and abstractions (Λv.e). Because Hydra uses a single Term grammar for both untyped and elaborated terms (unlike the paper's Term₀ ⇝ Term, which is two grammars), inference must be well-defined on terms it has already elaborated — and we deliberately avoid a "is this term already typed?" validation gate.

The property we want is idempotence: for any term e, running inference a second time reproduces the same elaborated term and type.

infer(infer(e)) ≡ infer(e)

Note this is not preservation of pre-existing annotations. Inference may strip a ⟨τ⟩/Λ and regenerate it; idempotence only requires that any elaboration added by the first pass is still present (up to type-variable normalization) after the second.

Current state: no idempotence test exists (no infer∘infer coverage in the kernel or any host test suite). The re-inference cases inferTypeOfTypeApplication and inferTypeOfTypeLambda strip their wrapper and re-infer the body, so the second pass re-instantiates at fresh type variables; convergence then depends on normalizeTypeVariablesInTerm at finalization canonicalizing both passes to the same names. Whether that always holds is exactly what this test would establish — it is currently unverified.

Proposed:

1. A test group that, for a corpus of terms, asserts infer(infer(e)) ≡ infer(e) (comparing elaborated term + inferred type modulo type-variable normalization — i.e. the checker's existing typesEffectivelyEqual/normalization notion, applied to terms).
2. Consider auto-deriving one idempotence case per existing inference/elaboration test case, so coverage tracks the inference suite automatically rather than needing a hand-maintained corpus.

Caveats:

• Performance. Auto-deriving doubles (≥) inference work for every inference test. If that is material for the larger suites, gate the auto-derived group behind a flag or run it over a representative subset rather than all cases.
• Equality notion. "≡" must be the normalized/effective equality, not raw structural equality, since fresh-variable names legitimately differ between passes. Reusing the checker's normalization keeps this principled.
• If the test fails, the fix is in inferTypeOfTypeApplication/inferTypeOfTypeLambda (and/or finalization normalization), not in the test — idempotence is the intended property.

Relates to #377 (inference/paper alignment): the re-inference cases are the code-side realization of the single-Term-grammar decision, which the paper covers as appendix/footnote material rather than as core inference rules.