Why does my refactor break State Monad in FPFL?

Stream: new members

[Michael Fishman]

I'm working through Functional Programming for Lean.

I'm trying to rewrite the implementation of Monad for State more explicitly, in order to better understand it. One of my rewrite steps breaks the definition, and I cannot understand why.

Here's the original definition:

def State (σ : Type) (α : Type) : Type :=
  σ → (σ × α)

instance : Monad (State σ) where
  pure x := fun s => (s, x)
  bind first next :=
    fun s =>
      let (s', x) := first s
      next x s'

Here is a rewritten, still working, implementation:

instance : Monad (State σ) where
  pure {α : Type} (value : α)  := fun context_applied => (context_applied, value)
  bind {α β : Type } (state_og : State σ α) (value_transfomer : α → State σ β) :=
    (
      fun context_input => (
        let applied_state := (state_og context_input)
        let (context_applied, value_applied) := applied_state
        (value_transfomer value_applied) context_applied
      )
    )

If I split the final line in two as follows, I get an error:

instance : Monad (State σ) where
  pure {α : Type} (value : α)  := fun context_applied => (context_applied, value)
  bind {α β : Type } (state_og : State σ α) (value_transfomer : α → State σ β) :=
    (
      fun context_input => (
        let applied_state := (state_og context_input)
        let (context_applied, value_applied) := applied_state
        let value_transformed := (value_transfomer value_applied)
        value_transformed context_applied
      )
    )

The error is at where and says fields missing: 'map', 'mapConst', 'seq', 'seqLeft'

Why does this happen?

I'm assuming the earlier versions are relying on some convenience funtionality that is breaking in my final version.