Subgroup definition yields "metavariables" error

Stream: mathlib4

[thielema]

The following simplified code causes the Lean kernel to emit suspicious errors:

import Mathlib
import Lean

def is_primitive_root [Monoid α] (n : Nat) (z : α)
  := ∀ k:ℕ, if n ∣ k then z^k = 1 else z^k ≠ 1

def subgroup_of_primitive_root [Monoid α] {n : Nat} [NeZero n]
  {z : α} (primitive_root : is_primitive_root n z)
  : Subgroup (Units α) where
  carrier := {x | ∃ k, x = z^k}
  mul_mem' {x y} | ⟨k,z_k⟩, ⟨j,z_j⟩ => ⟨k+j, by simp [pow_add, z_k, z_j]⟩
  one_mem' := by use 0; simp [pow_zero]
  inv_mem' {x}
    | ⟨k,z_k⟩ => by
      use (n-1)*k
      sorry

I get the error message:

(kernel) declaration has metavariables 'subgroup_of_primitive_root'

I think this is not intended?

[Edward van de Meent]

i'm not getting this error on the playground...

[Edward van de Meent]

ah, it seems that i do get the error when i specify mathlib stable on the playground...

[Etienne Marion]

This solves the issue. I'm not sure what the problem is exactly but this metavariable message often occurs because of a weird pattern matching (though it seems to be fixed in the latest version in this case).

import Mathlib

set_option autoImplicit false

variable {α : Type*}

def is_primitive_root [Monoid α] (n : Nat) (z : α)
  := ∀ k:ℕ, if n ∣ k then z^k = 1 else z^k ≠ 1

def subgroup_of_primitive_root [Monoid α] {n : Nat} [NeZero n]
  {z : α} (primitive_root : is_primitive_root n z)
  : Subgroup (Units α) where
  carrier := {x | ∃ k, x = z^k}
  mul_mem' := by
    rintro x y ⟨k, z_k⟩ ⟨j, z_j⟩
    exact ⟨k+j, by simp [pow_add, z_k, z_j]⟩
  one_mem' := by use 0; simp [pow_zero]
  inv_mem' := by
      rintro x ⟨k, z_k⟩
      use (n-1)*k
      sorry

[thielema]

Problem occured in 4.14. I confirm it has gone in 4.15.

[thielema]

No sorry, still occurs in 4.15.

[Etienne Marion]

The latest version is 4.16.0-rc2, but it is not a stable release.

[thielema]

Nice, with 4.16.0-rc2 the problem disappears.

[Kyle Miller]

I think it might have been lean4#6414