Problems with variables being unused

Stream: mathlib4

[Thomas Murrills]

There are points where a variable is available but Lean 4 doesn't use it (while Lean 3 did). This causing some issues in the file I'm porting (algebra.group.pi). For example,

theorem update_one [∀ i, One (f i)] [DecidableEq I] (i : I) : update (1 : ∀ i, f i) i 1 = 1 :=
  update_eq_self i 1

fails with error invalid universe level, ?u.79016 is not greater than 0, underlining 1 in red.

Some digging reveals that the real problem comes from trying to take 1 to have the type (a : I) → ?m.79014 a. It should instead be using variable {f : I → Type v} from earlier in the file to give 1 the type (a : I) → f a, using f for the metavariable; this is what Lean 3 does.

(f appears in the tactic state if I start a by ... in the place of 1, so Lean 4 "knows about it".)

It's easy enough to fix here, but I think this reluctancy to use variables (or whatever is actually going on) is somehow what's causing some strange problems with typeclass instance problems getting stuck elsewhere, which are more complicated to solve.

Is this intended behavior? Is there something I should be doing differently to force Lean 4 to use the variables when possible?

[Scott Morrison]

Just add the type annotation?

[Thomas Murrills]

Yes, that's why I said it's easy enough to fix here! :) It's the other cases I'm more worried about. I think I got it working in those other cases too, but it's a bit opaque...and it's actually needed somewhere within the type declaration itself there, which makes it look...not great.

[Thomas Murrills]

Actually, it disappears when used in mouseover, so...maybe it's not a problem from that perspective?