Merge PR #13166: Fixes #13165: implicit arguments in defined fields of record types not taken into account

Reviewed-by: SkySkimmer

13 files changed, 106 insertions, 51 deletions

diff --git a/dev/ci/user-overlays/13166-herbelin-master+fixes13165-missing-impargs-defined-fields.sh b/dev/ci/user-overlays/13166-herbelin-master+fixes13165-missing-impargs-defined-fields.sh
new file mode 100644
index 0000000000..7d55cf6883
--- /dev/null
+++ b/dev/ci/user-overlays/13166-herbelin-master+fixes13165-missing-impargs-defined-fields.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "13166" ] || [ "$CI_BRANCH" = "master+fixes13165-missing-impargs-defined-fields" ]; then
+
+    elpi_CI_REF=coq-master+adapt-coq-pr13166-impargs-record-fields
+    elpi_CI_GITURL=https://github.com/herbelin/coq-elpi
+
+fi
diff --git a/doc/changelog/02-specification-language/13166-master+fixes13165-missing-impargs-defined-fields.rst b/doc/changelog/02-specification-language/13166-master+fixes13165-missing-impargs-defined-fields.rst
new file mode 100644
index 0000000000..006989e6b3
--- /dev/null
+++ b/doc/changelog/02-specification-language/13166-master+fixes13165-missing-impargs-defined-fields.rst
@@ -0,0 +1,5 @@
+- **Fixed:**
+  Implicit arguments taken into account in defined fields of a record type declaration
+  (`#13166 <https://github.com/coq/coq/pull/13166>`_,
+  fixes `#13165 <https://github.com/coq/coq/issues/13165>`_,
+  by Hugo Herbelin).
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 3996c64b67..ffae2866c0 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -128,7 +128,7 @@ let classify_vernac e =
         | Constructors l -> List.map (fun (_,({v=id},_)) -> id) l
         | RecordDecl (oid,l) -> (match oid with Some {v=x} -> [x] | _ -> []) @
            CList.map_filter (function
-            | AssumExpr({v=Names.Name n},_), _ -> Some n
+            | AssumExpr({v=Names.Name n},_,_), _ -> Some n
             | _ -> None) l) l in
         VtSideff (List.flatten ids, VtLater)
     | VernacScheme l ->
