Messing up Option's Coe

Stream: lean4

[Marcus Rossel]

I have a case where the coercion X to Option X stops working after adding another Coe instance.
This works just as expected:

inductive A
  | yes
  | no

def A.yes? : A → Option Unit
  | yes => Unit.unit -- Coerces to `Option Unit`
  | no => none

But adding this Numbered type with a coercion from Numbered X to X messes up the Option-coercion in A.yes?:

structure Numbered (α) where
  num : Nat
  obj : α

instance : Coe (Numbered α) α := ⟨Numbered.obj⟩

inductive A
  | yes
  | no

def A.yes? : A → Option Unit
  | yes => Unit.unit -- Error message below
  | no => none

/-
type mismatch
  ()
has type
  Unit : Type
but is expected to have type
  Option Unit : Type
-/

Is there a way to fix this?