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

Reviewed-by: SkySkimmer
Ack-by: gares
Reviewed-by: mattam82

13 files changed, 236 insertions, 122 deletions

diff --git a/doc/changelog/01-kernel/11361-fix-11360-discharge-template-param-var.rst b/doc/changelog/01-kernel/11361-fix-11360-discharge-template-param-var.rst
new file mode 100644
index 0000000000..8c84648aa7
--- /dev/null
+++ b/doc/changelog/01-kernel/11361-fix-11360-discharge-template-param-var.rst
@@ -0,0 +1,4 @@
+- **Fixed:** `#11360 <https://github.com/issues/11360>`_
+  Broken section closing when a template polymorphic inductive type depends on
+  a section variable through its parameters (`#11361
+  <https://github.com/coq/coq/pull/11361>`_, by Gaëtan Gilbert).
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 78428be18f..8d59e64cdb 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -2547,3 +2547,8 @@ the context to help inferring the types of the remaining arguments.
 
       Arguments ex_intro _ _ & _ _.
       Check (ex_intro _ true _ : exists n : nat, n > 0).
+
+Coq will attempt to produce a term which uses the arguments you
+provided, but in some cases involving Program mode the arguments after
+the bidirectionality starts may be replaced by convertible but
+syntactically different terms.
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index 368724f9d2..70dadedd35 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -327,11 +327,8 @@ function on type :g:`A`). The keyword :g:`fun` can be followed by several
 binders as given in Section :ref:`binders`. Functions over
 several variables are equivalent to an iteration of one-variable
 functions. For instance the expression
-“fun :token:`ident`\ :math:`_{1}` … :token:`ident`\ :math:`_{n}` 
-: :token:`type` => :token:`term`”
-denotes the same function as “ fun :token:`ident`\
-:math:`_{1}` : :token:`type` => … 
-fun :token:`ident`\ :math:`_{n}` : :token:`type` => :token:`term`”. If
+:n:`fun {+ @ident__i } : @type => @term`
+denotes the same function as :n:`{+ fun @ident__i : @type => } @term`. If
 a let-binder occurs in
 the list of binders, it is expanded to a let-in definition (see
 Section :ref:`let-in`).
@@ -362,15 +359,14 @@ the propositional implication and function types.
 Applications
 ------------
 
-The expression :token:`term`\ :math:`_0` :token:`term`\ :math:`_1` denotes the
-application of :token:`term`\ :math:`_0` to :token:`term`\ :math:`_1`.
+The expression :n:`@term__fun @term` denotes the application of
+:n:`@term__fun` (which is expected to have a function type) to
+:token:`term`.
 
-The expression :token:`term`\ :math:`_0` :token:`term`\ :math:`_1` ...
-:token:`term`\ :math:`_n` denotes the application of the term
-:token:`term`\ :math:`_0` to the arguments :token:`term`\ :math:`_1` ... then
-:token:`term`\ :math:`_n`. It is equivalent to ( … ( :token:`term`\ :math:`_0`
-:token:`term`\ :math:`_1` ) … ) :token:`term`\ :math:`_n` : associativity is to the
-left.
+The expression :n:`@term__fun {+ @term__i }` denotes the application
+of the term :n:`@term__fun` to the arguments :n:`@term__i`.  It is
+equivalent to :n:`( … ( @term__fun @term__1 ) … ) @term__n`:
+associativity is to the left.
 
 The notation :n:`(@ident := @term)` for arguments is used for making
 explicit the value of implicit arguments (see
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 750ac86908..ab915e2b8d 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -379,17 +379,25 @@ let check_positivity ~chkpos kn names env_ar_par paramsctxt finite inds =
 (************************************************************************)
 (* Build the inductive packet *)
 
-let repair_arity indices = function
-  | RegularArity ar -> ar.mind_user_arity
-  | TemplateArity ar -> mkArity (indices,Sorts.sort_of_univ ar.template_level)
+let fold_arity f acc params arity indices = match arity with
+  | RegularArity ar -> f acc ar.mind_user_arity
+  | TemplateArity _ ->
+    let fold_ctx acc ctx =
+      List.fold_left (fun acc d ->
+          Context.Rel.Declaration.fold_constr (fun c acc -> f acc c) d acc)
+        acc
+        ctx
+    in
+    fold_ctx (fold_ctx acc params) indices
 
-let fold_inductive_blocks f =
+let fold_inductive_blocks f acc params inds =
   Array.fold_left (fun acc ((arity,lc),(indices,_),_) ->
-    f (Array.fold_left f acc lc) (repair_arity indices arity))
+      fold_arity f (Array.fold_left f acc lc) params arity indices)
+    acc inds
 
