feat: make Option.decidableEqNone coherent with Option.instDecidableEq (#9302)

This PR modifies `Option.instDecidableEq` and `Option.decidableEqNone`
so that the latter can be made into a global instance without causing
diamonds. It also adds `Option.decidabeNoneEq`.

See
[Zulip](https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Option.2EdecidableEqNone/near/527226250).

---------

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Rob Simmons <rob@lean-fro.org>

src/Init/Data/Option/Basic.lean

@@ -15,7 +15,39 @@ public section
 
 namespace Option
 
-deriving instance DecidableEq for Option
+/- We write the instance manually so that it is coherent with `decidableEqNone` and
+`decidableNoneEq`.
+
+TODO: adjust the `deriving instance DecidableEq` handler to generate something coherent. -/
+instance instDecidableEq {α} [DecidableEq α] : DecidableEq (Option α) := fun a b =>
+  match a with
+  | none => match b with
+    | none => .isTrue rfl
+    | some _ => .isFalse Option.noConfusion
+  | some a => match b with
+    | none => .isFalse Option.noConfusion
+    | some b => decidable_of_decidable_of_eq (Option.some.injEq a b).symm
+
+/--
+Equality with `none` is decidable even if the wrapped type does not have decidable equality.
+-/
+instance decidableEqNone (o : Option α) : Decidable (o = none) :=
+  /- We use a `match` instead of transferring from `isNone_iff_eq_none` for
+    compatibility with the `DecidableEq` instance. -/
+  match o with
+  | none => .isTrue rfl
+  | some _ => .isFalse Option.noConfusion
+
+/--
+Equality with `none` is decidable even if the wrapped type does not have decidable equality.
+-/
+instance decidableNoneEq (o : Option α) : Decidable (none = o) :=
+  /- We use a `match` instead of transferring from `isNone_iff_eq_none` for
+    compatibility with the `DecidableEq` instance. -/
+  match o with
+  | none => .isTrue rfl
+  | some _ => .isFalse Option.noConfusion
+
 deriving instance BEq for Option
 
 @[simp, grind =] theorem getD_none : getD none a = a := rfl

src/Init/Data/Option/Instances.lean

@@ -35,17 +35,6 @@ instance [DecidableEq α] (j : α) (o : Option α) : Decidable (j ∈ o) :=
 
 theorem some_inj {a b : α} : some a = some b ↔ a = b := by simp; rfl
 
-/--
-Equality with `none` is decidable even if the wrapped type does not have decidable equality.
-
-This is not an instance because it is not definitionally equal to the standard instance of
-`DecidableEq (Option α)`, which can cause problems. It can be locally bound if needed.
-
-Try to use the Boolean comparisons `Option.isNone` or `Option.isSome` instead.
--/
-@[inline] def decidableEqNone {o : Option α} : Decidable (o = none) :=
-  decidable_of_decidable_of_iff isNone_iff_eq_none
-
 instance decidableForallMem {p : α → Prop} [DecidablePred p] :
     ∀ o : Option α, Decidable (∀ a, a ∈ o → p a)
   | none => isTrue nofun

tests/lean/run/optionDecEq.lean

@@ -0,0 +1,11 @@
+variable {α : Type u} [DecidableEq α]
+
+-- test for instance diamonds
+
+example (x : Option α) :
+    Option.instDecidableEq x none = Option.decidableEqNone x := by
+  with_reducible_and_instances rfl
+
+example (x : Option α) :
+    Option.instDecidableEq none x = Option.decidableNoneEq x := by
+  with_reducible_and_instances rfl