Handle inversion of homogenous products in reflective type inversion

1 files changed, 16 insertions, 1 deletions

diff --git a/src/Reflection/TypeInversion.v b/src/Reflection/TypeInversion.v
index 7d0999061..2138a3788 100644
--- a/src/Reflection/TypeInversion.v
+++ b/src/Reflection/TypeInversion.v
@@ -13,7 +13,9 @@ Section language.
       match goal with
       | [ p : _ |- _ ] => specialize (H _ p)
       end;
-      assumption.
+      cbv beta iota in *;
+      try specialize (H eq_refl); simpl in *;
+      try assumption.
 
     Definition preinvert_Tbase (Q : forall t, P (Tbase t) -> Type)
       : (forall t (p : P t), match t return P t -> Type with Tbase _ => Q _ | _ => fun _ => True end p)
@@ -35,6 +37,15 @@ Section language.
         -> forall A B p, Q A B p.
     Proof. t. Defined.
 
+    Definition preinvert_Prod2_same (Q : forall A, P (Prod (Tbase A) (Tbase A)) -> Type)
+      : (forall t (p : P t), match t return P t -> Type with
+                             | Prod (Tbase A) (Tbase B)
+                               => fun p => forall pf : A = B, Q B (eq_rect _ (fun a => P (Prod (Tbase a) (Tbase B))) p _ pf)
+                             | _ => fun _ => True
+                             end p)
+        -> forall A p, Q A p.
+    Proof. t. Defined.
+
     Definition preinvert_Prod3 (Q : forall A B C, P (Tbase A * Tbase B * Tbase C)%ctype -> Type)
       : (forall t (p : P t), match t return P t -> Type with Prod (Prod (Tbase _) (Tbase _)) (Tbase _) => Q _ _ _ | _ => fun _ => True end p)
         -> forall A B C p, Q A B C p.
@@ -108,6 +119,10 @@ Ltac preinvert_one_type e :=
        move e at top;
        revert dependent T;
        refine (preinvert_Tbase P _ _)
+  | ?P (Prod (Tbase ?A) (Tbase ?A))
+    => is_var A;
+       move e at top; revert dependent A;
+       refine (preinvert_Prod2_same P _ _)
   | ?P (Prod (Tbase ?A) (Tbase ?B))
     => is_var A; is_var B;
        move e at top; revert dependent A; intros A e;