Fix test-suite file 3352 which was containing the wrong test.

1 files changed, 33 insertions, 114 deletions

diff --git a/test-suite/bugs/closed/3352.v b/test-suite/bugs/closed/3352.v
index bab197ed0..b57b0a0f0 100644
--- a/test-suite/bugs/closed/3352.v
+++ b/test-suite/bugs/closed/3352.v
@@ -1,115 +1,34 @@
-Require Coq.Vectors.Fin.
-Require Coq.Vectors.Vector.
 
-Local Generalizable All Variables.
-Set Implicit Arguments.
-
-Arguments Fin.F1 : clear implicits.
-
-Lemma fin_0_absurd : notT (Fin.t 0).
-Proof. hnf. apply Fin.case0. Qed.
-
-Fixpoint lower {n:nat} (p:Fin.t (S n)) {struct p} :
-  forall (i:Fin.t (S n)), option (Fin.t n)
-  := match p in Fin.t (S n1)
-           return Fin.t (S n1) -> option (Fin.t n1)
-     with
-       | @Fin.F1 n1 =>
-         fun (i:Fin.t (S n1)) =>
-           match i in Fin.t (S n2) return option (Fin.t n2) with
-             | @Fin.F1 n2 => None
-             | @Fin.FS n2 i2 => Some i2
-           end
-       | @Fin.FS n1 p1 =>
-         fun (i:Fin.t (S n1)) =>
-           match i in Fin.t (S n2) return Fin.t n2 -> option (Fin.t n2) with
-             | @Fin.F1 n2 =>
-               match n2 as n3 return Fin.t n3 -> option (Fin.t n3) with
-                 | 0 => fun p2 => False_rect _ (fin_0_absurd p2)
-                 | S n3 => fun p2 => Some (Fin.F1 n3)
-               end
-             | @Fin.FS n2 i2 =>
-               match n2 as n3 return Fin.t n3 -> Fin.t n3 -> option (Fin.t n3) with
-                 | 0 => fun i3 p3 => False_rect _ (fin_0_absurd p3)
-                 | S n3 => fun (i3 p3:Fin.t (S n3)) =>
-                             option_map (@Fin.FS _) (lower p3 i3)
-               end i2
-           end p1
-     end.
-
-Lemma lower_ind (P: forall n (p i:Fin.t (S n)), option (Fin.t n) -> Prop)
-      (c11 : forall n, P n (Fin.F1 n) (Fin.F1 n) None)
-      (c1S : forall n (i:Fin.t n), P n (Fin.F1 n) (Fin.FS i) (Some i))
-      (cS1 : forall n (p:Fin.t (S n)),
-               P (S n) (Fin.FS p) (Fin.F1 (S n)) (Some (Fin.F1 n)))
-      (cSSS : forall n (p i:Fin.t (S n)) (i':Fin.t n)
-                     (Elow:lower p i = Some i'),
-                P n p i (Some i') ->
-                P (S n) (Fin.FS p) (Fin.FS i) (Some (Fin.FS i')))
-      (cSSN : forall n (p i:Fin.t (S n))
-                (Elow:lower p i = None),
-                P n p i None ->
-                P (S n) (Fin.FS p) (Fin.FS i) None) :
-  forall n (p i:Fin.t (S n)), P n p i (lower p i).
-Proof.
-  fix 2. intros n p.
-  refine (match p as p1 in Fin.t (S n1)
-                return forall (i1:Fin.t (S n1)), P n1 p1 i1 (lower p1 i1)
-          with
-            | @Fin.F1 n1 => _
-            | @Fin.FS n1 p1 => _
-          end); clear n p.
-  { revert n1. refine (@Fin.caseS _ _ _); cbn; intros.
-    apply c11. apply c1S. }
-  { intros i1. revert p1.
-    pattern n1, i1; refine (@Fin.caseS _ _ _ _ _);
-    clear n1 i1;
-    (intros [|n] i; [refine (False_rect _ (fin_0_absurd i)) | cbn ]).
-    { apply cS1. }
-    { intros p. pose proof (lower_ind n p i) as H.
-      destruct (lower p i) eqn:E.
-      { apply cSSS; assumption. }
-      { cbn. apply cSSN; assumption. } } }
-Qed.
-
-Section squeeze.
-  Context {A:Type} (x:A).
-  Notation vec := (Vector.t A).
-
-  Fixpoint squeeze {n} (v:vec n) (i:Fin.t (S n)) {struct i} : vec (S n) :=
-    match i in Fin.t (S _n) return vec _n -> vec (S _n)
-    with
-      | @Fin.F1 n' => fun v' => Vector.cons _ x _ v'
-      | @Fin.FS n' i' =>
-        fun v' =>
-          match n' as _n return vec _n -> Fin.t _n -> vec (S _n)
-          with
-            | 0 => fun u i' => False_rect _ (fin_0_absurd i')
-            | S m =>
-              fun (u:vec (S m)) =>
-                match u in Vector.t _ (S _m)
-                      return Fin.t (S _m) -> vec (S (S _m))
-                with
-                  | Vector.nil _ => tt
-                  | Vector.cons _ h _ u' =>
-                    fun j' => Vector.cons _ h _ (squeeze u' j')
-                end
-          end v' i'
-    end v.
-End squeeze.
-
-Lemma squeeze_nth (A:Type) (x:A) (n:nat) (v:Vector.t A n) p i :
-  Vector.nth (squeeze x v p) i = match lower p i with
-                                   | Some j => Vector.nth v j
-                                   | None => x
-                                 end.
-Proof.
-  (* alternatively: [functional induction (lower p i) using lower_ind] *)
-  revert v. pattern n, p, i, (lower p i).
-  refine (@lower_ind _ _ _ _ _ _ n p i);
-    intros; cbn; auto.
-
-  (*** Fails here with "Conversion test raised an anomaly" ***)
-  revert v.
-
-Abort.
+(*
+I'm not sure what the general rule should be; intuitively, I want [IsHProp (* Set *) Foo] to mean [IsHProp (* U >= Set *) Foo].  (I think this worked in HoTT/coq, too.)  Morally, [IsHProp] has no universe level associated with it distinct from that of its argument, you should never get a universe inconsistency from unifying [IsHProp A] with [IsHProp A].  (The issue is tricker when IsHProp uses [A] elsewhere, as in:
+*)
+
+(* File reduced by coq-bug-finder from original input, then from 7725 lines to 78 lines, then from 51 lines to 13 lines *)
+Set Universe Polymorphism.
+Inductive Empty : Set := .
+Record IsHProp (A : Type) := { foo : True }.
+Definition hprop_Empty : IsHProp@{i} Empty := {| foo := I |}.
+Goal let U := Type in let gt := Set : U in IsHProp (Empty : U).
+simpl.
+Set Printing Universes.
+exact @hprop_Empty. (* Toplevel input, characters 21-32:
+Error:
+The term "hprop_Empty" has type "IsHProp (* Set *) Empty"
+while it is expected to have type "IsHProp (* Top.17 *) Empty"
+(Universe inconsistency: Cannot enforce Top.17 = Set because Set < Top.17)). *)
+Defined.
+
+Module B.
+(* -*- coq-prog-args: ("-emacs" "-indices-matter") -*- *)
+(* File reduced by coq-bug-finder from original input, then from 7725 lines to 78 lines, then from 51 lines to 13 lines *)
+Set Universe Polymorphism.
+Inductive paths {A} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y) : type_scope.
+Record Contr (A : Type) := { center : A }.
+Monomorphic Record IsHProp (A : Type) := { foo : forall x y : A, Contr (x = y) }.
+Definition hprop_Empty : IsHProp Empty := {| foo x y := match x : Empty with end |}.
+Goal let U := Type in let gt := Set : U in IsHProp (Empty : U).
+simpl.
+Set Printing Universes.
+exact hprop_Empty.
+Defined.
+End B.
\ No newline at end of file