Merge PR #6274: Attempt to fix inversion disregarding singleton types (fixes #3125)

5 files changed, 59 insertions, 27 deletions

diff --git a/API/API.mli b/API/API.mli
index 1a84600ec..2eb7c4736 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -3712,7 +3712,7 @@ end
 module Retyping :  (* reconstruct the type of a term knowing that it was already typechecked *)
 sig
   val get_type_of : ?polyprop:bool -> ?lax:bool -> Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.types
-  val get_sort_family_of : ?polyprop:bool -> Environ.env -> Evd.evar_map -> EConstr.types -> Sorts.family
+  val get_sort_family_of : ?truncation_style:bool -> ?polyprop:bool -> Environ.env -> Evd.evar_map -> EConstr.types -> Sorts.family
   val expand_projection : Environ.env -> Evd.evar_map -> Names.Projection.t -> EConstr.constr -> EConstr.constr list -> EConstr.constr
   val get_sort_of :
     ?polyprop:bool -> Environ.env -> Evd.evar_map -> EConstr.types -> Sorts.t
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 5dd6879d3..f8f086fad 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -166,23 +166,6 @@ let retype ?(polyprop=true) sigma =
     | Lambda _ | Fix _ | Construct _ -> retype_error NotAType
     | _ -> decomp_sort env sigma (type_of env t)
 
-  and sort_family_of env t =
-    match EConstr.kind sigma t with
-    | Cast (c,_, s) when isSort sigma s -> Sorts.family (destSort sigma s)
-    | Sort _ -> InType
-    | Prod (name,t,c2) ->
-	let s2 = sort_family_of (push_rel (LocalAssum (name,t)) env) c2 in
-	if not (is_impredicative_set env) &&
-	   s2 == InSet && sort_family_of env t == InType then InType else s2
-    | App(f,args) when is_template_polymorphic env sigma f ->
-	let t = type_of_global_reference_knowing_parameters env f args in
-        Sorts.family (sort_of_atomic_type env sigma t args)
-    | App(f,args) ->
-	Sorts.family (sort_of_atomic_type env sigma (type_of env f) args)
-    | Lambda _ | Fix _ | Construct _ -> retype_error NotAType
-    | _ -> 
-      Sorts.family (decomp_sort env sigma (type_of env t))
-
   and type_of_global_reference_knowing_parameters env c args =
     let argtyps =
       Array.map (fun c -> lazy (EConstr.to_constr sigma (type_of env c))) args in
@@ -198,15 +181,34 @@ let retype ?(polyprop=true) sigma =
       EConstr.of_constr (type_of_constructor env (cstr, u))
     | _ -> assert false
 
-  in type_of, sort_of, sort_family_of,
-     type_of_global_reference_knowing_parameters
+  in type_of, sort_of, type_of_global_reference_knowing_parameters
+
+let get_sort_family_of ?(truncation_style=false) ?(polyprop=true) env sigma t =
+  let type_of,_,type_of_global_reference_knowing_parameters = retype ~polyprop sigma in
+  let rec sort_family_of env t =
+    match EConstr.kind sigma t with
+    | Cast (c,_, s) when isSort sigma s -> Sorts.family (destSort sigma s)
+    | Sort _ -> InType
+    | Prod (name,t,c2) ->
+	let s2 = sort_family_of (push_rel (LocalAssum (name,t)) env) c2 in
+	if not (is_impredicative_set env) &&
+	   s2 == InSet && sort_family_of env t == InType then InType else s2
+    | App(f,args) when is_template_polymorphic env sigma f ->
+        if truncation_style then InType else
+	let t = type_of_global_reference_knowing_parameters env f args in
+        Sorts.family (sort_of_atomic_type env sigma t args)
+    | App(f,args) ->
+	Sorts.family (sort_of_atomic_type env sigma (type_of env f) args)
+    | Lambda _ | Fix _ | Construct _ -> retype_error NotAType
+    | Ind _ when truncation_style && is_template_polymorphic env sigma t -> InType
+    | _ -> 
+      Sorts.family (decomp_sort env sigma (type_of env t))
+  in sort_family_of env t
 
 let get_sort_of ?(polyprop=true) env sigma t =
-  let _,f,_,_ = retype ~polyprop sigma in anomaly_on_error (f env) t
-let get_sort_family_of ?(polyprop=true) env sigma c =
-  let _,_,f,_ = retype ~polyprop sigma in anomaly_on_error (f env) c
+  let _,f,_ = retype ~polyprop sigma in anomaly_on_error (f env) t
 let type_of_global_reference_knowing_parameters env sigma c args =
-  let _,_,_,f = retype sigma in anomaly_on_error (f env c) args
+  let _,_,f = retype sigma in anomaly_on_error (f env c) args
 
 let type_of_global_reference_knowing_conclusion env sigma c conclty =
   match EConstr.kind sigma c with
@@ -232,7 +234,7 @@ let type_of_global_reference_knowing_conclusion env sigma c conclty =
 (*   get_type_of polyprop lax env sigma c *)
 
 let get_type_of ?(polyprop=true) ?(lax=false) env sigma c =
-  let f,_,_,_ = retype ~polyprop sigma in
+  let f,_,_ = retype ~polyprop sigma in
     if lax then f env c else anomaly_on_error (f env) c
 
 (* Makes an unsafe judgment from a constr *)
diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli
index af86df499..6fdde9046 100644
--- a/pretyping/retyping.mli
+++ b/pretyping/retyping.mli
@@ -31,8 +31,11 @@ val get_type_of :
 val get_sort_of :
   ?polyprop:bool -> env -> evar_map -> types -> Sorts.t
 
+(* When [truncation_style] is [true], tells if the type has been explicitly
+   truncated to Prop or (impredicative) Set; in particular, singleton type and
+   small inductive types, which have all eliminations to Type, are in Type *)
 val get_sort_family_of :
-  ?polyprop:bool -> env -> evar_map -> types -> Sorts.family
+  ?truncation_style:bool -> ?polyprop:bool -> env -> evar_map -> types -> Sorts.family
 
 (** Makes an unsafe judgment from a constr *)
 val get_judgment_of : env -> evar_map -> constr -> unsafe_judgment
diff --git a/tactics/equality.ml b/tactics/equality.ml
index c36ad980e..0d6263246 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -739,7 +739,7 @@ let keep_proof_equalities = function
 let find_positions env sigma ~keep_proofs ~no_discr t1 t2 =
   let project env sorts posn t1 t2 =
     let ty1 = get_type_of env sigma t1 in
-    let s = get_sort_family_of env sigma ty1 in
+    let s = get_sort_family_of ~truncation_style:true env sigma ty1 in
     if Sorts.List.mem s sorts
     then [(List.rev posn,t1,t2)] else []
   in
diff --git a/test-suite/bugs/closed/3125.v b/test-suite/bugs/closed/3125.v
new file mode 100644
index 000000000..797146174
--- /dev/null
+++ b/test-suite/bugs/closed/3125.v
@@ -0,0 +1,27 @@
+(* Not considering singleton template-polymorphic inductive types as
+   propositions for injection/inversion *)
+
+(* This is also #4560 and #6273 *)
+
+Inductive foo := foo_1.
+
+Goal forall (a b : foo), Some a = Some b -> a = b.
+Proof.
+  intros a b H.
+  inversion H.
+  reflexivity.
+Qed.
+
+(* Check that Prop is not concerned *)
+
+Inductive bar : Prop := bar_1.
+
+Goal
+  forall (a b : bar),
+    Some a = Some b ->
+    a = b.
+Proof.
+  intros a b H.
+  inversion H.
+  Fail reflexivity.
+Abort.