Missing fields error despite minimal instance implementation for Monad

[sgraf812]

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

When I implement pure and bind of Monad, I get a missing fields error, prompting me to implement map, mapConst, seq, seqLeft as well.
If I extract the code for bind, the error goes away.

Steps to Reproduce

Check this file (live.lean-lang.org):

-------------------------------------------
-- Guarded recursion and the Later modality
universe u v

axiom Later : Sort u → Sort u
axiom next {α : Sort u} (a : PUnit → α) : Later α
axiom ap {α β : Sort u} (f : Later (α → β)) (a : Later α) : Later β
axiom gfix {α : Sort u} (f : Later α → α) : α

axiom DLater : Later (Sort u) → Sort u
axiom DLater.next_eq {α : Sort u} : Later α = DLater (next (fun () => α))

----------------------------------------
-- Repro
inductive T.F (α : Type u) (τ : Later (Type u)) : Type u where
  | ret : α → T.F α τ
  | step : DLater τ → T.F α τ
def T α := gfix (T.F α)
theorem T.unfold : T α = T.F α (next (fun () => T α)) := sorry
def T.ret (x : α) : T α := sorry
def T.step (tl : Later (T α)) : T α := sorry

instance : Monad T where
  pure := T.ret
  bind {α β} t k :=
    let loop loop' t : T β := match cast T.unfold t with
      | .ret a   => k a
      | .step tl => T.step (ap loop' (cast DLater.next_eq.symm tl))
    gfix loop t

Expected behavior: No error.

Actual behavior: An error in the instance : Monad T where line:

fields missing: 'map', 'mapConst', 'seq', 'seqLeft'

Now extract the RHS of bind into a separate definition:

noncomputable def T.bind {α β} (t : T α) (k : α → T β) : T β := 
  let loop loop' t : T β := match cast T.unfold t with
    | .ret a   => k a
    | .step tl => T.step (ap loop' (cast DLater.next_eq.symm tl))
  gfix loop t
noncomputable instance : Monad T where
  pure := T.ret
  bind := T.bind

No error, as expected. (noncomputable is needed because I omitted several definitions in the reproducer.)

Versions

4.10.0-rc2
Windows + 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.

[jthulhu]

This is a duplicate of #3146, and there is a pending PR that fixes it: #3152.