Why does the following code doesn't type check?

Stream: new members

[Rui Liu]

def f: Π {x : ℕ}, ℕ := fun (x : ℕ), x

def g (f: Π {x : ℕ}, ℕ): ℕ  := f

#check f

It doesn't check for the definition of g, however, since f has implicit argument, I'd assume f has type ℕ. This is also confirmed by #check f will print ℕ.

[Reid Barton]

f does have type ℕ but Lean has no way to infer what value to provide for the implicit argument, which is what the error message is complaining about

[Reid Barton]

for instance, g @f is a term of type ℕ, but what number should it be?

[Reid Barton]

The function g takes its argument and evaluates it at ...

[Rui Liu]

OK I see, yeah you're right @Reid Barton