Merge PR#662: Fixing bug #5233 and another bug with implicit arguments + a short econstr-cleaning of record.ml

10 files changed, 73 insertions, 56 deletions

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 5a05150d4..33d7acc31 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -45,6 +45,7 @@ val of_named_decl : (Constr.t, Constr.types) Context.Named.Declaration.pt -> (t,
 val unsafe_to_named_decl : (t, t) Context.Named.Declaration.pt -> (Constr.t, Constr.types) Context.Named.Declaration.pt
 val unsafe_to_rel_decl : (t, t) Context.Rel.Declaration.pt -> (Constr.t, Constr.types) Context.Rel.Declaration.pt
 val of_rel_decl : (Constr.t, Constr.types) Context.Rel.Declaration.pt -> (t, t) Context.Rel.Declaration.pt
+val to_rel_decl : Evd.evar_map -> (t, t) Context.Rel.Declaration.pt -> (Constr.t, Constr.types) Context.Rel.Declaration.pt
 end =
 struct
 
@@ -131,6 +132,7 @@ let of_named_decl d = d
 let unsafe_to_named_decl d = d
 let of_rel_decl d = d
 let unsafe_to_rel_decl d = d
+let to_rel_decl sigma d = Context.Rel.Declaration.map_constr (to_constr sigma) d
 
 end
 
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 9f45187cf..94b7ca96a 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -268,6 +268,8 @@ val is_global : Evd.evar_map -> Globnames.global_reference -> t -> bool
 val of_named_decl : (Constr.t, Constr.types) Context.Named.Declaration.pt -> (t, types) Context.Named.Declaration.pt
 val of_rel_decl : (Constr.t, Constr.types) Context.Rel.Declaration.pt -> (t, types) Context.Rel.Declaration.pt
 
+val to_rel_decl : Evd.evar_map -> (t, types) Context.Rel.Declaration.pt -> (Constr.t, Constr.types) Context.Rel.Declaration.pt
+
 (** {5 Unsafe operations} *)
 
 module Unsafe :
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 336cfac85..6f17324a1 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -46,7 +46,7 @@ open Context.Rel.Declaration
    types and recursive definitions and of projection names in records *)
 
 type var_internalization_type =
-  | Inductive of Id.t list (* list of params *)
+  | Inductive of Id.t list (* list of params *) * bool (* true = check for possible capture *)
   | Recursive
   | Method
   | Variable
@@ -176,7 +176,7 @@ let parsing_explicit = ref false
 let empty_internalization_env = Id.Map.empty
 
 let compute_explicitable_implicit imps = function
-  | Inductive params ->
+  | Inductive (params,_) ->
       (* In inductive types, the parameters are fixed implicit arguments *)
       let sub_impl,_ = List.chop (List.length params) imps in
       let sub_impl' = List.filter is_status_implicit sub_impl in
@@ -190,10 +190,10 @@ let compute_internalization_data env ty typ impl =
   let expls_impl = compute_explicitable_implicit impl ty in
   (ty, expls_impl, impl, compute_arguments_scope typ)
 
-let compute_internalization_env env ty =
+let compute_internalization_env env ?(impls=empty_internalization_env) ty =
   List.fold_left3
     (fun map id typ impl -> Id.Map.add id (compute_internalization_data env ty typ impl) map)
-    empty_internalization_env
+    impls
 
 (**********************************************************************)
 (* Contracting "{ _ }" in notations *)
@@ -358,16 +358,17 @@ let locate_if_hole ?loc na = function
 
 let reset_hidden_inductive_implicit_test env =
   { env with impls = Id.Map.map (function
-         | (Inductive _,b,c,d) -> (Inductive [],b,c,d)
+         | (Inductive (params,_),b,c,d) -> (Inductive (params,false),b,c,d)
          | x -> x) env.impls }
 
-let check_hidden_implicit_parameters id impls =
+let check_hidden_implicit_parameters ?loc id impls =
   if Id.Map.exists (fun _ -> function
-    | (Inductive indparams,_,_,_) -> Id.List.mem id indparams
+    | (Inductive (indparams,check),_,_,_) when check -> Id.List.mem id indparams
     | _ -> false) impls
   then
-    user_err  (strbrk "A parameter of an inductive type " ++
-    pr_id id ++ strbrk " is not allowed to be used as a bound variable in the type of its constructor.")
+    user_err ?loc (pr_id id ++ strbrk " is already used as name of " ++
+      strbrk "a parameter of the inductive type; bound variables in " ++
+      strbrk "the type of a constructor shall use a different name.")
 
 let push_name_env ?(global_level=false) ntnvars implargs env =
   function
