Fix conversion oracle bug, add test case.

Before `EvalProjectionRef` was added, any combination of proj and const would
hit the `EvalConstRef, EvalConstRef` case and thus produce `l2r`.

kernel/conv_oracle.ml

@@ -119,9 +119,10 @@ let dep_order l2r k1 k2 =
   | EvalVarRef _, EvalVarRef _ -> l2r
   | EvalVarRef _, (EvalConstRef _ | EvalProjectionRef _) -> true
   | EvalConstRef _, EvalVarRef _ -> false
-  | EvalConstRef _, EvalProjectionRef _ -> true
+  | EvalConstRef _, EvalProjectionRef _ -> l2r
   | EvalConstRef _, EvalConstRef _ -> l2r
-  | EvalProjectionRef _, (EvalVarRef _ | EvalConstRef _) -> false
+  | EvalProjectionRef _, EvalVarRef _ -> false
+  | EvalProjectionRef _, EvalConstRef _ -> l2r
   | EvalProjectionRef _, EvalProjectionRef _ -> l2r
 
 (* Unfold the first constant only if it is "more transparent" than the

test-suite/success/primproj_tactic_unif.v

@@ -1,4 +1,4 @@
-Section S.
+Module S.
   #[local] Set Printing Unfolded Projection As Match.
   #[projections(primitive=yes)]
   Record state (u : unit) :=
@@ -67,3 +67,42 @@ Section S.
   Qed.
 
 End S.
+
+Module I.
+  #[local] Set Printing Unfolded Projection As Match.
+  Record cmra := Cmra { cmra_car : Type }.
+  Record ucmra := { ucmra_car : Type }.
+
+  #[projections(primitive=yes)]
+  Record ofe (n : nat) := Ofe { ofe_car : Type }.
+
+  Axiom n : nat.
+
+  Definition ucmra_ofeO := fun A : ucmra => @Ofe n (ucmra_car A).
+
+  (* Canonical Structure cmra_ofeO := fun A : cmra => @Ofe n (cmra_car A). *)
+
+  Canonical Structure ucmra_cmraR :=
+    fun A : ucmra =>
+      Cmra (ucmra_car A).
+
+  Axiom A : ucmra.
+  Axiom bla : forall (A : cmra), cmra_car A.
+  Goal ofe_car n (ucmra_ofeO A).
+    Set Debug "tactic-unification,unification".
+    Fail autoapply (@bla) with typeclass_instances.
+
+
+  Goal forall A : ucmra,
+    exists C,
+      cmra_car C =
+        ofe_car n (ucmra_ofeO A).
+  Proof.
+    intros. eexists _.
+    unfold ucmra_ofeO.
+    Set Debug "unification".
+    Succeed refine (eq_refl).
+    Set Debug "tactic-unification".
+    Fail apply (eq_refl).
+
+End I.