type coe failed when use Monad and do block

Stream: lean4

[ZHAO Jiecheng]

do block is not able to coe the type when both α γ in Except α γ are different (but I feel should be able to coe) .

inductive ExitError where
| error1
| error2

inductive ExitReason where
| error : ExitError → ExitReason
| ok1 : ExitReason
| ok2 : ExitReason

instance : Coe ExitError ExitReason where
  coe a := ExitReason.error a

instance [Coe α β ]: Coe (Except α γ) (Except β γ) where
  coe a :=
    match a with
    | .ok n => .ok n
    | .error e => .error e

def f1 (a : Nat) : Except ExitError Nat := sorry
def f2 (a : Nat) : Except ExitError Nat := sorry

def f3 (a b : Nat) : Except ExitError Int := do
  let aa ← f1 a
  let bb ← f2 b
  pure (aa + bb)

def f4 (a b : Nat) : Except ExitReason Nat := do
  let aa ← f1 a
  let bb ← f2 b
  pure (aa + bb)

def f5 (a b : Nat) : Except ExitReason Int := do
  let aa ← f1 a
  let bb ← f2 b -- Error: type mismatch, How can I do here.
  pure (aa + bb)