@@ -376,7 +377,7 @@ let push_name_env ?(global_level=false) ntnvars implargs env =
 	user_err ?loc (str "Anonymous variables not allowed");
       env
   | loc,Name id ->
-      check_hidden_implicit_parameters id env.impls ;
+      check_hidden_implicit_parameters ?loc id env.impls ;
       if Id.Map.is_empty ntnvars && Id.equal id ldots_var
         then error_ldots_var ?loc;
       set_var_scope ?loc id false env ntnvars;
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 324f7a389..a92e94d97 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -38,7 +38,7 @@ open Misctypes
    of [env] *)
 
 type var_internalization_type =
-  | Inductive of Id.t list (* list of params *)
+  | Inductive of Id.t list (* list of params *) * bool (* true = check for possible capture *)
   | Recursive
   | Method
   | Variable
@@ -61,7 +61,7 @@ val empty_internalization_env : internalization_env
 val compute_internalization_data : env -> var_internalization_type ->
   types -> Impargs.manual_explicitation list -> var_internalization_data
 
-val compute_internalization_env : env -> var_internalization_type ->
+val compute_internalization_env : env -> ?impls:internalization_env -> var_internalization_type ->
   Id.t list -> types list -> Impargs.manual_explicitation list list ->
   internalization_env
 
diff --git a/test-suite/bugs/closed/5233.v b/test-suite/bugs/closed/5233.v
new file mode 100644
index 000000000..06286c740
--- /dev/null
+++ b/test-suite/bugs/closed/5233.v
@@ -0,0 +1,2 @@
+(* Implicit arguments on type were missing for recursive records *)
+Inductive foo {A : Type} : Type := { Foo : foo }.
diff --git a/test-suite/success/ImplicitArguments.v b/test-suite/success/ImplicitArguments.v
index f07773f8b..921433cad 100644
--- a/test-suite/success/ImplicitArguments.v
+++ b/test-suite/success/ImplicitArguments.v
@@ -27,3 +27,8 @@ Parameters (a:_) (b:a=0).
 Definition foo6 (x:=1) : forall {n:nat}, n=n := fun n => eq_refl.
 
 Fixpoint foo7 (x:=1) (n:nat) {p:nat} {struct n} : nat.
+
+(* Some example which should succeed with local implicit arguments *)
+
+Inductive A {P:forall m {n}, n=m -> Prop} := C : P 0 eq_refl -> A.
+Inductive B (P:forall m {n}, n=m -> Prop) := D : P 0 eq_refl -> B P.
diff --git a/test-suite/success/Record.v b/test-suite/success/Record.v
index 8334322c9..6f27c1d36 100644
--- a/test-suite/success/Record.v
+++ b/test-suite/success/Record.v
@@ -87,3 +87,8 @@ Record R : Type := {
   P (A : Type) : Prop := exists x : A -> A, x = x;
   Q A : P A -> P A
 }.
+
+(* We allow reusing an implicit parameter named in non-recursive types *)
+(* This is used in a couple of development such as UniMatch *)
+
+Record S {A:Type} := { a : A; b : forall A:Type, A }.
diff --git a/test-suite/success/coindprim.v b/test-suite/success/coindprim.v
index 5b9265b6a..05ab91393 100644
--- a/test-suite/success/coindprim.v
+++ b/test-suite/success/coindprim.v
@@ -13,9 +13,10 @@ Definition eta {A} (s : Stream A) := {| hd := s.(hd); tl := s.(tl) |}.
 CoFixpoint ones := {| hd := 1; tl := ones |}.
 CoFixpoint ticks := {| hd := tt; tl := ticks |}.
 
