Compiler error from monad with class parameter

[JamesGallicchio]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

Code fails to compile.

Steps to Reproduce

def MM (τ) := ∀ (_ : Type) [Inhabited Unit], Id τ

instance : Monad MM where
  pure a    := λ _ => pure a
  bind r f  := λ t => bind (r t) (fun x => f x t)

def foo : MM Unit := do
  while False do
    while False do
      pure ()

-- or without do notation
def foo' : MM Unit :=
  forIn Lean.Loop.mk PUnit.unit fun x r =>
    forIn Lean.Loop.mk (ForInStep.done PUnit.unit) fun x r =>
      pure (ForInStep.done <| ForInStep.done <| PUnit.unit)

The type and typeclass arguments to MM are both necessary to reproduce, as are the two nested forIns

Expected behavior: should compile

Actual behavior: error: unknown constant 'Lean.Loop.forIn.loop._at_.board.attempt._elam_4.spec_0'

Versions

Lean (version 4.0.0-nightly-2023-02-22, commit 7992ce6b4dd4, Release)

[Kha]

Works in 4.16.0