to_expr failure

Stream: metaprogramming / tactics

[Markus Himmel]

Hi, does anyone know what's going on in the following snippet?

lemma test (h : true) : true → true :=
λ h, trivial

lemma test' (h : 0 = 0) : true → true :=
λ h, trivial

meta def mk_test : tactic unit :=
do
  e ← tactic.to_expr ``(test trivial),
  tactic.to_expr ``(%%e trivial) >>= tactic.exact

meta def mk_test' : tactic unit :=
do
  e ← tactic.to_expr ``(test' rfl),
  tactic.to_expr ``(%%e trivial) >>= tactic.exact

lemma a : true :=
by mk_test -- works

lemma a' : true :=
by mk_test' -- function expected at `rfl` term has type `?m_2 = ?m_2`

In both cases, infering the type of e gives true → true as expected, but for some reason the second to_expr fails in mk_test'.

[Rob Lewis]

This definitely looks like a bug, one I don't remember seeing before. It seems like the elaborator is ignoring the as_is annotation on e.

[Rob Lewis]

For a bit more explanation: after e ← tactic.to_expr ``(test' rfl), e is a fully elaborated expr. When you insert it into ``(%%e trivial), which is a pexpr, Lean knows that e is already elaborated and makes a note of this. You can see the note if you trace ``(%%e trivial). When you elaborate that pexpr it should know not to touch the thing inside this annotation.

[Markus Himmel]

Thank you for having a look at this. I have opened lean#395.