Fix canonical structure resolution which was launched on the results of

eta-expansion, creating a loop. This is now deactivated. Fixes bugs #3665 and #3667.

2 files changed, 58 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/3665.v b/test-suite/bugs/closed/3665.v
new file mode 100644
index 000000000..f6a13596c
--- /dev/null
+++ b/test-suite/bugs/closed/3665.v
@@ -0,0 +1,33 @@
+(* File reduced by coq-bug-finder from original input, then from 5449 lines to 44 lines *)
+(* coqc version trunk (September 2014) compiled on Sep 25 2014 2:53:46 with OCaml 4.01.0
+   coqtop version trunk (September 2014) *)
+Set Primitive Projections.
+
+Axiom IsHSet : Type -> Type.
+Record hSet := BuildhSet {setT:> Type; iss :> IsHSet setT}.
+
+Module withdefault.
+Canonical Structure default_HSet := fun T P => (@BuildhSet T P).
+Goal forall (z : hSet) (T0 : Type -> Type),
+       (forall (A : Type) (P : T0 A -> Type) (aa : T0 A), P aa) ->
+       forall x0 : setT z, Set.
+  clear; intros z T H.
+  Set Debug Unification.
+  Fail refine (H _ _). (* Timeout! *)
+Abort.
+End withdefault.
+
+Module withnondefault.
+Variable T0 : Type -> Type.
+Variable T0hset: forall A, IsHSet (T0 A).
+
+Canonical Structure nondefault_HSet := fun A =>(@BuildhSet (T0 A) (T0hset A)).
+Canonical Structure default_HSet := fun A P =>(@BuildhSet A P).
+Goal forall (z : hSet) (T0 : Type -> Type),
+       (forall (A : Type) (P : T0 A -> Type) (aa : T0 A), P aa) ->
+       forall x0 : setT z, Set.
+  clear; intros z T H.
+  Set Debug Unification.
+  Fail refine (H _ _). (* Timeout! *)
+Abort.
+End withnondefault.
diff --git a/test-suite/bugs/closed/3667.v b/test-suite/bugs/closed/3667.v
new file mode 100644
index 000000000..e0d0e4486
--- /dev/null
+++ b/test-suite/bugs/closed/3667.v
@@ -0,0 +1,25 @@
+
+Set Primitive Projections.
+Axiom ap10 : forall {A B} {f g:A->B} (h:f=g) x, f x = g x.
+Axiom IsHSet : Type -> Type.
+Record hSet := BuildhSet {setT:> Type; iss :> IsHSet setT}.
+Canonical Structure default_HSet:= fun T P => (@BuildhSet T P).
+Record PreCategory := { object :> Type ; morphism : object -> object -> Type }.
+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 Implicit Arguments.
+Record NaturalTransformation C D (F G : Functor C D) :=
+  { components_of :> forall c, morphism D (F c) (G c);
+    commutes : forall s d (m : morphism C s d), components_of s = components_of s }.
+Definition set_cat : PreCategory.
+  exact ((@Build_PreCategory hSet
+                             (fun x y => x -> y))).
+Defined.
+Goal forall (A : PreCategory) (F : Functor A set_cat)
+            (a : A) (x : F a), x = x.
+  intros. 
+  pose (fun c d m => ap10 (commutes x c d m)).
+
+