list.rec_on foo different from foo.rec_on?

Stream: new members

[Martin C. Martin]

The following gives me a type error:

def lookup (env : list (ℕ × ℕ)) (var_num : ℕ): ℕ :=
  env.rec_on
    99
    (λ var_value tail tail_val, cond tt 23 tail_val)

But if I replace env.rec_on with list.rec_on env everything is happy. I thought these were the same? What's the difference?

[Eric Wieser]

Dot notation changes the elaboration order, and the resulting order probably doesn't work for recursors due to some higher order unification issue

[Kyle Miller]

I spent a few minutes trying to figure out what the elaborator is doing differently, but I only got as far as seeing that dot notation doesn't immediately call visit_elim_app, which is what elaborates things that have the elab_as_eliminator attribute.

You can help it out with a type hint:

def lookup (env : list (ℕ × ℕ)) (var_num : ℕ): ℕ :=
  env.rec_on
    99
    (λ var_value tail (tail_val : ℕ), cond tt 23 tail_val)

But I'd recommend that you use the equation compiler:

def lookup : list (ℕ × ℕ) → ℕ → ℕ
| [] _ := 99
| (var_value :: tail) var_num := cond tt 23 (lookup tail var_num)

[Martin C. Martin]

Thanks. One confusing thing was that, VS Code was telling me that tail_val was already of type \N, but it seems the actual Lean environment was following different rules and came to a different conclusion.

I'm on to chapter 8 of TPiL now, so starting to learn about the equation compiler. Thanks again for all your help.

[Kyle Miller]

It might eventually come to that conclusion, but it appears that while it is elaborating cond it has the type ?m_1 tail, where ?m_1 is a metavariable that hasn't been filled in by the elab_as_eliminator procedure yet.

9:33: type mismatch at application
  cond tt 23 tail_val
term
  tail_val
has type
  ?m_1 tail
but is expected to have type
  ?m_1 (var_value :: tail)