fix: instantiate and normalize level metavariables in getLevel

[sgraf812]

This PR adds instantiateLevelMVars and normalize to Meta.getLevel so that it returns fully resolved universe levels. Previously, getLevel returned levels with assigned-but-unsubstituted metavariables, causing getDecLevel to fail on sort-polymorphic types with Prop components.

For example, PProd.{?u, ?v} Nat True has sort Sort (max 1 ?u ?v). After ?u := 1 (from Nat : Sort 1) and ?v := 0 (from True : Sort 0), this is Sort (max 1 1 0) which normalizes to Sort 1, easily decremented to 0. But without instantiation, getLevel returns the level max 1 ?u ?v — and it is in general impossible to decrement max 1 ?u ?v without information loss (any component might be 0). Only after instantiation and normalization does the level become decrementable.

The cost of instantiateLevelMVars + normalize is negligible compared to the inferType + whnfD already in getLevel.

[sgraf812]

!bench

[leanprover-radar]

Benchmark results for 2d24377 against 82bb27f are in. There are no significant changes. @sgraf812

• 🟥 build//instructions: +3.9G (+0.03%)

Small changes (5✅, 4🟥)

• ✅ build/module/Lean.Data.EditDistance//instructions: -14.1M (-1.03%)
• ✅ build/module/Lean.Language.Lean//instructions: -49.4M (-0.67%)
• ✅ build/module/Lean.Meta.Constructions.BRecOn//instructions: -25.3M (-0.50%)
• ✅ build/module/Lean.Meta.Match.MatchEqs//instructions: -35.4M (-0.51%)
• ✅ build/module/Lean.Meta.Match.MatcherApp.Transform//instructions: -43.3M (-0.73%)
• 🟥 build/module/Lean.Meta.Tactic.Grind.Arith.Cutsat.Types//instructions: +343.6M (+1.34%) (reduced significance based on absolute threshold)
• 🟥 elab/bv_decide_mul//task-clock: +115ms (+3.97%)
• 🟥 elab/bv_decide_mul//wall-clock: +112ms (+3.81%)
• 🟥 elab/bv_decide_realworld//wall-clock: +62ms (+5.48%)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-04-07 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-04-09 09:11:47)

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-13343 has successfully built against this PR. (2026-04-09 10:05:38) View Log