failed to unify Finset Membership instances

Stream: mathlib4

[Moritz R]

How can i debug this unification failure any further?
image.png
If i type out

lemma bla [DecidableEq α] (a : α) : a ∈ ({a} : Finset α) := by simp

it works

[Moritz R]

Hovering {a} shows @singleton α (Finset α) Finset.instSingleton a : Finset α

[Moritz R]

Hovering {?a} shows @singleton ?α (Finset ?α) Finset.instSingleton ?a : Finset ?α

[Yury G. Kudryashov]

Please post a #mwe

[Yury G. Kudryashov]

One reason for simp to ignore a lemma like this is a mismatch in types.

[Moritz R]

Well if i type out the lemma one line above in the same file it doesn't fail!

[Moritz R]

solve_by_elim and grind would work for the goal in the simp-fail situation

[Yury G. Kudryashov]

For a simple goal like this, you can set pp.all true and see what are the types.

[Moritz R]

Are any types missing in my photo + text

[Yury G. Kudryashov]

Did you read #mwe?

[Moritz R]

yes?

[Yury G. Kudryashov]

A photo is not a #mwe

[Yury G. Kudryashov]

It has no code that leads to this goal.

[Moritz R]

of course. But i can't reproduce

[Moritz R]

I can't even reproduce one line above in the same file

[Moritz R]

How am i supposed to get a #mwe

[Yury G. Kudryashov]

You have some non-minimal example. You can start with that.

[Yury G. Kudryashov]

Moritz R said:

Are any types missing in my photo + text

There are lots of missing types/instances behind a \in {a} that become visible with pp.all.

[Moritz R]

image.png

[Moritz R]

Is there a way to get a trace for what the unifier tried and when it gave up?

[Moritz R]

im lucky, it only depends on very few defs

[Moritz R]

And i can reproduce with them

[Moritz R]

import Mathlib.Data.Finset.Union
import Mathlib.Data.Fintype.Basic

inductive Term (F : ℕ → Type*) (α : Type*) where
  | var : α → Term F α
  | func : ∀ (n : ℕ) (_f : F n) (_ts : Fin n → Term F α), Term F α
export Term (var func)

namespace Term

variable {α : Type*} {F : ℕ → Type*}

/-- The collection of all variables that appear in a given term. -/
@[simp]
def varFinset [DecidableEq α] : Term F α → Finset α
  | .var a => {a}
  | .func _ _ ts => Finset.univ.biUnion (fun i ↦ Term.varFinset (ts i))

/-- The embedding of `↥(ts i).varFinset` (as a type) into `↥(func n g ts).varFinset` (as a type). -/
abbrev argInclusion [DecidableEq α] {n} {g : F n} {ts : Fin n → Term F α} {i : Fin n} :
    ↥(ts i).varFinset → ↥(func n g ts).varFinset :=
  (Set.inclusion (Finset.subset_biUnion_of_mem (fun i => Term.varFinset (ts i)) (Finset.mem_univ i)))


/-- Restricts a term to use only a set of the given variables. -/
def restrictVar [DecidableEq α] : ∀ (t : Term F α) (_f : t.varFinset → β), Term F β
  | var a, f => var (f ⟨a, Finset.mem_singleton_self a⟩)
  | func n g ts, f => func n g (fun i => (ts i).restrictVar (f ∘ argInclusion))

lemma restrictVar_var [DecidableEq α] (a : α) (g : (var a).varFinset → β) :
  (var a : Term F α).restrictVar g = var (g ⟨a, by simp [Finset.mem_singleton]⟩) := by sorry

[Yury G. Kudryashov]

It looks like Mathlib provides both SetLike and Membership instances, and Lean fails to see that they're defeq.

[Notification Bot]

This topic was moved here from #lean4 > failed to unify by Yury G. Kudryashov.

[Yury G. Kudryashov]

@Moritz R I've moved the topic here, since it's about Mathlib, not core Lean.

[Yury G. Kudryashov]

This may be related to the recent change in what definitions Lean unfolds while unifying instances.

[Yury G. Kudryashov]

But I think that we should drop the Membership instance and use the one coming from SetLike instead.

[Robin Arnez]

Seems like

unif_hint (s : Finset α) (a : α) where
  ⊢ (SetLike.coe s).Mem a =?= s.val.Mem a

would fix the issue.