"(kernel) unknown constant" when specializing a mutually recursive function

[JovanGerb]

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

The following minimized example yields a "(kernel) unknown constant" error message:

variable {m : Type → Type} [Monad m]

mutual
  partial def A : m Unit := do
    pure ()
    B

  partial def B : m Unit := do
    pure ()
    A
end

def oops : ReaderT Unit (ReaderT Unit Id) Unit := A
-- (kernel) unknown constant 'A._at.oops._spec_1'

Context

I was doing some programming, and got the "(kernel) unknown constant" error. I posted it on Zulip.

Steps to Reproduce

1. Define a mutually recursive function like this one:

variable {m : Type → Type} [Monad m]

mutual
  partial def A : m Unit := do
    pure ()
    B

  partial def B : m Unit := do
    pure ()
    A
end

2. Specialize it to a monad stack that includes at least two of the set {ReaderT, StateT, StateRefT}

Expected behavior: [Clear and concise description of what you expect to happen]

The function can be executed.

Actual behavior: [Clear and concise description of what actually happens]

Compilation of the function throws an error.
A fix that I've found is to add the following instance that overwrites the default instance, which only differs from the default in having the @[inline] annotation:

@[inline]
instance {m : Type → Type} {ρ : Type} [Monad m] : Monad (ReaderT ρ m) where
  bind := ReaderT.bind

Versions

4.13.0-rc3

Additional Information

[Additional information, configuration or data that might be necessary to reproduce the issue]

Impact

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