Improve printing of reverse coercions

When a a term [x] is elaborated into [x'] through a reverse coercion,
return the term [rev_coerce x' x] that is convertible to [x'] but
printed [x], thanks to the coercion [rev_coerce]. Previously, the
returned term was directly [x'].

pretyping/coercion.ml

@@ -621,6 +621,13 @@ let lookup_reversible_path_to_common_point env sigma ~src_expected ~src_inferred
   in
     aux r
 
+let add_reverse_coercion env sigma v'_ty v_ty v' v =
+  match Coqlib.lib_ref_opt "core.coercion.reverse_coercion" with
+  | None -> sigma, v'
+  | Some reverse_coercion ->
+     let sigma, reverse_coercion = Evd.fresh_global env sigma reverse_coercion in
+     Typing.checked_appvect env sigma reverse_coercion [| v'_ty; v_ty; v'; v |]
+
 let inh_coerce_to_fail ?(use_coercions=true) flags env sigma rigidonly v v_ty target_type =
   if not use_coercions || (rigidonly && not (Heads.is_rigid env sigma target_type && Heads.is_rigid env sigma v_ty))
   then
@@ -643,7 +650,8 @@ let inh_coerce_to_fail ?(use_coercions=true) flags env sigma rigidonly v v_ty ta
           let sigma = unify_leq_delay ~flags env sigma direct_v rev_x in
           (try let _ = Evarutil.head_evar sigma (whd_evar sigma x) in raise Not_found
            with NoHeadEvar -> ());  (* fail if x is stil an unresolved evar *)
-          sigma, x, target_type, ReplaceCoe x
+          let sigma, rev_x = add_reverse_coercion env sigma target_type v_ty x v in
+          sigma, rev_x, target_type, ReplaceCoe rev_x
       in
       unify_leq_delay ~flags env sigma v'_ty target_type, v', trace
     with (Evarconv.UnableToUnify _ | Not_found) as exn ->

test-suite/output/bug_16224.out

@@ -6,6 +6,7 @@ Beware that the default locality for '::' is #[export], as opposed to
 #[global] for ':>' currently. Add an explicit #[global] attribute to the
 field if you need to keep the current behavior. For example: "Class foo := {
 #[global] field :: bar }." [future-coercion-class-field,records]
+[reverse_coercion] : ReverseCoercionSource >-> ReverseCoercionTarget
 [rc] : Rc >-> A (reversible)
 [ric] : Ric >-> A (reversible)
 ric : Ric -> A

test-suite/output/relaxed_ambiguous_paths.out

@@ -18,6 +18,7 @@ New coercion path [h1; f3] : B >-> C' is ambiguous with existing
 [f2; h2] : B >-> C'
 [h2] : B' >-> C'
 [f3] : C >-> C'
+[reverse_coercion] : ReverseCoercionSource >-> ReverseCoercionTarget
 File "./output/relaxed_ambiguous_paths.v", line 33, characters 0-28:
 Warning:
 New coercion path [ab; bc] : A >-> C is ambiguous with existing 
@@ -28,6 +29,7 @@ New coercion path [ab; bc] : A >-> C is ambiguous with existing
 [bc] : B >-> C
 [bc; cd] : B >-> D
 [cd] : C >-> D
+[reverse_coercion] : ReverseCoercionSource >-> ReverseCoercionTarget
 File "./output/relaxed_ambiguous_paths.v", line 50, characters 0-28:
 Warning:
 New coercion path [ab; bc] : A >-> C is ambiguous with existing 
@@ -41,12 +43,15 @@ New coercion path [ab; ba] : A >-> A is not definitionally an identity function.
 [ac] : A >-> C
 [ba] : B >-> A
 [bc] : B >-> C
+[reverse_coercion] : ReverseCoercionSource >-> ReverseCoercionTarget
+[reverse_coercion] : ReverseCoercionSource >-> ReverseCoercionTarget
 [B_A] : B >-> A
 [C_A] : C >-> A
 [D_A] : D >-> A
 [D_B] : D >-> B (reversible)
 [D_C] : D >-> C (reversible)
 [A'_A] : A' >-> A (reversible)
+[reverse_coercion] : ReverseCoercionSource >-> ReverseCoercionTarget
 [B_A'; A'_A] : B >-> A
 [B_A'] : B >-> A'
 [C_A'; A'_A] : C >-> A
@@ -59,6 +64,7 @@ File "./output/relaxed_ambiguous_paths.v", line 147, characters 0-86:
 Warning:
 New coercion path [D_C; C_A'] : D >-> A' is ambiguous with existing 
 [D_B; B_A'] : D >-> A'. [ambiguous-paths,typechecker]
+[reverse_coercion] : ReverseCoercionSource >-> ReverseCoercionTarget
 [A'_A] : A' >-> A
 [B_A'; A'_A] : B >-> A
 [B_A'] : B >-> A'

test-suite/output/reverse_coercions.out

@@ -0,0 +1,6 @@
+nat : S
+     : S
+reverse_coercion S_nat nat : S
+     : S
+@reverse_coercion S Set S_nat nat : S
+     : S

test-suite/output/reverse_coercions.v

@@ -0,0 +1,16 @@
+Structure S := {
+  ssort :> Type;
+  sstuff : ssort;
+}.
+
+Canonical Structure S_nat := {| ssort := nat; sstuff := 0; |}.
+
+Check nat : S.
+
+Set Printing Coercions.
+
+Check nat : S.
+
+Set Printing All.
+
+Check nat : S.

theories/Init/Prelude.v

@@ -54,3 +54,14 @@ Export Byte.ByteSyntaxNotations.
 
 (* Default substrings not considered by queries like Search *)
 Add Search Blacklist "_subproof" "_subterm" "Private_".
+
+(* Dummy coercion used by the elaborator to leave a trace in its
+   result. When [x] is (reversible) coerced to [x'], the result
+   [reverse_coercion x' x], convertible to [x'] will still be displayed [x]
+   thanks to the reverse_coercion coercion. *)
+#[universes(polymorphic=yes)] Definition ReverseCoercionSource (T : Type) := T.
+#[universes(polymorphic=yes)] Definition ReverseCoercionTarget (T : Type) := T.
+#[nonuniform, reversible=no, universes(polymorphic=yes)]
+Coercion reverse_coercion {T' T} (x' : T') (x : ReverseCoercionSource T)
+  : ReverseCoercionTarget T' := x'.
+Register reverse_coercion as core.coercion.reverse_coercion.