Add a regression test for 3427

1 files changed, 195 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/3427.v b/test-suite/bugs/closed/3427.v
new file mode 100644
index 000000000..8483a4ecf
--- /dev/null
+++ b/test-suite/bugs/closed/3427.v
@@ -0,0 +1,195 @@
+(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *)
+(* File reduced by coq-bug-finder from original input, then from 0 lines to 7171 lines, then from 7184 lines to 558 lines, then from 556 lines to 209 lines *)
+Generalizable All Variables.
+Set Universe Polymorphism.
+Notation Type0 := Set.
+Notation idmap := (fun x => x).
+Definition compose {A B C : Type} (g : B -> C) (f : A -> B) := fun x => g (f x).
+Notation "g 'o' f" := (compose g f) (at level 40, left associativity) : function_scope.
+Open Scope function_scope.
+Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y) : type_scope.
+Arguments idpath {A a} , [A] a.
+Delimit Scope path_scope with path.
+Local Open Scope path_scope.
+Definition concat {A : Type} {x y z : A} (p : x = y) (q : y = z) : x = z := match p, q with idpath, idpath => idpath end.
+Definition inverse {A : Type} {x y : A} (p : x = y) : y = x := match p with idpath => idpath end.
+Notation "1" := idpath : path_scope.
+Notation "p @ q" := (concat p q) (at level 20) : path_scope.
+Notation "p ^" := (inverse p) (at level 3) : path_scope.
+Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) : P y := match p with idpath => u end.
+Notation "p # x" := (transport _ p x) (right associativity, at level 65, only parsing) : path_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.
+Definition pointwise_paths {A} {P:A->Type} (f g:forall x:A, P x) := forall x:A, f x = g x.
+Notation "f == g" := (pointwise_paths f g) (at level 70, no associativity) : type_scope.
+Definition apD10 {A} {B:A->Type} {f g : forall x, B x} (h:f=g) : forall x, f x = g x := fun x => match h with idpath => idpath end.
+Definition Sect {A B : Type} (s : A -> B) (r : B -> A) := forall x : A, r (s x) = x.
+Class IsEquiv {A B : Type} (f : A -> B) := BuildIsEquiv {
+                                               equiv_inv : B -> A ;
+                                               eisretr : Sect equiv_inv f;
+                                               eissect : Sect f equiv_inv;
+                                               eisadj : forall x : A, eisretr (f x) = ap f (eissect x)
+                                             }.
+Record Equiv A B := BuildEquiv {
+                        equiv_fun :> A -> B ;
+                        equiv_isequiv :> IsEquiv equiv_fun
+                      }.
+
+Delimit Scope equiv_scope with equiv.
+
+Notation "A <~> B" := (Equiv A B) (at level 85) : equiv_scope.
+
+Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3) : equiv_scope.
+
+Class Contr_internal (A : Type) := BuildContr {
+                                       center : A ;
+                                       contr : (forall y : A, center = y)
+                                     }.
+
+Inductive trunc_index : Type :=
+| minus_two : trunc_index
+| trunc_S : trunc_index -> trunc_index.
+
+Fixpoint nat_to_trunc_index (n : nat) : trunc_index
+  := match n with
+       | 0 => trunc_S (trunc_S minus_two)
+       | S n' => trunc_S (nat_to_trunc_index n')
+     end.
+
+Coercion nat_to_trunc_index : nat >-> trunc_index.
+
+Fixpoint IsTrunc_internal (n : trunc_index) (A : Type) : Type :=
+  match n with
+    | minus_two => Contr_internal A
+    | trunc_S n' => forall (x y : A), IsTrunc_internal n' (x = y)
+  end.
+
+Notation minus_one:=(trunc_S minus_two).
+
+Class IsTrunc (n : trunc_index) (A : Type) : Type :=
+  Trunc_is_trunc : IsTrunc_internal n A.
+
+Notation Contr := (IsTrunc minus_two).
+Notation IsHProp := (IsTrunc minus_one).
+Notation IsHSet := (IsTrunc 0).
+
+Class Funext :=
+  { isequiv_apD10 :> forall (A : Type) (P : A -> Type) f g, IsEquiv (@apD10 A P f g) }.
+
+Definition concat_pV {A : Type} {x y : A} (p : x = y) :
+  p @ p^ = 1
+  :=
+    match p with idpath => 1 end.
+
+Definition concat_Vp {A : Type} {x y : A} (p : x = y) :
+  p^ @ p = 1
+  :=
+    match p with idpath => 1 end.
+
+Definition transport_pp {A : Type} (P : A -> Type) {x y z : A} (p : x = y) (q : y = z) (u : P x) :
+  p @ q # u = q # p # u :=
+  match q with idpath =>
+               match p with idpath => 1 end
+  end.
+
+Definition transport2 {A : Type} (P : A -> Type) {x y : A} {p q : x = y}
+           (r : p = q) (z : P x)
+: p # z = q # z
+  := ap (fun p' => p' # z) r.
+
+Inductive Unit : Type0 :=
+  tt : Unit.
+
+Instance contr_unit : Contr Unit | 0 := let x := {|
+                                              center := tt;
+                                              contr := fun t : Unit => match t with tt => 1 end
+                                            |} in x.
+
+Instance trunc_succ `{IsTrunc n A} : IsTrunc (trunc_S n) A | 1000.
+admit.
+Defined.
+
+Record hProp := hp { hproptype :> Type ; isp : IsHProp hproptype}.
+Definition Unit_hp:hProp:=(hp Unit _).
+
+Global Instance isequiv_ap_hproptype `{Funext} X Y : IsEquiv (@ap _ _ hproptype X Y).
+admit.
+Defined.
+
+Definition path_hprop `{Funext} X Y := (@ap _ _ hproptype X Y)^-1%equiv.
+
+Record hSet := BuildhSet {setT:> Type; iss :> IsHSet setT}.
+Local Open Scope equiv_scope.
+
+Instance isequiv_path {A B : Type} (p : A = B)
+: IsEquiv (transport (fun X:Type => X) p) | 0
+  := BuildIsEquiv _ _ _ (transport (fun X:Type => X) p^)
+                  (fun b => ((transport_pp idmap p^ p b)^ @ transport2 idmap (concat_Vp p) b))
+                  (fun a => ((transport_pp idmap p p^ a)^ @ transport2 idmap (concat_pV p) a))
+                  (fun a => match p in _ = C return
+                                  (transport_pp idmap p^ p (transport idmap p a))^ @
+                                                                                     transport2 idmap (concat_Vp p) (transport idmap p a) =
+                                  ap (transport idmap p) ((transport_pp idmap p p^ a) ^ @
+                                                                                          transport2 idmap (concat_pV p) a) with idpath => 1 end).
+
+Definition equiv_path (A B : Type) (p : A = B) : A <~> B
+  := BuildEquiv _ _ (transport (fun X:Type => X) p) _.
+
+Class Univalence := {
+                     isequiv_equiv_path :> forall (A B : Type), IsEquiv (equiv_path A B)
+                   }.
+
+Section Univalence.
+  Context `{Univalence}.
+
+  Definition path_universe_uncurried {A B : Type} (f : A <~> B) : A = B
+    := (equiv_path A B)^-1 f.
+End Univalence.
+
+Local Inductive minus1Trunc (A :Type) : Type :=
+  min1 : A -> minus1Trunc A.
+
+Instance minus1Trunc_is_prop {A : Type} : IsHProp (minus1Trunc A) | 0.
+admit.
+Defined.
+
+Definition hexists {X} (P:X->Type):Type:= minus1Trunc (sigT  P).
+
+Section AssumingUA.
+
+  Definition isepi {X Y} `(f:X->Y) := forall Z: hSet,
+                                      forall g h: Y -> Z, g o f = h o f -> g = h.
+  Context {X Y : hSet} (f : X -> Y) (Hisepi : isepi f).
+
+  Goal forall (X Y : hSet) (f : forall _ : setT X, setT Y),
+         let fib :=
+             fun y : setT Y =>
+               hp (@hexists (setT X) (fun x : setT X => @paths (setT Y) (f x) y))
+                  (@minus1Trunc_is_prop
+                     (@sigT (setT X) (fun x : setT X => @paths (setT Y) (f x) y))) in
+         forall (x : setT X) (_ : Univalence) (_ : Funext),
+           @paths hProp (fib (f x)) Unit_hp.
+  intros.
+
+  apply path_hprop.
+  simpl.
+  Set Printing Universes.
+  Set Printing All.
+  refine (path_universe_uncurried _).
+  Undo.
+  apply path_universe_uncurried. (* Toplevel input, characters 21-44:
+Error: Refiner was given an argument
+ "@path_universe_uncurried (* Top.425 Top.426 Top.427 Top.428 Top.429 *) X1
+    (@hexists (* Top.405 Top.404 Set Set *) (setT (* Top.405 *) X0)
+       (fun x0 : setT (* Top.405 *) X0 =>
+        @paths (* Top.404 *) (setT (* Top.404 *) Y0) (f0 x0) (f0 x))) Unit
+    ?63" of type
+ "@paths (* Top.428 *) Type (* Top.425 *)
+    (@hexists (* Top.405 Top.404 Set Set *) (setT (* Top.405 *) X0)
+       (fun x0 : setT (* Top.405 *) X0 =>
+        @paths (* Top.404 *) (setT (* Top.404 *) Y0) (f0 x0) (f0 x))) Unit"
+instead of
+ "@paths (* Top.413 *) Type (* Set *)
+    (@hexists (* Top.405 Top.404 Set Set *) (setT (* Top.405 *) X0)
+       (fun x0 : setT (* Top.405 *) X0 =>
+        @paths (* Top.404 *) (setT (* Top.404 *) Y0) (f0 x0) (f0 x))) Unit".
+ *)