c.someRight : Option Nat
evalWithMVar.lean:13:6-13:21: error: don't know how to synthesize implicit argument `α`
  @Sum.someRight ?m Nat c
context:
⊢ Type ?u
evalWithMVar.lean:13:20-13:21: error: don't know how to synthesize implicit argument `α`
  @c ?m
context:
⊢ Type ?u
c.someRight : Option Nat
c.someRight : Option Nat