From ca630605330828b9b6456477b0fd4f8a0c3f1831 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 21 May 2017 22:23:24 +0200
Subject: More precise on preventing clash between bound vars name and hidden
 impargs.

We want to avoid capture in "Inductive I {A} := C : forall A, I".
But in "Record I {A} := { C : forall A, A }.", non recursivity ensures
that no clash will occur.

This fixes previous commit, with which it could possibly be merged.
---
 interp/constrintern.ml      | 8 ++++----
 interp/constrintern.mli     | 2 +-
 test-suite/success/Record.v | 5 +++++
 vernac/command.ml           | 2 +-
 vernac/record.ml            | 7 ++++---
 5 files changed, 15 insertions(+), 9 deletions(-)

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 3dfc850410..ce51f21c7b 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
@@ -358,12 +358,12 @@ 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 =
   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 " ++
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index f3306b5929..8a759a8033 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
diff --git a/test-suite/success/Record.v b/test-suite/success/Record.v
index 8334322c99..6f27c1d369 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/vernac/command.ml b/vernac/command.ml
index 02d8525158..0064af77d2 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -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 ~impls (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 a220e515e7..88f4586800 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -94,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
@@ -139,7 +139,8 @@ let typecheck_params_and_fields def id pl t ps nots fs =
   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 impls_env = compute_internalization_env env0 ~impls:impls_env (Inductive params) [id] [EConstr.to_constr !evars arity] [imps] 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
@@ -563,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 ->
-- 
cgit v1.2.3