Inconsistent automatic passing of section variables

Stream: lean4

[Simon Dima]

I am very confused about the way section variables are passed.

section S
variable {x: Unit}
include x

mutual
def f n :=
  match n with
  | 0 => let _ := x; 0
  | n+1 => g n

def g n :=
  match n with
  | 0 => 1
  | n+1 => f n
end

def h n := f n -- error: don't know how to synthesize implicit argument 'x'

end S

Here, the recursive calls to g and f in the body of f resp. g do not require the argument x to be passed explicitly. However, when h calls f, Lean seems to be trying (and failing) to find an appropriate x by implicit argument resolution instead of using the section variable.

To add to my confusion, the above code works without an error if the definition of h is moved inside the mutual block or if the section variable x is defined with regular binders (x: Unit).

Here is another example which behaves slightly differently:

section S

variable {n: Nat} {H: n = 0}
include n H

def notone: (n = 1) -> False := by
  intro
  rewrite [H] at *
  contradiction

def f (H': n = 1): Bool :=
  False.elim (notone H') -- error: don't know how to synthesize implicit argument 'H'

end S

Here, changing the binders of the section variables from implicit to regular does not solve the error, but wrapping notone and f inside a mutual block does allow f to call notone without explicitly specifying the parameter H.

What is going on in these two examples? Why is it the case that the section variables sometimes need to be passed explicitly and sometimes are inserted automatically at function calls?
The relevant section of the reference manual does not address this.

[Etienne Marion]

I don't know how mutual def really works, but as f is defined in the same as g it does not surprise me that lean is able to infer x from the definition of f. In your definition of h however, how is lean supposed to infer what x is? Implicit variables can only be inferred if they are referred to by explicitly provided variables, which is not the case here. Note that when you make x explicit, what happens in the definition of h is that n is interpreted as a unit element and f n as a function from Nat to Nat. I think it would be easier to see what's going on if you declared all your variables and their types, as well as the types of your defs.

[Simon Dima]

Etienne Marion said:

Note that when you make x explicit, what happens in the definition of h is that n is interpreted as a unit element and f n as a function from Nat to Nat.

Ah, thanks, that does explain what was going on with the binders.

I'm still quite curious about what's going on in the mutual blocks, I don't see why that would change the way section variables are passed.

[Aaron Liu]

Mutual blocks are weird, sometimes I have a recursive call to a mutual function that doesn't typecheck but when I make all the implicit arguments explicitly by filling them in with _ then it typechecks