Make pattern_of_constr typed so that we can infer the proper patterns

for primitive projections, fixing bug #3661. Also fix expand_projection
so that it does enough reduction to find the inductive type of its
argument.

1 files changed, 88 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/3661.v b/test-suite/bugs/closed/3661.v
new file mode 100644
index 000000000..fdca49bc4
--- /dev/null
+++ b/test-suite/bugs/closed/3661.v
@@ -0,0 +1,88 @@
+(* File reduced by coq-bug-finder from original input, then from 11218 lines to 438 lines, then from 434 lines to 202 lines, then from 140 lines to 94 lines *)
+(* coqc version trunk (September 2014) compiled on Sep 25 2014 2:53:46 with OCaml 4.01.0
+   coqtop version cagnode16:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (bec7e0914f4a7144cd4efa8ffaccc9f72dbdb790) *)
+Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a.
+Set Implicit Arguments.
+Delimit Scope morphism_scope with morphism.
+Record PreCategory := { object :> Type ; morphism : object -> object -> Type }.
+Bind Scope category_scope with PreCategory.
+Local Open Scope morphism_scope.
+Record Functor (C D : PreCategory) :=
+  { object_of :> C -> D;
+    morphism_of : forall s d, morphism C s d -> morphism D (object_of s) (object_of d) }.
+Set Primitive Projections.
+Class IsIsomorphism {C : PreCategory} {s d} (m : morphism C s d) := { morphism_inverse : morphism C d s }.
+Record NaturalTransformation C D (F G : Functor C D) := { components_of :> forall c, morphism D (F c) (G c) }.
+Unset Primitive Projections.
+Class Isomorphic {C : PreCategory} s d :=
+  { morphism_isomorphic :> morphism C s d;
+    isisomorphism_isomorphic :> IsIsomorphism morphism_isomorphic }.
+Arguments morphism_inverse {C s d} m {_} / .
+Local Notation "m ^-1" := (morphism_inverse m) (at level 3, format "m '^-1'") : morphism_scope.
+Definition functor_category (C D : PreCategory) : PreCategory.
+  exact (@Build_PreCategory (Functor C D)
+                            (@NaturalTransformation C D)).
+Defined.
+Local Notation "C -> D" := (functor_category C D) : category_scope.
+Generalizable All Variables.
+Definition isisomorphism_components_of `{@IsIsomorphism (C -> D) F G T} x : IsIsomorphism (T x).
+Proof.
+  constructor.
+  exact (T^-1 x).
+Defined.
+Hint Immediate isisomorphism_components_of : typeclass_instances.
+Goal forall (x3 x9 : PreCategory) (x12 f0 : Functor x9 x3)
+            (x35 : @Isomorphic (@functor_category x9 x3) f0 x12)
+            (x37 : object x9)
+            (H3 : morphism x3 (@object_of x9 x3 f0 x37)
+                           (@object_of x9 x3 f0 x37))
+            (x34 : @Isomorphic (@functor_category x9 x3) x12 f0)
+            (m : morphism x3 (x12 x37) (f0 x37) ->
+                 morphism x3 (f0 x37) (x12 x37) ->
+                 morphism x3 (f0 x37) (f0 x37)),
+       @paths
+         (morphism x3 (@object_of x9 x3 f0 x37) (@object_of x9 x3 f0 x37))
+         H3
+         (m
+            (@components_of x9 x3 x12 f0
+                            (@morphism_inverse (@functor_category x9 x3) f0 x12
+                                               (@morphism_isomorphic (@functor_category x9 x3) f0 x12 x35)
+                                               (@isisomorphism_isomorphic (@functor_category x9 x3) f0 x12
+                                                                          x35)) x37)
+            (@components_of x9 x3 f0 x12
+                            (@morphism_inverse (@functor_category x9 x3) x12 f0
+                                               (@morphism_isomorphic (@functor_category x9 x3) x12 f0 x34)
+                                               (@isisomorphism_isomorphic (@functor_category x9 x3) x12 f0
+                                                                          x34)) x37)).
+  Unset Printing All.
+  intros.
+  match goal with
+    | [ |- context[components_of ?T^-1 ?x] ]
+      => progress let T1 := constr:(T^-1 x) in
+                  let T2 := constr:((T x)^-1) in
+                  change T1 with T2 || fail 1 "too early"
+  end.
+
+  Undo.
+
+  match goal with
+    | [ |- context[components_of ?T^-1 ?x] ]
+      => progress let T1 := constr:(T^-1 x) in
+                  change T1 with ((T x)^-1) || fail 1 "too early 2"
+  end.
+
+  Undo.
+
+  match goal with
+    | [ |- context[components_of ?T^-1 ?x] ]
+      => progress let T2 := constr:((T x)^-1) in
+                  change (T^-1 x) with T2
+  end. (* not convertible *)
+
+(*
+
+  (@components_of x9 x3 x12 f0
+     (@morphism_inverse _ _ _
+        (@morphism_isomorphic (functor_category x9 x3) f0 x12 x35) _) x37)
+
+*)
\ No newline at end of file