match pattern variable contains metavariables

Stream: lean4

[Yaël Dillies]

I have just minimised the following from #12572:

variable {α : Type}

instance [Setoid α] (p : α → Prop) : Setoid (Subtype p) := .mk (fun s t ↦ (s : α) ≈ (t : α)) sorry

inductive Perm : List α → List α → Prop

instance List.isSetoid (α) : Setoid (List α) := .mk Perm sorry

def Multiset (α : Type) : Type _ := Quotient (List.isSetoid α)

def Multiset.card (s : Multiset α) : Nat := sorry

def Equiv.subtypeQuotientEquivQuotientSubtype (p₁ : α → Prop) {s₁ : Setoid α}
    {s₂ : Setoid (Subtype p₁)} (p₂ : Quotient s₁ → Prop)
    (h : ∀ x y : Subtype p₁, s₂.r x y ↔ s₁.r x y) : {x // p₂ x} → Quotient s₂ := sorry

def Sym.oneEquiv (s : {s : Multiset α // Multiset.card s = 1}) : α :=
  (Equiv.subtypeQuotientEquivQuotientSubtype (·.length = 1) _ (fun l l' ↦ by rfl) s).liftOn
    sorry
    fun ⟨_, _⟩ ⟨_, h⟩ hperm ↦ sorry
/-
invalid match-expression, type of pattern variable 'hperm' contains metavariables
  ⟨val✝¹, property✝⟩ ≈ ⟨val✝, h⟩
-/

def Sym.oneEquiv' (s : {s : Multiset α // Multiset.card s = 1}) : α :=
  (Equiv.subtypeQuotientEquivQuotientSubtype (·.length = 1) _ (fun l l' ↦ by rfl) s).liftOn
    sorry
    fun ⟨_, _⟩ ⟨_, h⟩ ↦ fun hperm ↦ sorry
-- works fine

[Yaël Dillies]

Does anybody know why breaking up the fun into two funs makes the problem go away?

[Damiano Testa]

My guess is that destructuring within fun uses much less information to figure out what metavariables should be. Once the fun is done, though, some metavariables get assigned and then Lean is happy with hperm (that depends on the previously destructured variables). :shrug:

[Kyle Miller]

If you hover over everything in ⟨val✝¹, property✝⟩ ≈ ⟨val✝, h⟩, there doesn't seem to be a metavariable in sight. I wonder if there's a bug where match isn't instantiating metavariables?