-let used_section_variables env inds =
+let used_section_variables env params inds =
   let fold l c = Id.Set.union (Environ.global_vars_set env c) l in
-  let ids = fold_inductive_blocks fold Id.Set.empty inds in
+  let ids = fold_inductive_blocks fold Id.Set.empty params inds in
   keep_hyps env ids
 
 let rel_vect n m = Array.init m (fun i -> mkRel(n+m-i))
@@ -461,7 +469,7 @@ let compute_projections (kn, i as ind) mib =
 let build_inductive env names prv univs variance paramsctxt kn isrecord isfinite inds nmr recargs =
   let ntypes = Array.length inds in
   (* Compute the set of used section variables *)
-  let hyps = used_section_variables env inds in
+  let hyps = used_section_variables env paramsctxt inds in
   let nparamargs = Context.Rel.nhyps paramsctxt in
   (* Check one inductive *)
   let build_one_packet (id,cnames) ((arity,lc),(indices,splayed_lc),kelim) recarg =
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index aa6ec1c941..cbd04a76ad 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -436,7 +436,7 @@ let adjust_tomatch_to_pattern ~program_mode sigma pb ((current,typ),deps,dep) =
                 | exception Evarconv.UnableToUnify _ -> sigma, current
                 | sigma -> sigma, current
               else
-                let sigma, j = Coercion.inh_conv_coerce_to ?loc ~program_mode true !!(pb.env) sigma (make_judge current typ) indt in
+                let sigma, j, _trace = Coercion.inh_conv_coerce_to ?loc ~program_mode true !!(pb.env) sigma (make_judge current typ) indt in
                 sigma, j.uj_val
             in
             sigma, (current, try_find_ind !!(pb.env) sigma indt names))
@@ -1955,8 +1955,12 @@ let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign =
 
 let inh_conv_coerce_to_tycon ?loc ~program_mode env sigma j tycon =
   match tycon with
-    | Some p -> Coercion.inh_conv_coerce_to ?loc ~program_mode true env sigma
-                ~flags:(default_flags_of TransparentState.full) j p
+    | Some p ->
+      let (evd,v,_trace) =
+        Coercion.inh_conv_coerce_to ?loc ~program_mode true env sigma
+          ~flags:(default_flags_of TransparentState.full) j p
+      in
+      (evd,v)
     | None -> sigma, j
 
 (* We put the tycon inside the arity signature, possibly discovering dependencies. *)
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index c980d204ca..3c7f9a8f00 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -136,20 +136,6 @@ let lift_args n sign =
   in
     liftrec (List.length sign) sign
 
-let mu env evdref t =
-  let rec aux v =
-    let v' = hnf env !evdref v in
-      match disc_subset !evdref v' with
-      | Some (u, p) ->
-        let f, ct = aux u in
-        let p = hnf_nodelta env !evdref p in
-          (Some (fun x ->
-                   app_opt env evdref
-                     f (papp evdref sig_proj1 [| u; p; x |])),
-           ct)
-      | None -> (None, v)
-  in aux t
-
 let coerce ?loc env evdref (x : EConstr.constr) (y : EConstr.constr)
     : (EConstr.constr -> EConstr.constr) option
     =
@@ -367,36 +353,97 @@ let saturate_evd env evd =
   Typeclasses.resolve_typeclasses
     ~filter:Typeclasses.no_goals ~split:true ~fail:false env evd
 
