Fix #11140: Bidirectionality hints perform (surprising?) simplification

We typecheck arguments like previously, using bidirectionality hints,
but ultimately replace them with user-provided arguments on which we
replay coercion traces.

This is a fix which should be easy to backport, but there are two
directions of future work:
- Coercion traces for `Program` coercions (in these cases, we currently
use the inferred arguments)
- Separate the Coercion API in two phases: inference and application of
coercions. It will make the approach taken here cleaner, and probably
make it easier to interleave typing steps with coercion inference.

Co-Authored-By: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>

1 files changed, 9 insertions, 3 deletions

diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli
index fe93a26f4f..b92f3709cc 100644
--- a/pretyping/coercion.mli
+++ b/pretyping/coercion.mli
@@ -16,13 +16,19 @@ open Glob_term
 
 (** {6 Coercions. } *)
 
+type coercion_trace
+
+val empty_coercion_trace : coercion_trace
+
+val reapply_coercions : evar_map -> coercion_trace -> EConstr.t -> EConstr.t
+
 (** [inh_app_fun resolve_tc env isevars j] coerces [j] to a function; i.e. it
     inserts a coercion into [j], if needed, in such a way it gets as
     type a product; it returns [j] if no coercion is applicable.
     resolve_tc=false disables resolving type classes (as the last
     resort before failing) *)
 val inh_app_fun : program_mode:bool -> bool ->
-  env -> evar_map -> unsafe_judgment -> evar_map * unsafe_judgment
+  env -> evar_map -> unsafe_judgment -> evar_map * unsafe_judgment * coercion_trace
 
 (** [inh_coerce_to_sort env isevars j] coerces [j] to a type; i.e. it
     inserts a coercion into [j], if needed, in such a way it gets as
@@ -48,11 +54,11 @@ val inh_coerce_to_prod : ?loc:Loc.t -> program_mode:bool ->
 
 val inh_conv_coerce_to : ?loc:Loc.t -> program_mode:bool -> bool ->
   env -> evar_map -> ?flags:Evarconv.unify_flags ->
-  unsafe_judgment -> types -> evar_map * unsafe_judgment
+  unsafe_judgment -> types -> evar_map * unsafe_judgment * coercion_trace option
 
 val inh_conv_coerce_rigid_to : ?loc:Loc.t -> program_mode:bool ->bool ->
   env -> evar_map -> ?flags:Evarconv.unify_flags ->
-  unsafe_judgment -> types -> evar_map * unsafe_judgment
+  unsafe_judgment -> types -> evar_map * unsafe_judgment * coercion_trace option
 
 (** [inh_pattern_coerce_to loc env isevars pat ind1 ind2] coerces the Cases
     pattern [pat] typed in [ind1] into a pattern typed in [ind2];