calc tactic resolves notation incorrectly

[eric-wieser]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
    • Specifically, check out the wishlist, open RFCs,
      or feature requests.
  • Reduced the issue to a self-contained, reproducible test case.

Description

calc, the tactic, is confused by a local variable called eq.

Steps to Reproduce

example (eq : ℕ) : 1 = 1 :=
begin
  calc 1 = 1 : rfl
     ... = 1 : rfl,
end

Expected behavior: No diagnostics

Actual behavior: invalid occurrence of field notation

Reproduces how often: Always

Versions

Lean (version 3.35.1, commit 4887d8a, Release)

[eric-wieser]

I think this is the start of the offending code:

lean/src/frontends/lean/tactic_notation.cpp

Lines 285 to 290 in e4203af

	auto& data = m_p.new_ast("exact_shortcut", pos, m_p.get_token_info().value());
	ast_id arg_ast; expr arg;
	std::tie(arg_ast, arg) = parse_qexpr();
	id = data.push(arg_ast).m_id;
	r = m_p.mk_app(m_p.save_pos(mk_constant(get_interactive_tactic_full_name(m_tac_class, "refine")), pos), arg, pos);
	if (m_use_istep) r = mk_tactic_istep(m_p, r, pos, pos, id, m_tac_class);

[digama0]

I believe the issue is in the quoting and antiquoting that occurs when translating the calc proof to a pexpr to pass to refine. The calc part elaborates to the equivalent of:

example (eq : ℕ) : 1 ≤ 1 :=
by tactic.interactive.refine ``(@eq.trans _ 1 1 1 rfl rfl)

which fails because you can't write @eq.trans when eq is a local variable (which seems like an issue all on its own, but probably for another day). Using calc directly doesn't have this issue because it directly generates an expr.const `eq.trans which can't be misinterpreted.

[digama0]

This is also visible as a difference in how expr vs pexpr quoting is handled:

example (eq : ℕ) : 1 = 1 :=
by exact %%`(@eq.trans _ 1 1 1 rfl rfl) -- ok, uses global eq.trans

example (eq : ℕ) : 1 = 1 :=
by exact %%``(@eq.trans _ 1 1 1 rfl rfl) -- fail, tries to project on the local variable