+type coercion_trace =
+  | IdCoe
+  | PrimProjCoe of {
+      proj : Projection.Repr.t;
+      args : econstr list;
+      previous : coercion_trace;
+    }
+  | Coe of {
+      head : econstr;
+      args : econstr list;
+      previous : coercion_trace;
+    }
+  | ProdCoe of { na : Name.t binder_annot; ty : econstr; dom : coercion_trace; body : coercion_trace }
+
+let empty_coercion_trace = IdCoe
+
+(* similar to iterated apply_coercion_args *)
+let rec reapply_coercions sigma trace c = match trace with
+  | IdCoe -> c
+  | PrimProjCoe { proj; args; previous } ->
+    let c = reapply_coercions sigma previous c in
+    let args = args@[c] in
+    let head, args = match args with [] -> assert false | hd :: tl -> hd, tl in
+    applist (mkProj (Projection.make proj false, head), args)
+  | Coe {head; args; previous} ->
+    let c = reapply_coercions sigma previous c in
+    let args = args@[c] in
+    applist (head, args)
+  | ProdCoe { na; ty; dom; body } ->
+    let x = reapply_coercions sigma dom (mkRel 1) in
+    let c = beta_applist sigma (lift 1 c, [x]) in
+    let c = reapply_coercions sigma body c in
+    mkLambda (na, ty, c)
+
 (* Apply coercion path from p to hj; raise NoCoercion if not applicable *)
 let apply_coercion env sigma p hj typ_cl =
-  let j,t,evd =
+  let j,t,trace,evd =
     List.fold_left
-      (fun (ja,typ_cl,sigma) i ->
+      (fun (ja,typ_cl,trace,sigma) i ->
          let isid = i.coe_is_identity in
          let isproj = i.coe_is_projection in
          let sigma, c = new_global sigma i.coe_value in
          let typ = Retyping.get_type_of env sigma c in
          let fv = make_judge c typ in
-         let argl = (class_args_of env sigma typ_cl)@[ja.uj_val] in
-         let sigma, jres =
-           apply_coercion_args env sigma true isproj argl fv
+         let argl = class_args_of env sigma typ_cl in
+         let trace =
+           if isid then trace
+           else match isproj with
+           | None -> Coe {head=fv.uj_val;args=argl;previous=trace}
+           | Some proj ->
+             let args = List.skipn (Projection.Repr.npars proj) argl in
+             PrimProjCoe {proj; args; previous=trace }
          in
-         (if isid then
+         let argl = argl@[ja.uj_val] in
+         let sigma, jres = apply_coercion_args env sigma true isproj argl fv in
+         let jres =
+         if isid then
             { uj_val = ja.uj_val; uj_type = jres.uj_type }
           else
-            jres),
-         jres.uj_type,sigma)
-      (hj,typ_cl,sigma) p
-  in evd, j
+            jres
+         in
+         jres, jres.uj_type, trace, sigma)
+      (hj,typ_cl,IdCoe,sigma) p
+  in evd, j, trace
+
+let mu env evdref t =
+  let rec aux v =
+    let v' = hnf env !evdref v in
+      match disc_subset !evdref v' with
+      | Some (u, p) ->
+        let f, ct, trace = aux u in
+        let p = hnf_nodelta env !evdref p in
+        let p1 = delayed_force sig_proj1 in
+        let evd, p1 = Evarutil.new_global !evdref p1 in
+        evdref := evd;
+          (Some (fun x ->
+                   app_opt env evdref
+                     f (mkApp (p1, [| u; p; x |]))),
+           ct,
+           Coe {head=p1; args=[u;p]; previous=trace})
+      | None -> (None, v, IdCoe)
+  in aux t
 
 (* Try to coerce to a funclass; raise NoCoercion if not possible *)
 let inh_app_fun_core ~program_mode env evd j =
   let t = whd_all env evd j.uj_type in
     match EConstr.kind evd t with
