Unexpected kernel error involving two structures

[roos-j]

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

structure A where
  p: Prop
  q: True

structure B extends A where
  q': p → True

example: B where
  p := True ∧ True
  q := by exact True.intro
  q' := λ ⟨_,_⟩ ↦ True.intro

Expected behavior: No errors.

Actual behavior: (kernel) declaration has metavariables '_example'

Mysteriously (to me), any one of the following changes make the error disappear:

• replacing by exact True.intro by True.intro
• replacing ⟨_,_⟩ by _
• moving any of p, q into B (or q' into A)

I originally encountered this example when playing with Mathlib definitions and then simplified it. I don't see how it could be reduced further.

Context

I asked about this on Zulip.

A similar issue is #5925 (pointed out by @kim-em).

If these two issues indeed have the same underlying cause, the present example is maybe simpler to investigate.

Versions

Originally tested on Lean version 4.15.0-nightly-2024-11-15, also still persists on today's version at https://live.lean-lang.org/:

Lean 4.16.0-nightly-2024-12-10
Target: x86_64-unknown-linux-gnu

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

[b-mehta]

I just hit a similar example:

class Preorder (α : Type) extends LE α, LT α where
  le_refl : ∀ a : α, a ≤ a
  lt := fun a b => a ≤ b ∧ ¬b ≤ a

class PartialOrder (α : Type) extends Preorder α where
  le_antisymm : ∀ a b : α, a ≤ b → b ≤ a → a = b

inductive MyOrder : Nat × Nat → Nat × Nat → Prop
  | within {x u m : Nat} : x ≤ u → MyOrder (x, m) (u, m)

instance : PartialOrder (Nat × Nat) where
  le := MyOrder
  le_refl x := .within (Nat.le_refl _)
  le_antisymm | _, _, .within _, .within _ => Prod.ext (Nat.le_antisymm ‹_› ‹_›) rfl

[artie2000]

Similar example: https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Possible.20bug.3A.20.22unknown.20free.20variable.22/near/489831202

[kmill]

Minimized the example further:

structure A where
  p: Prop
  q: True

example := (λ ⟨_,_⟩ ↦ True.intro : (A.mk (And True True) (by exact True.intro)).p → True)

This at least excludes it from being an issue with structure instance notation (where). However, I think we can fix this particular issue by changing how structure instance notation works. The issue basically seems to be that unification isn't able to assign a metavariable that appears inside the matcher generated by λ ⟨_,_⟩ ↦ ... notation (a metavariable that exists because by exact True.intro postpones its elaboration) because it would involve concluding from (A.mk x y).p =?= (A.mk x ?m).p that y =?= ?m, which would not be correct.

Edit: It appears there is a bug in match itself that causes delayed assigned metavariables to be abstracted out incorrectly.