On the explicit passing of section variables

Stream: lean4

[Jonathan Laurent]

Why do section variables have to be passed explicitly _within_ the section in which they are defined? For example, consider the following snippet:

section TestSection

  variable {α: Type} (u: Nat)
  def f (x: Nat): Prop := x = u
  def g (x: Nat): Prop := f u x

end TestSection

Here, in the definition of g, f must be passed argument u explicitly. Why were section variables designed this way? I can see three reasons but none of them is very convincing to me:

1. The ability of calling f with another value of u within the section is valuable.
2. Explicitness is deemed a good thing.
3. Allowing to omit such arguments raises implementation and/or tooling challenges (e.g. should terms involving f be printed differently inside and outside the section?)

Reason 1 is unconvincing to me since I would simply not use section variables in those cases, for the sake of clarity. Reason 2 seems to be running against existing mathematical practice, where it is reasonably common to have related definitions and lemmas implicitly depend on a number of fixed objects.

Am I missing other possible motivations?

[Niels Voss]

Lean 3 had a feature called param (or maybe parameter, I can't remember) which did what you wanted but it was removed from Lean 4, although I'm not sure why. It might be worth searching that in this zulip

[Eric Wieser]

I think it was removed because it interacted unexpectedly with other language constructs, and wasn't useful enough to justify the complexity