| 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 |