-CoInductive stream_equiv {A} {s : Stream A} {s' : Stream A} : Prop :=
-  mkStreamEq { hdeq : s.(hd) = s'.(hd); tleq : stream_equiv _ s.(tl) s'.(tl) }.
-Arguments stream_equiv {A} s s'.
+CoInductive stream_equiv {A} (s : Stream A) (s' : Stream A) : Prop :=
+  mkStreamEq { hdeq : s.(hd) = s'.(hd); tleq : stream_equiv s.(tl) s'.(tl) }.
+Arguments hdeq {A} {s} {s'}.
+Arguments tleq {A} {s} {s'}.
 
 Program CoFixpoint ones_eq : stream_equiv ones ones.(tl) :=
   {| hdeq := eq_refl; tleq := ones_eq |}.
@@ -88,4 +89,4 @@ Lemma eq (x : U) : x = force x.
 Proof.
   Fail destruct x.
 Abort.
-  (* Impossible *)
\ No newline at end of file
+  (* Impossible *)
diff --git a/vernac/command.ml b/vernac/command.ml
index 0f9dee12c..ad84c17b7 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -582,7 +582,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
   let pl = (List.hd indl).ind_univs in
   let ctx = Evd.make_evar_universe_context env0 pl in
   let evdref = ref Evd.(from_ctx ctx) in
-  let _, ((env_params, ctx_params), userimpls) =
+  let impls, ((env_params, ctx_params), userimpls) =
     interp_context_evars env0 evdref paramsl
   in
   let ctx_params = List.map (fun d -> map_rel_decl EConstr.Unsafe.to_constr d) ctx_params in
@@ -603,7 +603,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
   let indimpls = List.map (fun (_, _, impls) -> userimpls @ 
     lift_implicits (Context.Rel.nhyps ctx_params) impls) arities in
   let arities = List.map pi1 arities and aritypoly = List.map pi2 arities in
-  let impls = compute_internalization_env env0 (Inductive params) indnames fullarities indimpls in
+  let impls = compute_internalization_env env0 ~impls (Inductive (params,true)) indnames fullarities indimpls in
   let implsforntn = compute_internalization_env env0 Variable indnames fullarities indimpls in
   let mldatas = List.map2 (mk_mltype_data evdref env_params params) arities indnames in
 
diff --git a/vernac/record.ml b/vernac/record.ml
index f8e12f4ee..8cde88dc9 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -63,29 +63,28 @@ let interp_fields_evars env evars impls_env nots l =
   List.fold_left2
     (fun (env, uimpls, params, impls) no ((loc, i), b, t) ->
       let t', impl = interp_type_evars_impls env evars ~impls t in
-      let b' = Option.map (fun x -> EConstr.Unsafe.to_constr (fst (interp_casted_constr_evars_impls env evars ~impls x t'))) b in
-      let t' = EConstr.Unsafe.to_constr t' in
+      let b' = Option.map (fun x -> fst (interp_casted_constr_evars_impls env evars ~impls x t')) b in
       let impls =
 	match i with
 	| Anonymous -> impls
-	| Name id -> Id.Map.add id (compute_internalization_data env Constrintern.Method t' impl) impls
+	| Name id -> Id.Map.add id (compute_internalization_data env Constrintern.Method (EConstr.to_constr !evars t') impl) impls
       in
       let d = match b' with
 	      | None -> LocalAssum (i,t')
 	      | Some b' -> LocalDef (i,b',t')
       in
       List.iter (Metasyntax.set_notation_for_interpretation impls) no;
-      (push_rel d env, impl :: uimpls, d::params, impls))
+      (EConstr.push_rel d env, impl :: uimpls, d::params, impls))
     (env, [], [], impls_env) nots l
 
 let compute_constructor_level evars env l =
   List.fold_right (fun d (env, univ) ->
     let univ = 
       if is_local_assum d then
-	let s = Retyping.get_sort_of env evars (EConstr.of_constr (RelDecl.get_type d)) in
+	let s = Retyping.get_sort_of env evars (RelDecl.get_type d) in
 	  Univ.sup (univ_of_sort s) univ 
       else univ
-    in (push_rel d env, univ)) 
+    in (EConstr.push_rel d env, univ))
     l (env, Univ.type0m_univ)
 
 let binder_of_decl = function
@@ -95,7 +94,7 @@ let binder_of_decl = function
 
 let binders_of_decls = List.map binder_of_decl
 
-let typecheck_params_and_fields def id pl t ps nots fs =
+let typecheck_params_and_fields finite def id pl t ps nots fs =
   let env0 = Global.env () in
   let ctx = Evd.make_evar_universe_context env0 pl in
   let evars = ref (Evd.from_ctx ctx) in
@@ -113,63 +112,63 @@ let typecheck_params_and_fields def id pl t ps nots fs =
               Loc.raise ?loc (Stream.Error "pattern with quote not allowed in record parameters.")) ps
   in 
   let impls_env, ((env1,newps), imps) = interp_context_evars env0 evars ps in
-  let newps = List.map (fun d -> Termops.map_rel_decl EConstr.Unsafe.to_constr d) newps in
-  let t', template = match t with 
+  let typ, sort, template = match t with
     | Some t -> 
-       let env = push_rel_context newps env0 in
+       let env = EConstr.push_rel_context newps env0 in
        let poly =
          match t with
          | { CAst.v = CSort (Misctypes.GType []) } -> true | _ -> false in
        let s = interp_type_evars env evars ~impls:empty_internalization_env t in
        let sred = Reductionops.whd_all env !evars s in
