Background

As the Lean Reference's Instances for nested types example shows, in a function that implements a type class method for a certain type, one can already use the type class instance for that type itself (i.e., recursively) by making the function partial and defining a local instance inside the function (here called _):

inductive NatRoseTree where
  | node (val : Nat) (children : Array NatRoseTree)

partial def NatRoseTree.beq : (tree1 tree2 : NatRoseTree) → Bool
  | .node val1 children1, .node val2 children2 =>
    let _ : BEq NatRoseTree := ⟨NatRoseTree.beq⟩
    val1 == val2 &&
    children1 == children2

-- [subsequent global instance definition is omitted in the example,
--  but it's just BEq NatRoseTree := ⟨NatRoseTree.beq⟩ again]

Lean's instance search will find the _ instance and use it to make sense of the == expressions inside the function, even though no global BEq NatRoseTree instance has been defined yet.

The problem

I would like to apply the same technique to ForIn / ForM, so that I can iterate over values of a type with for ... in ... do inside that type's own ForM.forM definition.

For example, here is a simple "countdown" type with (pointless) recursive usage of for over a value of its own type in its forM implementation:

structure Countdown where
  val: Nat

partial def Countdown.forM
  [Monad m] (c : Countdown) (action : Nat → m PUnit) : m PUnit
:= do match c with
  | ⟨0⟩ => action 0
  | ⟨n⟩ =>

      -- ...
      -- This is where you would probably need to add
      -- a local `ForIn` instance to make `for` work
      -- ...

      action n
      for i in (⟨n-1⟩ : Countdown) do
        action i

instance : ForM m Countdown Nat := ⟨Countdown.forM⟩
instance : ForIn m Countdown Nat := ⟨ForM.forIn⟩

def main : IO Unit :=
  for x in (⟨3⟩ : Countdown) do
    IO.println s!"count: {x}"

What do I need to put at the indicated placeholder (and, potentially, change elsewhere in the code) to make this work?

Obviously, simply calling the forM function itself recursively instead of using an actual for loop doesn't count.

My attempts so far

I first tried naively applying the technique from the Lean Reference by creating local ForM and ForIn instances given Countdown.forM's own monad m:

      let _ := (⟨Countdown.forM⟩ : ForM m Countdown Nat)
      let _ := (⟨ForM.forIn⟩ : ForIn m Countdown Nat)

But that doesn't compile at all:

error: Main.lean:10:17: failed to synthesize
  ForM (StateT β✝ (ExceptT β✝ m)) Countdown Nat

So I tried to let the compiler infer the correct monads automatically instead by making them implicit:

      let {m'} := (⟨Countdown.forM⟩ : ForM m' Countdown Nat)
      let {m'} := (⟨ForM.forIn⟩ : ForIn m' Countdown Nat)

This then compiles just fine, but doesn't appear to actually run the for loop, only the preceding action (output is just count: 3). Upon closer inspection, it turns out that it segfaults, likely due to a stack overflow.