Lean 'numerals are data… universe polymorphic': a `_` domain in `(2 : _ → R)`

On Lean/Mathlib v4.35.0, example : ℕ → ℝ := (2 : _ → ℝ) fails with 'numerals are data in Lean, but the expected type is universe polymorphic and may be a proposition: ?m → ℝ : Sort (max 1 ?u)'. The hole in the domain is elaborated as an arbitrary Sort, so the function type might be a Prop, and the ascription is elaborated before it is unified with the outer expected type, so the outer type cannot fill the hole in time. Any of these fixes it: drop the ascription (example : ℕ → ℝ := 2 works, since Pi.instOfNat applies once the type is known), name the domain ((2 : ℕ → ℝ)), or leave only the codomain open ((2 : ℕ → _) works). A typical case is s.indicator (1 : _ → ENNReal), where you should write (1 : α → ENNReal) or omit the annotation if the codomain is fixed by the context. If the codomain is open instead, e.g. an unannotated (∑ p ∈ s, (X p).indicator 1) ≤ t.indicator 2, you get a different error: 'typeclass instance problem is stuck: OfNat (α → ?m) 1'.