-    | Prod _ -> (evd,j)
+    | Prod _ -> (evd,j,IdCoe)
     | Evar ev ->
         let (evd',t) = Evardefine.define_evar_as_product env evd ev in
-          (evd',{ uj_val = j.uj_val; uj_type = t })
+          (evd',{ uj_val = j.uj_val; uj_type = t },IdCoe)
     | _ ->
         try let t,p =
           lookup_path_to_fun_from env evd j.uj_type in
@@ -405,11 +452,11 @@ let inh_app_fun_core ~program_mode env evd j =
          if program_mode then
            try
              let evdref = ref evd in
-             let coercef, t = mu env evdref t in
+             let coercef, t, trace = mu env evdref t in
              let res = { uj_val = app_opt env evdref coercef j.uj_val; uj_type = t } in
-             (!evdref, res)
+             (!evdref, res, trace)
            with NoSubtacCoercion | NoCoercion ->
-             (evd,j)
+             (evd,j,IdCoe)
          else raise NoCoercion
 
 (* Try to coerce to a funclass; returns [j] if no coercion is applicable *)
@@ -417,10 +464,10 @@ let inh_app_fun ~program_mode resolve_tc env evd j =
   try inh_app_fun_core ~program_mode env evd j
   with
   | NoCoercion when not resolve_tc
-    || not (get_use_typeclasses_for_conversion ()) -> (evd, j)
+    || not (get_use_typeclasses_for_conversion ()) -> (evd, j, IdCoe)
   | NoCoercion ->
     try inh_app_fun_core ~program_mode env (saturate_evd env evd) j
-    with NoCoercion -> (evd, j)
+    with NoCoercion -> (evd, j, IdCoe)
 
 let type_judgment env sigma j =
   match EConstr.kind sigma (whd_all env sigma j.uj_type) with
@@ -430,7 +477,7 @@ let type_judgment env sigma j =
 let inh_tosort_force ?loc env evd j =
   try
     let t,p = lookup_path_to_sort_from env evd j.uj_type in
-    let evd,j1 = apply_coercion env evd p j t in
+    let evd,j1,_trace = apply_coercion env evd p j t in
     let j2 = Environ.on_judgment_type (whd_evar evd) j1 in
       (evd,type_judgment env evd j2)
   with Not_found | NoCoercion ->
@@ -449,7 +496,7 @@ let inh_coerce_to_sort ?loc env evd j =
 let inh_coerce_to_base ?loc ~program_mode env evd j =
   if program_mode then
     let evdref = ref evd in
-    let ct, typ' = mu env evdref j.uj_type in
+    let ct, typ', trace = mu env evdref j.uj_type in
     let res =
       { uj_val = (app_coercion env evdref ct j.uj_val);
         uj_type = typ' }
@@ -459,7 +506,7 @@ let inh_coerce_to_base ?loc ~program_mode env evd j =
 let inh_coerce_to_prod ?loc ~program_mode env evd t =
   if program_mode then
     let evdref = ref evd in
-    let _, typ' = mu env evdref t in
+    let _, typ', _trace = mu env evdref t in
       !evdref, typ'
   else (evd, t)
 
@@ -468,24 +515,24 @@ let inh_coerce_to_fail flags env evd rigidonly v t c1 =
   then
     raise NoCoercion
   else
-    let evd, v', t' =
+    let evd, v', t', trace =
       try
         let t2,t1,p = lookup_path_between env evd (t,c1) in
-        let evd,j =
+        let evd,j,trace =
           apply_coercion env evd p
             {uj_val = v; uj_type = t} t2
         in
-        evd, j.uj_val, j.uj_type
+        evd, j.uj_val, j.uj_type, trace
       with Not_found -> raise NoCoercion
     in
-    try (unify_leq_delay ~flags env evd t' c1, v')
+    try (unify_leq_delay ~flags env evd t' c1, v', trace)
     with UnableToUnify _ -> raise NoCoercion
 
 let default_flags_of env =
   default_flags_of TransparentState.full
 
 let rec inh_conv_coerce_to_fail ?loc env evd ?(flags=default_flags_of env) rigidonly v t c1 =
-  try (unify_leq_delay ~flags env evd t c1, v)
+  try (unify_leq_delay ~flags env evd t c1, v, IdCoe)
   with UnableToUnify (best_failed_evd,e) ->
     try inh_coerce_to_fail flags env evd rigidonly v t c1
     with NoCoercion ->
@@ -505,24 +552,27 @@ let rec inh_conv_coerce_to_fail ?loc env evd ?(flags=default_flags_of env) rigid
             | na -> na) name in
           let open Context.Rel.Declaration in
           let env1 = push_rel (LocalAssum (name,u1)) env in
-          let (evd', v1) =
+          let (evd', v1, trace1) =
             inh_conv_coerce_to_fail ?loc env1 evd rigidonly
               (mkRel 1) (lift 1 u1) (lift 1 t1) in
           let v2 = beta_applist evd' (lift 1 v,[v1]) in
           let t2 = Retyping.get_type_of env1 evd' v2 in
-          let (evd'',v2') = inh_conv_coerce_to_fail ?loc env1 evd' rigidonly v2 t2 u2 in
-            (evd'', mkLambda (name, u1, v2'))
+          let (evd'',v2',trace2) = inh_conv_coerce_to_fail ?loc env1 evd' rigidonly v2 t2 u2 in
+          let trace = ProdCoe { na=name; ty=u1; dom=trace1; body=trace2 } in
+          (evd'', mkLambda (name, u1, v2'), trace)
       | _ -> raise (NoCoercionNoUnifier (best_failed_evd,e))
 
 (* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *)
 let inh_conv_coerce_to_gen ?loc ~program_mode resolve_tc rigidonly flags env evd cj t =
-  let (evd', val') =
+  let (evd', val', otrace) =
     try
-      inh_conv_coerce_to_fail ?loc env evd ~flags rigidonly cj.uj_val cj.uj_type t
+      let (evd', val', trace) = inh_conv_coerce_to_fail ?loc env evd ~flags rigidonly cj.uj_val cj.uj_type t in
+      (evd', val', Some trace)
     with NoCoercionNoUnifier (best_failed_evd,e) ->
       try
         if program_mode then
-          coerce_itf ?loc env evd cj.uj_val cj.uj_type t
+          let (evd', val') = coerce_itf ?loc env evd cj.uj_val cj.uj_type t in
+          (evd', val', None)
         else raise NoSubtacCoercion
       with
       | NoSubtacCoercion when not resolve_tc || not (get_use_typeclasses_for_conversion ()) ->
@@ -533,11 +583,12 @@ let inh_conv_coerce_to_gen ?loc ~program_mode resolve_tc rigidonly flags env evd
             if evd' == evd then
               error_actual_type ?loc env best_failed_evd cj t e
             else
-              inh_conv_coerce_to_fail ?loc env evd' rigidonly cj.uj_val cj.uj_type t
+              let (evd', val', trace) = inh_conv_coerce_to_fail ?loc env evd' rigidonly cj.uj_val cj.uj_type t in
+              (evd', val', Some trace)
           with NoCoercionNoUnifier (_evd,_error) ->
             error_actual_type ?loc env best_failed_evd cj t e
   in
-  (evd',{ uj_val = val'; uj_type = t })
+  (evd',{ uj_val = val'; uj_type = t },otrace)
 
 let inh_conv_coerce_to ?loc ~program_mode resolve_tc env evd ?(flags=default_flags_of env) =
   inh_conv_coerce_to_gen ?loc ~program_mode resolve_tc false flags env evd
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];
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index bfdb471c46..bf61d44a10 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -361,7 +361,7 @@ let adjust_evar_source sigma na c =
 
 (* coerce to tycon if any *)
 let inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma j = function
-  | None -> sigma, j
+  | None -> sigma, j, Some Coercion.empty_coercion_trace
   | Some t ->
     Coercion.inh_conv_coerce_to ?loc ~program_mode resolve_tc !!env sigma j t
 
@@ -604,16 +604,18 @@ let pretype_instance self ~program_mode ~poly resolve_tc env sigma loc hyps evk
 module Default =
 struct
 
+  let discard_trace (sigma,t,otrace) = sigma, t
+
   let pretype_ref self (ref, u) =
     fun ?loc ~program_mode ~poly resolve_tc tycon env sigma ->
     let sigma, t_ref = pretype_ref ?loc sigma env ref u in
-    inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma t_ref tycon
+    discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma t_ref tycon
 
   let pretype_var self id =
     fun ?loc ~program_mode ~poly resolve_tc tycon env sigma ->
     let pretype tycon env sigma t = eval_pretyper self ~program_mode ~poly resolve_tc tycon env sigma t in
     let sigma, t_id = pretype_id (fun e r t -> pretype tycon e r t) loc env sigma id in
-    inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma t_id tycon
+    discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma t_id tycon
 
   let pretype_evar self (id, inst) ?loc ~program_mode ~poly resolve_tc tycon env sigma =
       (* Ne faudrait-il pas s'assurer que hyps est bien un
@@ -626,7 +628,7 @@ struct
       let sigma, args = pretype_instance self ~program_mode ~poly resolve_tc env sigma loc hyps evk inst in
       let c = mkEvar (evk, args) in
       let j = Retyping.get_judgment_of !!env sigma c in
-      inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma j tycon
+      discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma j tycon
 
   let pretype_patvar self kind ?loc ~program_mode ~poly resolve_tc tycon env sigma =
     let sigma, ty =
@@ -757,12 +759,12 @@ struct
                iraise (e, info));
             make_judge (mkCoFix cofix) ftys.(i)
       in
-      inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma fixj tycon
+      discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma fixj tycon
 
   let pretype_sort self s =
     fun ?loc ~program_mode ~poly resolve_tc tycon env sigma ->
     let sigma, j = pretype_sort ?loc sigma s in
-    inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma j tycon
+    discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma j tycon
 
   let pretype_app self (f, args) =
     fun ?loc ~program_mode ~poly resolve_tc tycon env sigma ->
@@ -771,12 +773,15 @@ struct
     let floc = loc_of_glob_constr f in
     let length = List.length args in
     let nargs_before_bidi =
+      if Option.is_empty tycon then length
+      (* We apply bidirectionality hints only if an expected type is specified *)
+      else
       (* if `f` is a global, we retrieve bidirectionality hints *)
-      try
-        let (gr,_) = destRef sigma fj.uj_val in
-        Option.default length @@ GlobRef.Map.find_opt gr !bidi_hints
-      with DestKO ->
-        length
+        try
+          let (gr,_) = destRef sigma fj.uj_val in
+          Option.default length @@ GlobRef.Map.find_opt gr !bidi_hints
+        with DestKO ->
+          length
     in
     let candargs =
       (* Bidirectional typechecking hint:
@@ -813,24 +818,38 @@ struct
           else fun f v -> applist (f, [v])
       | _ -> fun _ f v -> applist (f, [v])
     in
-    let rec apply_rec env sigma n resj candargs bidiargs = function
-      | [] -> sigma, resj, List.rev bidiargs
+    let refresh_template env sigma resj =
+      (* Special case for inductive type applications that must be
+         refreshed right away. *)
+      match EConstr.kind sigma resj.uj_val with
+      | App (f,args) ->
+        if Termops.is_template_polymorphic_ind !!env sigma f then
+          let c = mkApp (f, args) in
+          let sigma, c = Evarsolve.refresh_universes (Some true) !!env sigma c in
+          let t = Retyping.get_type_of !!env sigma c in
+          sigma, make_judge c (* use this for keeping evars: resj.uj_val *) t
+        else sigma, resj
+      | _ -> sigma, resj
+    in
+    let rec apply_rec env sigma n resj resj_before_bidi candargs bidiargs = function
+      | [] -> sigma, resj, resj_before_bidi, List.rev bidiargs
       | c::rest ->
         let bidi = n >= nargs_before_bidi in
         let argloc = loc_of_glob_constr c in
-        let sigma, resj = Coercion.inh_app_fun ~program_mode resolve_tc !!env sigma resj in
+        let sigma, resj, trace = Coercion.inh_app_fun ~program_mode resolve_tc !!env sigma resj in
         let resty = whd_all !!env sigma resj.uj_type in
         match EConstr.kind sigma resty with
         | Prod (na,c1,c2) ->
-          let tycon = Some c1 in
           let (sigma, hj), bidiargs =
-            if bidi && Option.has_some tycon then
+            if bidi then
               (* We want to get some typing information from the context before
               typing the argument, so we replace it by an existential
               variable *)
               let sigma, c_hole = new_evar env sigma ~src:(loc,Evar_kinds.InternalHole) c1 in
-              (sigma, make_judge c_hole c1), (c_hole, c) :: bidiargs
-            else pretype tycon env sigma c, bidiargs
+              (sigma, make_judge c_hole c1), (c_hole, c, trace) :: bidiargs
+            else
+              let tycon = Some c1 in
+              pretype tycon env sigma c, bidiargs
           in
           let sigma, candargs, ujval =
             match candargs with
@@ -845,29 +864,18 @@ struct
           in
           let sigma, ujval = adjust_evar_source sigma na.binder_name ujval in
           let value, typ = app_f n (j_val resj) ujval, subst1 ujval c2 in
-          let j = { uj_val = value; uj_type = typ } in
-          apply_rec env sigma (n+1) j candargs bidiargs rest
+          let resj = { uj_val = value; uj_type = typ } in
+          let resj_before_bidi = if bidi then resj_before_bidi else resj in
+          apply_rec env sigma (n+1) resj resj_before_bidi candargs bidiargs rest
         | _ ->
           let sigma, hj = pretype empty_tycon env sigma c in
           error_cant_apply_not_functional
             ?loc:(Loc.merge_opt floc argloc) !!env sigma resj [|hj|]
     in
-    let sigma, resj, bidiargs = apply_rec env sigma 0 fj candargs [] args in
-    let sigma, resj =
-      match EConstr.kind sigma resj.uj_val with
-      | App (f,args) ->
-        if Termops.is_template_polymorphic_ind !!env sigma f then
-          (* Special case for inductive type applications that must be
-             refreshed right away. *)
-          let c = mkApp (f, args) in
-          let sigma, c = Evarsolve.refresh_universes (Some true) !!env sigma c in
-          let t = Retyping.get_type_of !!env sigma c in
-          sigma, make_judge c (* use this for keeping evars: resj.uj_val *) t
-        else sigma, resj
-      | _ -> sigma, resj
-    in
-    let sigma, t = inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma resj tycon in
-    let refine_arg sigma (newarg,origarg) =
+    let sigma, resj, resj_before_bidi, bidiargs = apply_rec env sigma 0 fj fj candargs [] args in
+    let sigma, resj = refresh_template env sigma resj in
+    let sigma, resj, otrace = inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma resj tycon in
+    let refine_arg n (sigma,t) (newarg,origarg,trace) =
       (* Refine an argument (originally `origarg`) represented by an evar
          (`newarg`) to use typing information from the context *)
       (* Recover the expected type of the argument *)
@@ -876,12 +884,25 @@ struct
       let sigma, j = pretype (Some ty) env sigma origarg in
       (* Unify the (possibly refined) existential variable with the
       (typechecked) original value *)
-      Evarconv.unify_delay !!env sigma newarg (j_val j)
+      let sigma = Evarconv.unify_delay !!env sigma newarg (j_val j) in
+      sigma, app_f n (Coercion.reapply_coercions sigma trace t) (j_val j)
     in
     (* We now refine any arguments whose typing was delayed for
        bidirectionality *)
-    let sigma = List.fold_left refine_arg sigma bidiargs in
-    (sigma, t)
+    let t = resj_before_bidi.uj_val in
+    let sigma, t = List.fold_left_i refine_arg nargs_before_bidi (sigma,t) bidiargs in
+    (* If we did not get a coercion trace (e.g. with `Program` coercions, we
+    replaced user-provided arguments with inferred ones. Otherwise, we apply
+    the coercion trace to the user-provided arguments. *)
+    let resj =
+      match otrace with
+      | None -> resj
+      | Some trace ->
+        let resj = { resj with uj_val = t } in
+        let sigma, resj = refresh_template env sigma resj in
+        { resj with uj_val = Coercion.reapply_coercions sigma trace t }
+    in
+    (sigma, resj)
 
   let pretype_lambda self (name, bk, c1, c2) =
     fun ?loc ~program_mode ~poly resolve_tc tycon env sigma ->
@@ -903,7 +924,7 @@ struct
     let sigma, j' = eval_pretyper self ~program_mode ~poly resolve_tc rng env' sigma c2 in
     let name = get_name var' in
     let resj = judge_of_abstraction !!env (orelse_name name name'.binder_name) j j' in
-    inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma resj tycon
+    discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma resj tycon
 
   let pretype_prod self (name, bk, c1, c2) =
     fun ?loc ~program_mode ~poly resolve_tc tycon env sigma ->
@@ -929,7 +950,7 @@ struct
         let (e, info) = CErrors.push e in
         let info = Option.cata (Loc.add_loc info) info loc in
         iraise (e, info) in
-      inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma resj tycon
+      discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma resj tycon
 
   let pretype_letin self (name, c1, t, c2) =
     fun ?loc ~program_mode ~poly resolve_tc tycon env sigma ->
@@ -1122,7 +1143,7 @@ struct
           mkCase (ci, pred, cj.uj_val, [|b1;b2|])
       in
       let cj = { uj_val = v; uj_type = p } in
-      inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma cj tycon
+      discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma cj tycon
 
   let pretype_cast self (c, k) =
     fun ?loc ~program_mode ~poly resolve_tc tycon env sigma ->
@@ -1165,7 +1186,7 @@ struct
         in
         let v = mkCast (cj.uj_val, k, tval) in
         sigma, { uj_val = v; uj_type = tval }
-    in inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma cj tycon
+    in discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma cj tycon
 
   let pretype_int self i =
     fun ?loc ~program_mode ~poly resolve_tc tycon env sigma ->
@@ -1174,7 +1195,7 @@ struct
           with Invalid_argument _ ->
             user_err ?loc ~hdr:"pretype" (str "Type of int63 should be registered first.")
         in
-        inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma resj tycon
+        discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma resj tycon
 
   let pretype_float self f =
     fun ?loc ~program_mode ~poly resolve_tc tycon env sigma ->
@@ -1183,7 +1204,7 @@ struct
         with Invalid_argument _ ->
           user_err ?loc ~hdr:"pretype" (str "Type of float should be registered first.")
         in
-        inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma resj tycon
+        discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma resj tycon
 
 (* [pretype_type valcon env sigma c] coerces [c] into a type *)
 let pretype_type self c ?loc ~program_mode ~poly resolve_tc valcon (env : GlobEnv.t) sigma = match DAst.get c with
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 48d5fac321..6486435ca2 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1290,7 +1290,7 @@ let is_mimick_head sigma ts f =
 
 let try_to_coerce env evd c cty tycon =
   let j = make_judge c cty in
-  let (evd',j') = inh_conv_coerce_rigid_to ~program_mode:false true env evd j tycon in
+  let (evd',j',_trace) = inh_conv_coerce_rigid_to ~program_mode:false true env evd j tycon in
   let evd' = Evarconv.solve_unif_constraints_with_heuristics env evd' in
   let evd' = Evd.map_metas_fvalue (fun c -> nf_evar evd' c) evd' in
     (evd',j'.uj_val)
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 58c0f7db53..e466992721 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -678,7 +678,7 @@ let define_with_type sigma env ev c =
   let t = Retyping.get_type_of env sigma ev in
   let ty = Retyping.get_type_of env sigma c in
   let j = Environ.make_judge c ty in
-  let (sigma, j) = Coercion.inh_conv_coerce_to ~program_mode:false true env sigma j t in
+  let (sigma, j, _trace) = Coercion.inh_conv_coerce_to ~program_mode:false true env sigma j t in
   let (ev, _) = destEvar sigma ev in
   let sigma = Evd.define ev j.Environ.uj_val sigma in
   sigma
diff --git a/test-suite/Makefile b/test-suite/Makefile
index b3a633e528..1d21b4b5e0 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -530,14 +530,16 @@ $(addsuffix .log,$(wildcard complexity/*.v)): %.v.log: %.v $(PREREQUISITELOG)
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
 	  true "extract effective user time"; \
-	  res=`$(coqc_interactive) "$<" $(call get_coq_prog_args,"$<") 2>&1 | sed -n -e "s/Finished transaction in .*(\([0-9]*\.[0-9]*\)u.*)/\1/p" | head -1 | sed "s/\r//g"`; \
+	  res=`$(coqc_interactive) "$<" $(call get_coq_prog_args,"$<") 2>&1 | sed -n -e "s/Finished .*transaction in .*(\([0-9]*\.[0-9]*\)u.*)/\1/p" | head -1 | sed "s/\r//g"`; \
 	  R=$$?; times; \
 	  if [ $$R != 0 ]; then \
 	    echo $(log_failure); \
 	    echo "    $<...Error! (should be accepted)" ; \
+	    $(FAIL); \
 	  elif [ "$$res" = "" ]; then \
 	    echo $(log_failure); \
 	    echo "    $<...Error! (couldn't find a time measure)"; \
+	    $(FAIL); \
 	  else \
 	    true "express effective time in centiseconds"; \
 	    resorig="$$res"; \
diff --git a/test-suite/bugs/bug_11140.v b/test-suite/bugs/bug_11140.v
new file mode 100644
index 0000000000..ca806ea324
--- /dev/null
+++ b/test-suite/bugs/bug_11140.v
@@ -0,0 +1,11 @@
+Axiom T : nat -> Prop.
+Axiom f : forall x, T x.
+Arguments f & x.
+
+Lemma test : (f (1 + _) : T 2) = f 2.
+match goal with
+| |- (f (1 + 1) = f 2) => idtac
+| |- (f 2 = f 2) => fail (* Issue 11140 *)
+| |- _ => fail
+end.
+Abort.
diff --git a/test-suite/bugs/closed/bug_11360.v b/test-suite/bugs/closed/bug_11360.v
new file mode 100644
index 0000000000..d8bc4a9f02
--- /dev/null
+++ b/test-suite/bugs/closed/bug_11360.v
@@ -0,0 +1,6 @@
+Section S.
+  Variable (A:Type).
+  #[universes(template)]
+  Inductive bar (d:A) := .
+End S.
+Check bar nat 0.