Metavariables preventing unification

Stream: lean4

[Matej Penciak]

I'm running into a puzzling situation. I've been able to minimize it to the following MWE:

inductive HList {α : Type v} (β : α → Type u) : List α → Type (max u v) where
| nil : HList β []
| cons : ∀ {a : α} {as : List α}, β a → HList β as → HList β (a :: as)

@[reducible] def tester (x : HList Fin [1]) : Nat := match x with
| HList.cons _ HList.nil => 0

example : ∃x, tester (HList.cons x HList.nil) = 0 := by
  apply Exists.intro
  · try rfl -- Doesn't unify
    with_unfolding_all rfl -- Does unify
  · exact 0

I would expect the first try rfl to work. It seems like the unresolved metavariable is preventing Lean from seeing through the defeq (if you fill in the metavariable before trying rfl it works with no problem) though... If that was it, I suppose I'd be satisfied with "this just doesn't work". The weird thing is with_unfolding_all must be doing something beyond just unfolding definitions, because with_unfolding_all rfl does work, despite the metavariable still being there!

I've tried to parse through the trace.Meta.isDefEq traces but I wasn't able to gather much from them (maybe I should be looking at something else?) What exactly is preventing the unification from going through in the first case, and what is with_unfolding_all doing to make it work in the second?

[Sebastian Ullrich]

It's because match is semireducible

[Marcin Kostrzewa]

@Sebastian Ullrich is there any way to control that? For example, the same works for Lists:

def tester2 (x : List Nat): Nat := match x with
| _ :: _ => 0
| _ => 1

example : ∃x, tester2 [x] = 0 := by
  apply Exists.intro
  · rfl
  · use 17

Making the HList matcher reducible would definitely help, given we have examples like this all over our codebase.

[Robin Arnez]

defeq doesn't always play nice with metavariables.
try:

example : ∃ x, tester (HList.cons x HList.nil) = 0 := by
  refine ⟨?_, ?_⟩
  · exact 0
  · rfl

[Marcin Kostrzewa]

Thanks, but this is just an artificial example distilled down from the actual problem. The actual problem pops up in a custom tactic that uses apply with user-provided theorems. So to avoid these mvars we'd have to parse the provided theorem and figure out the assignments ourselves – not impossible, but pretty much duplicating the work that apply should be doing and re-solving the problem that mvars were invented to solve. If we could just get the HList recursor to play nicely that would be awesome. Also not ruling out just bumping the transparency setting for that tactic, but I'm worried about the performance impact of that.

[Robin Arnez]

You can try to use goal.apply e { newGoals := .all } (MVarId.apply) if you want to avoid this problem

[Robin Arnez]

(I don't know what exactly your tactic aims to do so I can't tell whether this applies)

[Robin Arnez]

With batteries, you can also use fapply if you want macro instead of elaboration

[Marcin Kostrzewa]

So the whole issue happens inside the call to apply, our problem is not "we ended up with weird mvars", the problem is "apply creates mvars and then cannot unify the term it created with the goal". We start from an mvar-free goal, try to apply a theorem and apply fails and deep within the traces of isDefEqs the actual reason for failure _looks like_ what we've recreated with the apply Exists.intro above. But the mvar that blocks the unification is not the result of us doing something weird, it's the result of apply working correctly and then isDefEq not being able to deal with that.

And the transparency stuff comes in at the apply level – we have apply foo failing and with_unfolding_all apply foo succeeding. We've just trimmed it down to this tiny repro to avoid having to copy-paste a bajillion auxiliary definitions. Sorry if I wasn't clear enough with the real nature of this.