Fixing critical inductive polymorphism bug found by Bruno.

If two distinct parameters of the inductive type contributes to
polymorphism, they must have distinct names, othewise an aliasing
problem of the form "fun x x => max(x,x)" happens.

Also insisted that a parameter contributes to universe polymorphism
only if the corresponding occurrence of Type is not hidden behind a
definition.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14511 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 27 insertions, 3 deletions

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 77fd062be..46e866a04 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -235,9 +235,18 @@ let typecheck_inductive env mie =
   let arities = Array.of_list arity_list in
   let param_ccls = List.fold_left (fun l (_,b,p) ->
     if b = None then
-      let _,c = dest_prod_assum env p in
-      let u = match kind_of_term c with Sort (Type u) -> Some u | _ -> None in
-      u::l
+      (* Parameter contributes to polymorphism only if explicit Type *)
+      let c = strip_prod_assum p in
+      (* Add Type levels to the ordered list of parameters contributing to *)
+      (* polymorphism unless there is aliasing (i.e. non distinct levels) *)
+      match kind_of_term c with
+      | Sort (Type u) ->
+          if List.mem (Some u) l then
+            None :: List.map (function Some v when u = v -> None | x -> x) l
+          else
+            Some u :: l
+      | _ ->
+          None :: l
     else
       l) [] params in
 
diff --git a/test-suite/failure/inductive4.v b/test-suite/failure/inductive4.v
new file mode 100644
index 000000000..6ba36fd20
--- /dev/null
+++ b/test-suite/failure/inductive4.v
@@ -0,0 +1,15 @@
+(* This used to succeed in versions 8.1 to 8.3 *)
+
+Require Import Logic.
+Require Hurkens.
+Definition Ti := Type.
+Inductive prod (X Y:Ti) := pair : X -> Y -> prod X Y.
+Definition B : Prop := let F := prod True in F Prop. (* Aie! *)
+Definition p2b (P:Prop) : B := pair True Prop I P.
+Definition b2p (b:B) : Prop := match b with pair _ P => P end.
+Lemma L1 : forall A : Prop, b2p (p2b A) -> A.
+Proof (fun A x => x).
+Lemma L2 : forall A : Prop, A -> b2p (p2b A).
+Proof (fun A x => x).
+Check Hurkens.paradox B p2b b2p L1 L2.
+