diff options
author | 2011-10-05 15:51:57 +0000 | |
---|---|---|
committer | 2011-10-05 15:51:57 +0000 | |
commit | 8082d1faf85a0ab29f6c144a137791902a4e9c1f (patch) | |
tree | 431f9fc4fe167e77c6be5163db41314ecd872ba6 /kernel | |
parent | b82f23627766b39ca0343ac41b061a5ce76c18f2 (diff) |
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
Diffstat (limited to 'kernel')
-rw-r--r-- | kernel/indtypes.ml | 15 |
1 files changed, 12 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 |