Fixes/enhancements with local definitions in records.

Fixes implicit arguments from the body of a defined field not taken into account.
Get (a bit) more information for detection of SProp relevance in
implicitly-typed defined field. (It should be done at the very end of
the inference phase, though, because some evars may not yet be
instantiated.)

8 files changed, 58 insertions, 38 deletions

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 56f846ebdb..12194ea20c 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -71,7 +71,8 @@ let declare_axiom is_coe ~poly ~local ~kind typ (univs, pl) imps nl {CAst.v=name
 let interp_assumption ~program_mode env sigma impl_env bl c =
   let flags = { Pretyping.all_no_fail_flags with program_mode } in
   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 sigma ~impls c 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
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