application / elaboration confusion

Stream: general

[Gihan Marasingha]

I've written a simple function that fails in a way that I don't understand.

def foo : ℕ → list (ℤ → ℤ)
  | 0 := []
  | (n+1) := (λ x, x + n) :: foo n

-- The following gives the error message "function expected at `f` term has type `?m_`"
def bar (n : ℕ) (x : ℤ) : list ℤ := list.map (λ f, f x) (foo n)

This confuses me because the infoview shows f : ℤ → ℤ.

However, it works fine if I state the type of f explicitly:

def bar2 (n : ℕ) (x : ℤ) : list ℤ := list.map (λ f : ℤ → ℤ, f x) (foo n)

It also works if I use a higher-order function for application.

def appf (f : ℤ → ℤ) (x : ℤ) : ℤ := f x

example (f : ℤ → ℤ) (x : ℤ) : appf f x = f x := rfl

def bar3 (n : ℕ) (x : ℤ) : list ℤ := list.map (λ f, appf f x) (foo n)

But it fails again if I use a generic version of the application function:

def appf2 {α β} (f : α → β) (x : α) : β := f x

/- The function `bar4` gives the following error message:
type mismatch at application appf2 f term f has type ?m_1 : Type ?
but is expected to have type ?m_1 → ℤ : Sort (max ? 1)
-/
def bar4 (n : ℕ) (x : ℤ) : list ℤ := list.map (λ f, appf2 f x) (foo n)

What's going on? Why is it that the Infoview shows f : ℤ → ℤ but this type information seems to be ignored in elaboration?

[Floris van Doorn]

Not exactly sure, but it is probably related to the fact that Lean

• Elaborates arguments from left to right (so it tries to figure out what (λ f, f x) means before looking at foo n
• Is not great with function types involving metavariables

I'm not quite sure why the infoview gives the correct answer here. Usually the correct response to these problems is to just give a little more information to Lean. If you desperately don't want to give more information, write (foo n).map (λ f, f x).

[Gihan Marasingha]

Thanks! Fortunately, I'm not desperate to not give more information to the elaborator.