Unknown constant ...._spec_N

Stream: lean4

[cognivore]

@Matej Penciak has reduced a fail case I discovered:

import Lean.Data.Parsec

open Lean

variable {α β : Type} {φ : Type → Type} [Monad φ] [Alternative φ]

mutual
  partial def mut1 [Inhabited (φ $ List α)] (p : φ α) (sep : φ β) : φ (List α) :=
    (sep *> mut2 p sep)
  partial def mut2 [Inhabited (φ $ List α)] (p : φ α) (sep : φ β) : φ (List α) :=
    mut1 p sep <|> pure []
end

partial def problem : Parsec Nat := do -- (kernel) unknown constant 'mut2._at.problem._spec_1'
  let asdf ← mut2 (pure 1) (pure 2)
  pure 3

It seems like a Lean 4 bug, but I don't understand what does it mean.

Please suggest a way to proceed.

[Leonardo de Moura]

This is a bug in the code generator. Could you please create an issue on GitHub?

[cognivore]

https://github.com/leanprover/lean4/issues/1573 I hope this will work.