A "declaration has metavariables" error

[mik-jozef]

Prerequisites

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

• Check that your issue is not already filed.
• Reduce the issue to a minimal, self-contained, reproducible test case.
• Test your test case against the latest nightly release.

Description

The following code

structure ValVar (D: Type) where
  d: D
  x: Nat

def Set (T : Type) := T → Prop

structure Salg where
  D: Type
  I: Nat

def natSalg: Salg := { D := Nat, I := 42 }

inductive HasMem (salg: Salg): Set (Set (ValVar salg.D))
| hasMem
  (set: Set (ValVar salg.D))
  (isElem: set ⟨d, x⟩)
:
  HasMem salg set

def valVarSet: Set (ValVar Nat) :=
  fun ⟨d, x⟩ => x = 0 ∧ d = 0 ∧ d ∉ []

def valVarSetHasMem: HasMem natSalg valVarSet :=
  HasMem.hasMem
    valVarSet
    (show valVarSet _ from ⟨rfl, rfl, nofun⟩)

throws (kernel) declaration has metavariables 'valVarSetHasMem'.

There is a list of things that make the issue go away (which is also why I couldn't come up with a more specific title -- I've no idea what the underlying cause is :sorry:):

• removing x from ValVar, along with its occurences in the rest of the program
• removing I from Salg
• removing the salg param from HasMem & replacing occurences with natSalg
• removing d ∉ [] from the definition of valVarSet
• replacing HasMem.hasMem valVarSet with HasMem.hasMem _ in valVarSetHasMem.
• replacing show valVarSet _ from with show _ from, show valVarSet ⟨0, 0⟩ from, or removing it entirely.

Expected behavior: The code throws no errors.

Versions

Version: Lean 4.14.0-nightly-2024-11-01
Platform: live.lean-lang.org

Impact

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

[Komyyy]

We have the similar issue:

open Function

theorem my_mul_right_injective {M₀ : Type} [Mul M₀] [Zero M₀] {a : M₀} (ha : a ≠ 0) :
  Injective fun (x : M₀) ↦ a * x := sorry

-- (kernel) declaration has metavariables 'mul2'
def mul2 : { f : Nat → Nat // Injective f } := ⟨fun x : Nat ↦ 2 * x, mul_right_injective nofun⟩

[kmill]

Note: this issue's example doesn't typecheck on a recent Lean, I think because of the changes in #6024. In the tests for #6414 I added the following unification hint to make up for the difference:

unif_hint (s : Salg) where
  s =?= natSalg
  |-
  Salg.D s =?= Nat

Unfortunately, this covers up the issue in 4.14. I figure it's still worth including the example in #6414 as a regression test, but it would be better if we could observe that this issue has been fixed.

testing on stable mathlib live-lean, which is currently 4.14

[mik-jozef]

While updating Lean to v4.15.0-rc1, I noticed this issue is still present in my project. So here's another (less successfully) minified example that reproduces on latest Mathlib. It no longer reproduces on Lean nightly, so we have a confirmation the issue us gone.

def Set (D: Type) := D → Prop

structure ValVar where
  d: Empty
  x: Nat

structure Salgebra where
  D: Type
  I: Empty → Empty

def pairSalgebra: Salgebra := ⟨Empty, nofun⟩

structure Cause (D: Type) where
  contextIns: Set Nat

mutual
inductive Ins (salg: Salgebra): Prop

inductive IsCauseInapplicable (salg: Salgebra):
  Cause salg.D → Prop

| blockedContextIns
  (cause: Cause salg.D)
  (inContextIns: cause.contextIns 0)
:
  IsCauseInapplicable salg cause
end

def IsVarFree (x: Nat): Prop := ∀ d, ValVar.mk d x ∉ []

def extOfIntCause
  (internalCause: Cause Empty)
:
  Cause Empty
:= {
  contextIns :=
    fun _ => ∃ vvI, internalCause.contextIns vvI ∧ IsVarFree vvI
}

def insInternalToInsExternal
  (isInapp: IsCauseInapplicable pairSalgebra internalCause)
:
  IsCauseInapplicable pairSalgebra (extOfIntCause internalCause)
:=
  isInapp.rec
    (motive_1 := fun _ => True)
    (motive_2 :=
      fun cause _ =>
        IsCauseInapplicable pairSalgebra (extOfIntCause cause))
    (fun cause inCins =>
      IsCauseInapplicable.blockedContextIns
        (salg := pairSalgebra)
        (extOfIntCause cause)
        (⟨_, inCins, nofun⟩))

[kmill]

Thanks @mik-jozef, I've added this as a regression test in #6511 (and once I actually get around to verifying that the fix I think fixed it fixed it, I'll merge).