-       let s = EConstr.Unsafe.to_constr s in
-       let sred = EConstr.Unsafe.to_constr sred in
-	 (match kind_of_term sred with
-	 | Sort s' -> 
+	 (match EConstr.kind !evars sred with
+	 | Sort s' ->
+            let s' = EConstr.ESorts.kind !evars s' in
 	    (if poly then
                match Evd.is_sort_variable !evars s' with
 	       | Some l -> evars := Evd.make_flexible_variable !evars true l; 
-	                  sred, true
-	       | None -> s, false
-             else s, false)
+	                  s, s', true
+	       | None -> s, s', false
+             else s, s', false)
 	 | _ -> user_err ?loc:(constr_loc t) (str"Sort expected."))
     | None -> 
       let uvarkind = Evd.univ_flexible_alg in
-	mkSort (Evarutil.evd_comb0 (Evd.new_sort_variable uvarkind) evars), true
+      let s = Evarutil.evd_comb0 (Evd.new_sort_variable uvarkind) evars in
+      EConstr.mkSort s, s, true
   in
-  let fullarity = it_mkProd_or_LetIn t' newps in
-  let env_ar = push_rel_context newps (push_rel (LocalAssum (Name id,fullarity)) env0) in
+  let arity = EConstr.it_mkProd_or_LetIn typ newps in
+  let env_ar = EConstr.push_rel_context newps (EConstr.push_rel (LocalAssum (Name id,arity)) env0) in
+  let assums = List.filter is_local_assum newps in
+  let params = List.map (RelDecl.get_name %> out_name) assums in
+  let ty = Inductive (params,(finite != BiFinite)) in
+  let impls_env = compute_internalization_env env0 ~impls:impls_env ty [id] [EConstr.to_constr !evars arity] [imps] in
   let env2,impls,newfs,data =
     interp_fields_evars env_ar evars impls_env nots (binders_of_decls fs)
   in
-  let sigma = 
+  let evars =
     Pretyping.solve_remaining_evars Pretyping.all_and_fail_flags env_ar !evars Evd.empty in
-  let evars, nf = Evarutil.nf_evars_and_universes sigma in
-  let arity = nf t' in
-  let arity, evars = 
+  let typ, evars =
     let _, univ = compute_constructor_level evars env_ar newfs in
-    let ctx, aritysort = Reduction.dest_arity env0 arity in
-      assert(List.is_empty ctx); (* Ensured by above analysis *)
-      if not def && (Sorts.is_prop aritysort || 
-	(Sorts.is_set aritysort && is_impredicative_set env0)) then
-	arity, evars
+      if not def && (Sorts.is_prop sort ||
+	(Sorts.is_set sort && is_impredicative_set env0)) then
+	typ, evars
       else
-	let evars = Evd.set_leq_sort env_ar evars (Type univ) aritysort in
+	let evars = Evd.set_leq_sort env_ar evars (Type univ) sort in
 	if Univ.is_small_univ univ &&
-	   Option.cata (Evd.is_flexible_level evars) false (Evd.is_sort_variable evars aritysort) then
+	   Option.cata (Evd.is_flexible_level evars) false (Evd.is_sort_variable evars sort) then
 	   (* We can assume that the level in aritysort is not constrained
 	       and clear it, if it is flexible *)
-	  mkArity (ctx, Sorts.sort_of_univ univ),
-	  Evd.set_eq_sort env_ar evars (Prop Pos) aritysort
-	else arity, evars
+	  EConstr.mkSort (Sorts.sort_of_univ univ),
+	  Evd.set_eq_sort env_ar evars (Prop Pos) sort
+	else typ, evars
   in
   let evars, nf = Evarutil.nf_evars_and_universes evars in
-  let newps = Context.Rel.map nf newps in
-  let newfs = Context.Rel.map nf newfs in
+  let newfs = List.map (EConstr.to_rel_decl evars) newfs in
+  let newps = List.map (EConstr.to_rel_decl evars) newps in
+  let typ = EConstr.to_constr evars typ in
   let ce t = Pretyping.check_evars env0 Evd.empty evars (EConstr.of_constr t) in
     List.iter (iter_constr ce) (List.rev newps);
     List.iter (iter_constr ce) (List.rev newfs);
-    Evd.universe_context ?names:pl evars, nf arity, template, imps, newps, impls, newfs
+    Evd.universe_context ?names:pl evars, typ, template, imps, newps, impls, newfs
 
 let degenerate_decl decl =
   let id = match RelDecl.get_name decl with
@@ -565,7 +564,7 @@ let definition_structure (kind,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cfs,id
   (* Now, younger decl in params and fields is on top *)
   let (pl, ctx), arity, template, implpars, params, implfs, fields =
     States.with_state_protection (fun () ->
-      typecheck_params_and_fields (kind = Class true) idstruc pl s ps notations fs) () in
+      typecheck_params_and_fields finite (kind = Class true) idstruc pl s ps notations fs) () in
   let sign = structure_signature (fields@params) in
   let gr = match kind with
   | Class def ->