Pattern matching in "do" requires a MonadFail context, which we don't have in
pure code. Instead, we'll use "case-of" to bind the part of the state that
we're interested in.