Metavariables in types of local hypotheses

Stream: metaprogramming / tactics

[Eric Wieser]

Is this expected behavior?

example : ∀ (y : ℕ), y ≤ 37 → true :=
begin
  refine λ y hy, _,
  do {
    [y, hy] ← tactic.local_context,
    t ← infer_type hy,
    tactic.trace t.is_mvar },
  trivial
end

This traces tt, which foils attempts at matching on t syntactically

[Eric Wieser]

This isn't hypothetical: the following code fails because interval_cases expects infer_type not to contain metavariables:

import tactic.interval_cases

example : ∀ y, y ≤ 37 → true :=
begin
  refine λ y hy, _,  -- replace with `intros y hy` and it works
  interval_cases y,
  all_goals { trivial },
end

[Jannis Limperg]

Probably needs an instantiate_mvars. As a general rule, it's safer to assume that mvars are never fully instantiated except directly after instantiate_mvars.

[Eric Wieser]

So in general, matching against an expression without a instantiate_mvars is pretty much always a bug?

[Jannis Limperg]

Syntactic matching yes, very likely.

[Eric Wieser]

Another failure:

example : ∀ (y : ℕ), y ≤ 37 → y < 40 :=
begin
  refine λ y hy, _,    -- replace with `intros y hy` and it works
  linarith
end

[Eric Wieser]

Fixed in !3#19232 and !3#19233

[Eric Wieser]

These won't need forward-porting, but for anyone still working on downstream projects in Lean 3 I think they're worth merging

[Eric Wieser]

Just found this old thread