3 files changed, 20 insertions, 2 deletions
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 979240663b..455965af42 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -34,9 +34,17 @@ let current_fixpoints = ref ([] : constant list)
 
 let none = Evd.empty
 
-let type_of env c = Retyping.get_type_of env none (strip_outer_cast c)
+let type_of env c =
+  try
+    let polyprop = (lang() = Haskell) in
+    Retyping.get_type_of ~polyprop env none (strip_outer_cast c)
+  with SingletonInductiveBecomesProp id -> error_singleton_become_prop id
 
-let sort_of env c = Retyping.get_sort_family_of env none (strip_outer_cast c)
+let sort_of env c =
+  try
+    let polyprop = (lang() = Haskell) in
+    Retyping.get_sort_family_of ~polyprop env none (strip_outer_cast c)
+  with SingletonInductiveBecomesProp id -> error_singleton_become_prop id
 
 (*S Generation of flags and signatures. *)
 
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index ad5424deb1..aa312321b6 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -334,6 +334,15 @@ let error_no_module_expr mp =
        ++ str "some Declare Module outside any Module Type.\n"
        ++ str "This situation is currently unsupported by the extraction.")
 
+let error_singleton_become_prop id =
+  err (str "The informative inductive type " ++ pr_id id ++
+       str " has a Prop instance.\n" ++
+       str "This happens when a sort-polymorphic singleton inductive type\n" ++
+       str "has logical parameters, such as (I,I) : (True * True) : Prop.\n" ++
+       str "The Ocaml extraction cannot handle this situation yet.\n" ++
+       str "Instead, use a sort-monomorphic type such as (True /\\ True)\n" ++
+       str "or extract to Haskell.")
+
 let error_unknown_module m =
   err (str "Module" ++ spc () ++ pr_qualid m ++ spc () ++ str "not found.")
 
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index ce57a78407..d656edfb74 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -29,6 +29,7 @@ val error_inductive : global_reference -> 'a
 val error_nb_cons : unit -> 'a
 val error_module_clash : module_path -> module_path -> 'a
 val error_no_module_expr : module_path -> 'a
+val error_singleton_become_prop : identifier -> 'a
 val error_unknown_module : qualid -> 'a
 val error_scheme : unit -> 'a
 val error_not_visible : global_reference -> 'a