diff --git a/test-suite/success/Record.v b/test-suite/success/Record.v
index ce07512a1e..beb424dd40 100644
--- a/test-suite/success/Record.v
+++ b/test-suite/success/Record.v
@@ -93,3 +93,18 @@ Record R : Type := {
 (* This is used in a couple of development such as UniMatch *)
 
 Record S {A:Type} := { a : A; b : forall A:Type, A }.
+
+(* Bug #13165 on implicit arguments in defined fields *)
+Record T := {
+ f {n:nat} (p:n=n) := nat;
+ g := f (eq_refl 0)
+}.
+
+(* Slight improvement in when SProp relevance is detected *)
+Inductive True : SProp := I.
+Inductive eqI : True -> SProp := reflI : eqI I.
+
+Record U (c:True) := {
+ u := c;
+ v := reflI : eqI u;
+ }.
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 401ba0fba4..12194ea20c 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -68,10 +68,12 @@ let declare_axiom is_coe ~poly ~local ~kind typ (univs, pl) imps nl {CAst.v=name
   let inst = instance_of_univ_entry univs in
   (gr,inst)
 
-let interp_assumption ~program_mode sigma env impls c =
+let interp_assumption ~program_mode env sigma impl_env bl c =
   let flags = { Pretyping.all_no_fail_flags with program_mode } in
-  let sigma, (ty, impls) = interp_type_evars_impls ~flags env sigma ~impls c in
-  sigma, (ty, impls)
+  let sigma, (impls, ((env_bl, ctx), impls1)) = interp_context_evars ~program_mode ~impl_env env sigma bl in
+  let sigma, (ty, impls2) = interp_type_evars_impls ~flags env_bl sigma ~impls c in
+  let ty = EConstr.it_mkProd_or_LetIn ty ctx in
+  sigma, ty, impls1@impls2
 
 (* When monomorphic the universe constraints and universe names are
    declared with the first declaration only. *)
@@ -153,7 +155,7 @@ let do_assumptions ~program_mode ~poly ~scope ~kind nl l =
   in
   (* We interpret all declarations in the same evar_map, i.e. as a telescope. *)
   let (sigma,_,_),l = List.fold_left_map (fun (sigma,env,ienv) (is_coe,(idl,c)) ->
-    let sigma,(t,imps) = interp_assumption ~program_mode sigma env ienv c in
+    let sigma,t,imps = interp_assumption ~program_mode env sigma ienv [] c in
     let r = Retyping.relevance_of_type env sigma t in
     let env =
       EConstr.push_named_context (List.map (fun {CAst.v=id} -> LocalAssum (make_annot id r,t)) idl) env in
diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli
index 3d425ad768..64b8212b90 100644
--- a/vernac/comAssumption.mli
+++ b/vernac/comAssumption.mli
@@ -14,6 +14,15 @@ open Constrexpr
 
 (** {6 Parameters/Assumptions} *)
 
+val interp_assumption
+  : program_mode:bool
+  -> Environ.env
+  -> Evd.evar_map
+  -> Constrintern.internalization_env
+  -> Constrexpr.local_binder_expr list
+  -> constr_expr
+  -> Evd.evar_map * EConstr.t * Impargs.manual_implicits
+
 val do_assumptions
   :  program_mode:bool
   -> poly:bool
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index 37b7106856..c1dbf0a1ea 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -81,14 +81,11 @@ let protect_pattern_in_binder bl c ctypopt =
   else
     (bl, c, ctypopt, fun f env evd c -> f env evd c)
 
-let interp_definition ~program_mode pl bl ~poly red_option c ctypopt =
+let interp_definition ~program_mode env evd impl_env bl red_option c ctypopt =
   let flags = Pretyping.{ all_no_fail_flags with program_mode } in
-  let env = Global.env() in
-  (* Explicitly bound universes and constraints *)
-  let evd, udecl = Constrexpr_ops.interp_univ_decl_opt env pl in
   let (bl, c, ctypopt, apply_under_binders) = protect_pattern_in_binder bl c ctypopt in
   (* Build the parameters *)
-  let evd, (impls, ((env_bl, ctx), imps1)) = interp_context_evars ~program_mode env evd bl in
+  let evd, (impls, ((env_bl, ctx), imps1)) = interp_context_evars ~program_mode ~impl_env env evd bl in
   (* Build the type *)
   let evd, tyopt = Option.fold_left_map
       (interp_type_evars_impls ~flags ~impls env_bl)
@@ -111,12 +108,15 @@ let interp_definition ~program_mode pl bl ~poly red_option c ctypopt =
   (* Declare the definition *)
   let c = EConstr.it_mkLambda_or_LetIn c ctx in
   let tyopt = Option.map (fun ty -> EConstr.it_mkProd_or_LetIn ty ctx) tyopt in
-  (c, tyopt), evd, udecl, imps
+  evd, (c, tyopt), imps
 
 let do_definition ?hook ~name ~scope ~poly ~kind udecl bl red_option c ctypopt =
   let program_mode = false in
-  let (body, types), evd, udecl, impargs =
-    interp_definition ~program_mode udecl bl ~poly red_option c ctypopt
+  let env = Global.env() in
+  (* Explicitly bound universes and constraints *)
+  let evd, udecl = Constrexpr_ops.interp_univ_decl_opt env udecl in
+  let evd, (body, types), impargs =
+    interp_definition ~program_mode env evd empty_internalization_env bl red_option c ctypopt
   in
   let kind = Decls.IsDefinition kind in
   let cinfo = Declare.CInfo.make ~name ~impargs ~typ:types () in
@@ -127,8 +127,11 @@ let do_definition ?hook ~name ~scope ~poly ~kind udecl bl red_option c ctypopt =
 
 let do_definition_program ?hook ~pm ~name ~scope ~poly ~kind udecl bl red_option c ctypopt =
   let program_mode = true in
-  let (body, types), evd, udecl, impargs =
-    interp_definition ~program_mode udecl bl ~poly red_option c ctypopt
+  let env = Global.env() in
+  (* Explicitly bound universes and constraints *)
+  let evd, udecl = Constrexpr_ops.interp_univ_decl_opt env udecl in
+  let evd, (body, types), impargs =
+    interp_definition ~program_mode env evd empty_internalization_env bl red_option c ctypopt
   in
   let term, typ, uctx, obls = Declare.Obls.prepare_obligation ~name ~body ~types evd in
   let pm, _ =
diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli
index d95e64a85f..7420235449 100644
--- a/vernac/comDefinition.mli
+++ b/vernac/comDefinition.mli
@@ -14,6 +14,17 @@ open Constrexpr
 
 (** {6 Definitions/Let} *)
 
+val interp_definition
+  :  program_mode:bool
+  -> Environ.env
+  -> Evd.evar_map
+  -> Constrintern.internalization_env
+  -> Constrexpr.local_binder_expr list
+  -> red_expr option
+  -> constr_expr
+  -> constr_expr option
+  -> Evd.evar_map * (EConstr.t * EConstr.t option) * Impargs.manual_implicits
+
 val do_definition
   :  ?hook:Declare.Hook.t
   -> name:Id.t
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 49d4847fde..dfc7b05b51 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -429,19 +429,19 @@ GRAMMAR EXTEND Gram
   ;
   record_binder_body:
     [ [ l = binders; oc = of_type_with_opt_coercion;
-         t = lconstr -> { fun id -> (oc,AssumExpr (id,mkProdCN ~loc l t)) }
+         t = lconstr -> { fun id -> (oc,AssumExpr (id,l,t)) }
       | l = binders; oc = of_type_with_opt_coercion;
          t = lconstr; ":="; b = lconstr -> { fun id ->
-           (oc,DefExpr (id,mkLambdaCN ~loc l b,Some (mkProdCN ~loc l t))) }
+           (oc,DefExpr (id,l,b,Some t)) }
       | l = binders; ":="; b = lconstr -> { fun id ->
          match b.CAst.v with
          | CCast(b', (CastConv t|CastVM t|CastNative t)) ->
-             (NoInstance,DefExpr(id,mkLambdaCN ~loc l b',Some (mkProdCN ~loc l t)))
+             (NoInstance,DefExpr(id,l,b',Some t))
          | _ ->
-             (NoInstance,DefExpr(id,mkLambdaCN ~loc l b,None)) } ] ]
+             (NoInstance,DefExpr(id,l,b,None)) } ] ]
   ;
   record_binder:
-    [ [ id = name -> { (NoInstance,AssumExpr(id, CAst.make ~loc @@ CHole (None, IntroAnonymous, None))) }
+    [ [ id = name -> { (NoInstance,AssumExpr(id, [], CAst.make ~loc @@ CHole (None, IntroAnonymous, None))) }
       | id = name; f = record_binder_body -> { f id } ] ]
   ;
   assum_list:
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index e9cd4272e6..0e660bf20c 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -508,13 +508,15 @@ let pr_oc = function
 
 let pr_record_field (x, { rf_subclass = oc ; rf_priority = pri ; rf_notation = ntn }) =
   let prx = match x with
-    | AssumExpr (id,t) ->
+    | AssumExpr (id,binders,t) ->
       hov 1 (pr_lname id ++
+             pr_binders_arg binders ++ spc() ++
              pr_oc oc ++ spc() ++
              pr_lconstr_expr t)
-    | DefExpr(id,b,opt) -> (match opt with
+    | DefExpr(id,binders,b,opt) -> (match opt with
         | Some t ->
           hov 1 (pr_lname id ++
+                 pr_binders_arg binders ++ spc() ++
                  pr_oc oc ++ spc() ++
                  pr_lconstr_expr t ++ str" :=" ++ pr_lconstr b)
         | None ->
diff --git a/vernac/record.ml b/vernac/record.ml
index e362cb052a..a4bf9893d9 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -62,23 +62,33 @@ let () =
 let interp_fields_evars env sigma ~ninds ~nparams impls_env nots l =
   let _, sigma, impls, newfs, _ =
     List.fold_left2
-      (fun (env, sigma, uimpls, params, impls) no ({CAst.loc;v=i}, b, t) ->
-         let sigma, (t', impl) = interp_type_evars_impls env sigma ~impls t in
-         let r = Retyping.relevance_of_type env sigma t' in
-         let sigma, b' =
-           Option.cata (fun x -> on_snd (fun x -> Some (fst x)) @@
-                         interp_casted_constr_evars_impls ~program_mode:false env sigma ~impls x t') (sigma,None) b in
-         let impls =
+      (fun (env, sigma, uimpls, params, impls_env) no d ->
+         let sigma, (i, b, t), impl = match d with
+           | Vernacexpr.AssumExpr({CAst.loc;v=id},bl,t) ->
+             (* Temporary compatibility with the type-classes heuristics *)
+             (* which are applied after the interpretation of bl and *)
+             (* before the one of t otherwise (see #13166) *)
+             let t = if bl = [] then t else mkCProdN bl t in
+             let sigma, t, impl =
+               ComAssumption.interp_assumption ~program_mode:false env sigma impls_env [] t in
+             sigma, (id, None, t), impl
+           | Vernacexpr.DefExpr({CAst.loc;v=id},bl,b,t) ->
+             let sigma, (b, t), impl =
+               ComDefinition.interp_definition ~program_mode:false env sigma impls_env bl None b t in
+             let t = match t with Some t -> t | None -> Retyping.get_type_of env sigma b in
+             sigma, (id, Some b, t), impl in
+          let r = Retyping.relevance_of_type env sigma t in
+         let impls_env =
            match i with
-           | Anonymous -> impls
-           | Name id -> Id.Map.add id (compute_internalization_data env sigma id Constrintern.Method t' impl) impls
+           | Anonymous -> impls_env
+           | Name id -> Id.Map.add id (compute_internalization_data env sigma id Constrintern.Method t impl) impls_env
          in
-         let d = match b' with
-           | None -> LocalAssum (make_annot i r,t')
-           | Some b' -> LocalDef (make_annot i r,b',t')
+         let d = match b with
+           | None -> LocalAssum (make_annot i r,t)
+           | Some b -> LocalDef (make_annot i r,b,t)
          in
-         List.iter (Metasyntax.set_notation_for_interpretation env impls) no;
-         (EConstr.push_rel d env, sigma, impl :: uimpls, d::params, impls))
+         List.iter (Metasyntax.set_notation_for_interpretation env impls_env) no;
+         (EConstr.push_rel d env, sigma, impl :: uimpls, d::params, impls_env))
       (env, sigma, [], [], impls_env) nots l
   in
   let _, _, sigma = Context.Rel.fold_outside ~init:(env,0,sigma) (fun f (env,k,sigma) ->
@@ -101,14 +111,6 @@ let compute_constructor_level evars env l =
     in (EConstr.push_rel d env, univ))
     l (env, Univ.Universe.sprop)
 
-let binder_of_decl = function
-  | Vernacexpr.AssumExpr(n,t) -> (n,None,t)
-  | Vernacexpr.DefExpr(n,c,t) ->
-    (n,Some c, match t with Some c -> c
-                          | None   -> CAst.make ?loc:n.CAst.loc @@ CHole (None, Namegen.IntroAnonymous, None))
-
-let binders_of_decls = List.map binder_of_decl
-
 let check_anonymous_type ind =
   match ind with
   | { CAst.v = CSort (Glob_term.UAnonymous {rigid=true}) } -> true
@@ -176,7 +178,7 @@ let typecheck_params_and_fields def poly pl ps records =
   let ninds = List.length arities in
   let nparams = List.length newps in
   let fold sigma (_, _, nots, fs) arity =
-    interp_fields_evars env_ar sigma ~ninds ~nparams impls_env nots (binders_of_decls fs)
+    interp_fields_evars env_ar sigma ~ninds ~nparams impls_env nots fs
   in
   let (sigma, data) = List.fold_left2_map fold sigma records arities in
   let sigma =
@@ -676,8 +678,8 @@ open Vernacexpr
 
 let check_unique_names records =
   let extract_name acc (rf_decl, _) = match rf_decl with
-      Vernacexpr.AssumExpr({CAst.v=Name id},_) -> id::acc
-    | Vernacexpr.DefExpr ({CAst.v=Name id},_,_) -> id::acc
+      Vernacexpr.AssumExpr({CAst.v=Name id},_,_) -> id::acc
+    | Vernacexpr.DefExpr ({CAst.v=Name id},_,_,_) -> id::acc
     | _ -> acc in
   let allnames =
     List.fold_left (fun acc (_, id, _, cfs, _, _) ->
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 0d3f38d139..3ced38d6ea 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -700,7 +700,7 @@ let vernac_record ~template udecl ~cumulative k ~poly finite records =
       if Dumpglob.dump () then
         let () = Dumpglob.dump_definition id false "rec" in
         let iter (x, _) = match x with
-        | Vernacexpr.AssumExpr ({loc;v=Name id}, _) ->
+        | Vernacexpr.(AssumExpr ({loc;v=Name id}, _, _) | DefExpr ({loc;v=Name id}, _, _, _)) ->
           Dumpglob.dump_definition (make ?loc id) false "proj"
         | _ -> ()
         in
@@ -777,7 +777,7 @@ let vernac_inductive ~atts kind indl =
     in
     let (coe, (lid, ce)) = l in
     let coe' = if coe then BackInstance else NoInstance in
-    let f = AssumExpr ((make ?loc:lid.loc @@ Name lid.v), ce),
+    let f = AssumExpr ((make ?loc:lid.loc @@ Name lid.v), [], ce),
             { rf_subclass = coe' ; rf_priority = None ; rf_notation = [] ; rf_canonical = true } in
     vernac_record ~template udecl ~cumulative (Class true) ~poly finite [id, bl, c, None, [f]]
   else if List.for_all is_record indl then
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index eeebb43114..6a9a74144f 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -167,8 +167,8 @@ type fixpoint_expr = recursion_order_expr option fix_expr_gen
 type cofixpoint_expr = unit fix_expr_gen
 
 type local_decl_expr =
-  | AssumExpr of lname * constr_expr
-  | DefExpr of lname * constr_expr * constr_expr option
+  | AssumExpr of lname * local_binder_expr list * constr_expr
+  | DefExpr of lname * local_binder_expr list * constr_expr * constr_expr option
 
 type inductive_kind = Inductive_kw | CoInductive | Variant | Record | Structure | Class of bool (* true = definitional, false = inductive *)
 type simple_binder = lident list  * constr_expr