Failing ssreflect rewrite (that works with Coq's rewrite)

[robbertkrebbers]

Description of the problem

This problem came up in std++, see https://gitlab.mpi-sws.org/iris/stdpp/-/issues/168 Below I include a minimized and self-contained version (that does not depend on std++):

Require Import ssreflect Utf8 PeanoNat.
Global Open Scope general_if_scope.

Class Decision (P : Prop) := decide : {P} + {¬P}.
Global Hint Mode Decision ! : typeclass_instances.
Global Arguments decide _ {_}.

Global Instance nat_eq_dec : ∀ n1 n2, Decision (n1 = n2) := Nat.eq_dec.

Lemma decide_True {A} {P} `{Decision P} (x y : A) :
  P -> (if decide P then x else y) = x.
Proof. destruct (decide P); tauto. Qed.

Lemma bar n : (if decide (n = 0) then 0 else 0) = 0.
Proof.
  Succeed rewrite decide_True. (* just works *)
Abort.

Lemma bar : (if decide (0 = 0) then 0 else 0) = 0.
Proof. (* Now with two times 0 instead of a variable n *)
  Succeed rewrite ->decide_True.
  Fail rewrite decide_True.
  (* Fails with: The LHS of (@decide_True _ _ _)
    match @decide _ _ return _ with
    | left _ => _
    | right _ => _
    end

  The goal is:

    @eq nat
      match @decide (@eq nat O O) (nat_eq_dec O O) return nat with
      | left _ => O
      | right _ => O
      end O

  So it _does_ contain the LHS of the lemma. *)

Coq Version

$ coqtop -v
The Coq Proof Assistant, version 8.16.0
compiled with OCaml 4.13.1

[robbertkrebbers]

Maybe this has something to do with ssreflect normalizing the goal too eagerly? (if decide (0 = 0) then 0 else 0) is convertible to 0 after all.

If I admit the Decision instance so the goal no longer computes:

Global Instance nat_eq_dec : ∀ n1 n2 : nat, Decision (n1 = n2). Admitted.

Then ssreflect's rewrite does work.

[SkySkimmer]

Looks like there's a mismatch between old and new unification behaviours:

  (* unify: old unification *)
  let l := open_constr:(if decide _ then _ else _) in
  unify l (if @decide (0 = 0) (nat_eq_dec _ _) then 0 else 0).

  (* evarconv unification *)
  Fail Check eq_refl : (if decide _ then _ else _) =
                         (if @decide (0 = 0) (nat_eq_dec _ _) then 0 else 0).

[Janno]

Data point of questionable use: unicoq agrees with old unification.

  From Unicoq Require Import Unicoq.
  Set Use Unicoq.

  let l := open_constr:(if decide _ then _ else _) in
  munify l (if @decide (0 = 0) (nat_eq_dec _ _) then 0 else 0).
  Check eq_refl : (if decide _ then _ else _) =
                         (if @decide (0 = 0) (nat_eq_dec _ _) then 0 else 0).