Extraction: forbid Prop-polymorphism of inductives when extracting to Ocaml

 A particular case in sort-polymorphism of inductive types allows
 an informative type (such as prod) to have instances in Prop:

   (I,I) : True * True : Prop

 This is due to the fact that prod is a singleton type: indeed (I,I)
 has no informative content. But this invalidates an important invariant
 for the correctness of the extraction: inductive constructors stop
 having always the same sort as their inductive type. Consider for instance:

  Definition f (X:Type)(x:X*X)(g:X->nat) := g (fst x).
  Definition test := f _ (I,I) (fun _ => 0).

 Then the inductive element (I,I) is extracted as a logical part __,
 but during a strict evaluation (i.e. in Ocaml, not Haskell), this __
 will be given to fst, and hence to a match, leading to a nasty result
 (potentially segfault). Haskell is not affected, since fst is never
 evaluated.

 This patch adds a check for this situation during any Ocaml extraction,
 leading for the moment to a fatal error. Some functions in inductive.ml
 and retyping.ml now have an extra optional argument ?(polyprop=true)
 that should stay untouched in regular Coq usage, while type-checking
 done during extraction will disable this prop-polymorphism.

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

2 files changed, 20 insertions, 9 deletions

diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 62cd844d83..502e238b30 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -42,7 +42,7 @@ let type_of_var env id =
   with Not_found ->
     anomaly ("type_of: variable "^(string_of_id id)^" unbound")
 
-let retype sigma =
+let retype ?(polyprop=true) sigma =
   let rec type_of env cstr=
     match kind_of_term cstr with
     | Meta n ->
@@ -127,7 +127,8 @@ let retype sigma =
     match kind_of_term c with
     | Ind ind ->
       let (_,mip) = lookup_mind_specif env ind in
-	(try Inductive.type_of_inductive_knowing_parameters env mip argtyps
+	(try Inductive.type_of_inductive_knowing_parameters
+	       ~polyprop env mip argtyps
 	 with Reduction.NotArity -> anomaly "type_of: Not an arity")
     | Const cst ->
       let t = constant_type env cst in
@@ -140,8 +141,10 @@ let retype sigma =
   in type_of, sort_of, sort_family_of,
      type_of_global_reference_knowing_parameters
 
-let get_sort_of env sigma t = let _,f,_,_ = retype sigma in f env t
-let get_sort_family_of env sigma c = let _,_,f,_ = retype sigma in f env c
+let get_sort_of ?(polyprop=true) env sigma t =
+  let _,f,_,_ = retype ~polyprop sigma in f env t
+let get_sort_family_of ?(polyprop=true) env sigma c =
+  let _,_,f,_ = retype ~polyprop sigma in f env c
 let type_of_global_reference_knowing_parameters env sigma c args =
   let _,_,_,f = retype sigma in f env c args
 
@@ -161,8 +164,8 @@ let type_of_global_reference_knowing_conclusion env sigma c conclty =
 
 (* We are outside the kernel: we take fresh universes *)
 (* to avoid tactics and co to refresh universes themselves *)
-let get_type_of ?(refresh=true) env sigma c =
-  let f,_,_,_ = retype sigma in
+let get_type_of ?(polyprop=true) ?(refresh=true) env sigma c =
+  let f,_,_,_ = retype ~polyprop sigma in
   let t = f env c in
     if refresh then refresh_universes t else t
 
diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli
index c0d6336ccc..445f623a41 100644
--- a/pretyping/retyping.mli
+++ b/pretyping/retyping.mli
@@ -17,9 +17,17 @@ open Environ
    either produces a wrong result or raise an anomaly. Use with care.
    It doesn't handle predicative universes too. *)
 
-val get_type_of : ?refresh:bool -> env -> evar_map -> constr -> types
-val get_sort_of : env -> evar_map -> types -> sorts
-val get_sort_family_of : env -> evar_map -> types -> sorts_family
+(** The "polyprop" optional argument is used by the extraction to
+    disable "Prop-polymorphism", cf comment in [inductive.ml] *)
+
+val get_type_of :
+  ?polyprop:bool -> ?refresh:bool -> env -> evar_map -> constr -> types
+
+val get_sort_of :
+  ?polyprop:bool -> env -> evar_map -> types -> sorts
+
+val get_sort_family_of :
+  ?polyprop:bool -> env -> evar_map -> types -> sorts_family
 
 (** Makes an assumption from a constr *)
 val get_assumption_of : env -> evar_map -> constr -> types