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

1 files changed, 8 insertions, 1 deletions

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 07195c493f..aeeefbfa42 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -178,13 +178,20 @@ let instantiate_universes env ctx ar argsorts =
   (* This is a Type with constraints *)
  else Type level
 
-let type_of_inductive_knowing_parameters env mip paramtyps =
+exception SingletonInductiveBecomesProp of identifier
+
+let type_of_inductive_knowing_parameters ?(polyprop=true) env mip paramtyps =
   match mip.mind_arity with
   | Monomorphic s ->
       s.mind_user_arity
   | Polymorphic ar ->
       let ctx = List.rev mip.mind_arity_ctxt in
       let ctx,s = instantiate_universes env ctx ar paramtyps in
+      (* The Ocaml extraction cannot handle (yet?) "Prop-polymorphism", i.e.
+         the situation where a non-Prop singleton inductive becomes Prop
+         when applied to Prop params *)
+      if not polyprop && not (is_type0m_univ ar.poly_level) && s = prop_sort
+      then raise (SingletonInductiveBecomesProp mip.mind_typename);
       mkArity (List.rev ctx,s)
 
 (* Type of a (non applied) inductive type *)