Merge PR#787: [typeclasses eauto] Fix bug #3943: non-termination in topological

1 files changed, 50 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/3943.v b/test-suite/bugs/closed/3943.v
new file mode 100644
index 000000000..5e5ba816f
--- /dev/null
+++ b/test-suite/bugs/closed/3943.v
@@ -0,0 +1,50 @@
+(* File reduced by coq-bug-finder from original input, then from 9492 lines to 119 lines *)
+(* coqc version 8.5beta1 (January 2015) compiled on Jan 18 2015 7:27:36 with OCaml 3.12.1
+   coqtop version 8.5beta1 (January 2015) *)
+
+Set Typeclasses Dependency Order.
+
+Inductive paths {A : Type} (a : A) : A -> Type :=
+  idpath : paths a a.
+Arguments idpath {A a} , [A] a.
+Notation "x = y" := (@paths _ x y) : type_scope.
+Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y
+  := match p with idpath => idpath end.
+
+Set Implicit Arguments.
+Delimit Scope morphism_scope with morphism.
+Delimit Scope category_scope with category.
+Delimit Scope object_scope with object.
+
+Record PreCategory := Build_PreCategory' {
+      object :> Type;
+      morphism : object -> object -> Type;
+      identity : forall x, morphism x x;
+      compose : forall s d d',
+                  morphism d d'
+                  -> morphism s d
+                  -> morphism s d' }.
+Arguments identity {!C%category} / x%object : rename.
+Arguments compose {!C%category} / {s d d'}%object (m1 m2)%morphism : rename.
+
+Class IsIsomorphism {C : PreCategory} {s d} (m : morphism C s d) := {
+    morphism_inverse : morphism C d s;
+    left_inverse : compose morphism_inverse m = identity _;
+    right_inverse : compose m morphism_inverse = identity _ }.
+Arguments morphism_inverse {C s d} m {_}.
+Local Notation "m ^-1" := (morphism_inverse m) (at level 3, format "m '^-1'") : morphism_scope.
+
+Class Isomorphic {C : PreCategory} s d := {
+    morphism_isomorphic :> morphism C s d;
+    isisomorphism_isomorphic :> IsIsomorphism morphism_isomorphic }.
+Coercion morphism_isomorphic : Isomorphic >-> morphism.
+
+Variable C : PreCategory.
+Variables s d : C.
+
+Definition path_isomorphic (i j : Isomorphic s d)
+: @morphism_isomorphic _ _ _ i = @morphism_isomorphic _ _ _ j -> i = j.
+Admitted.
+
+Definition ap_morphism_inverse_path_isomorphic (i j : Isomorphic s d) p q
+: ap (fun e : Isomorphic s d => e^-1)%morphism (path_isomorphic i j p) = q.
\ No newline at end of file