diff options
| -rw-r--r-- | kernel/indtypes.ml | 15 | ||||
| -rw-r--r-- | test-suite/failure/inductive4.v | 15 |
2 files changed, 27 insertions, 3 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 77fd062bec..46e866a047 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 0000000000..6ba36fd20a --- /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. + |