Weird behaviour of section variables in match

Stream: lean4

[Daniel Weber]

What's going on here in S2 here?
First of all, why is a even included, under the new variable inclusion mechanism? It isn't mentioned in the type of the function and isn't an instance.
Second, how come somefun2 is invoked without having to pass a to it?

set_option autoImplicit false

section S1

def somefun (a : Nat) : Nat → Nat
| 0 => a
| n+1 => somefun a n

end S1

section S2

variable (a : Nat)

def somefun2 : Nat → Nat
| 0 => a
| n+1 => somefun2 n

end S2

[Kyle Miller]

Here's the relevant release notes entry:

The variable inclusion mechanism has been changed. Like before, when a definition mentions a variable, Lean will add it as an argument of the definition, but now in theorem bodies, variables are not included based on usage in order to ensure that changes to the proof cannot change the statement of the overall theorem. Instead, variables are only available to the proof if they have been mentioned in the theorem header or in an include command or are instance implicit and depend only on such variables. The omit command can be used to omit included variables.

I thought it was just theorem (and Prop-valued example?) that used the more restrictive inclusion rule.

[Daniel Weber]

Ah, I see, thanks (it only happens for theorem, not example)