Merge PR #6775: Allow using cumulativity without forcing strict constraints.

4 files changed, 324 insertions, 49 deletions

diff --git a/test-suite/bugs/closed/6661.v b/test-suite/bugs/closed/6661.v
new file mode 100644
index 000000000..e88a3704d
--- /dev/null
+++ b/test-suite/bugs/closed/6661.v
@@ -0,0 +1,259 @@
+(* -*- mode: coq; coq-prog-args: ("-noinit" "-indices-matter" "-w" "-notation-overridden,-deprecated-option") -*- *)
+(*
+    The Coq Proof Assistant, version 8.7.1 (January 2018)
+    compiled on Jan 21 2018 15:02:24 with OCaml 4.06.0
+    from commit 391bb5e196901a3a9426295125b8d1c700ab6992
+ *)
+
+
+Require Export Coq.Init.Notations.
+Notation "'∏'  x .. y , P" := (forall x, .. (forall y, P) ..)
+  (at level 200, x binder, y binder, right associativity) : type_scope.
+Notation "'λ' x .. y , t" := (fun x => .. (fun y => t) ..)
+  (at level 200, x binder, y binder, right associativity).
+Notation "A -> B" := (forall (_ : A), B) : type_scope.
+Reserved Notation "p @ q" (at level 60, right associativity).
+Reserved Notation "! p " (at level 50).
+
+Monomorphic Universe uu.
+Monomorphic Universe uu0.
+Monomorphic Universe uu1.
+Constraint uu0 < uu1.
+
+Global Set Universe Polymorphism.
+Global Set Polymorphic Inductive Cumulativity.
+Global Unset Universe Minimization ToSet.
+
+Notation UU  := Type (only parsing).
+Notation UU0 := Type@{uu0} (only parsing).
+
+Global Set Printing Universes.
+
+ Inductive unit : UU0 := tt : unit.
+
+Inductive paths@{i} {A:Type@{i}} (a:A) : A -> Type@{i} := idpath : paths a a.
+Hint Resolve idpath : core .
+Notation "a = b" := (paths a b) (at level 70, no associativity) : type_scope.
+
+Set Primitive Projections.
+Set Nonrecursive Elimination Schemes.
+
+Record total2@{i} { T: Type@{i} } ( P: T -> Type@{i} ) : Type@{i}
+  := tpair { pr1 : T; pr2 : P pr1 }.
+
+Arguments tpair {_} _ _ _.
+Arguments pr1 {_ _} _.
+Arguments pr2 {_ _} _.
+
+Notation "'∑'  x .. y , P" := (total2 (λ x, .. (total2 (λ y, P)) ..))
+  (at level 200, x binder, y binder, right associativity) : type_scope.
+
+Definition foo (X:Type) (xy : @total2 X (λ _, X)) : X.
+  induction xy as [x y].
+  exact x.
+Defined.
+
+Unset Automatic Introduction.
+
+Definition idfun (T : UU) := λ t:T, t.
+
+Definition pathscomp0 {X : UU} {a b c : X} (e1 : a = b) (e2 : b = c) : a = c.
+Proof.
+  intros. induction e1. exact e2.
+Defined.
+
+Hint Resolve @pathscomp0 : pathshints.
+
+Notation "p @ q" := (pathscomp0 p q).
+
+Definition pathsinv0 {X : UU} {a b : X} (e : a = b) : b = a.
+Proof.
+  intros. induction e. exact (idpath _).
+Defined.
+
+Notation "! p " := (pathsinv0 p).
+
+Definition maponpaths {T1 T2 : UU} (f : T1 -> T2) {t1 t2 : T1}
+           (e: t1 = t2) : f t1 = f t2.
+Proof.
+  intros. induction e. exact (idpath _).
+Defined.
+
+Definition map_on_two_paths {X Y Z : UU} (f : X -> Y -> Z) {x x' y y'} (ex : x = x') (ey: y = y') :
+  f x y = f x' y'.
+Proof.
+  intros. induction ex. induction ey. exact (idpath _).
+Defined.
+
+
+Definition maponpathscomp0 {X Y : UU} {x1 x2 x3 : X}
+           (f : X -> Y) (e1 : x1 = x2) (e2 : x2 = x3) :
+  maponpaths f (e1 @ e2) = maponpaths f e1 @ maponpaths f e2.
+Proof.
+  intros. induction e1. induction e2. exact (idpath _).
+Defined.
+
+Definition maponpathsinv0 {X Y : UU} (f : X -> Y)
+           {x1 x2 : X} (e : x1 = x2) : maponpaths f (! e) = ! (maponpaths f e).
+Proof.
+  intros. induction e. exact (idpath _).
+Defined.
+
+
+
+Definition constr1 {X : UU} (P : X -> UU) {x x' : X} (e : x = x') :
+  ∑ (f : P x -> P x'),
+  ∑ (ee : ∏ p : P x, tpair _ x p = tpair _ x' (f p)),
+  ∏ (pp : P x), maponpaths pr1 (ee pp) = e.
+Proof.
+  intros. induction e.
+  split with (idfun (P x)).
+  split with (λ p, idpath _).
+  unfold maponpaths. simpl.
+  intro. exact (idpath _).
+Defined.
+
+Definition transportf@{i} {X : Type@{i}} (P : X -> Type@{i}) {x x' : X}
+           (e : x = x') : P x -> P x' := pr1 (constr1 P e).
+
+Lemma two_arg_paths_f@{i} {A : Type@{i}} {B : A -> Type@{i}} {C:Type@{i}} {f : ∏ a, B a -> C} {a1 b1 a2 b2}
+      (p : a1 = a2) (q : transportf B p b1 = b2) : f a1 b1 = f a2 b2.
+Proof.
+  intros. induction p. induction q. exact (idpath _).
+Defined.
+
+Definition iscontr@{i} (T:Type@{i}) : Type@{i} := ∑ cntr:T, ∏ t:T, t=cntr.
+
+Lemma proofirrelevancecontr {X : UU} (is : iscontr X) (x x' : X) : x = x'.
+Proof.
+  intros.
+  induction is as [y fe].
+  exact (fe x @ !(fe x')).
+Defined.
+
+
+Definition hfiber@{i} {X Y : Type@{i}} (f : X -> Y) (y : Y) : Type@{i} := total2 (λ x, f x = y).
+
+Definition hfiberpair {X Y : UU} (f : X -> Y) {y : Y}
+           (x : X) (e : f x = y) : hfiber f y :=
+  tpair _ x e.
+
+Definition coconustot (T : UU) (t : T) := ∑ t' : T, t' = t.
+
+Definition coconustotpair (T : UU) {t t' : T} (e: t' = t) : coconustot T t
+  := tpair _ t' e.
+
+Lemma connectedcoconustot {T : UU} {t : T} (c1 c2 : coconustot T t) : c1 = c2.
+Proof.
+  intros.
+  induction c1 as [x0 x].
+  induction x.
+  induction c2 as [x1 y].
+  induction y.
+  exact (idpath _).
+Defined.
+
+Definition isweq@{i} {X Y : Type@{i}} (f : X -> Y) : Type@{i} :=
+  ∏ y : Y, iscontr (hfiber f y).
+
+Lemma isProofIrrelevantUnit : ∏ x x' : unit, x = x'.
+Proof.
+  intros. induction x. induction x'. exact (idpath _).
+Defined.
+
+Lemma unitl0 : tt = tt -> coconustot _ tt.
+Proof.
+  intros e. exact (coconustotpair unit e).
+Defined.
+
+Lemma unitl1: coconustot _ tt -> tt = tt.
+Proof.
+  intro cp. induction cp as [x t]. induction x. exact t.
+Defined.
+
+Lemma unitl2: ∏ e : tt = tt, unitl1 (unitl0 e) = e.
+Proof.
+  intros. unfold unitl0. simpl. exact (idpath _).
+Defined.
+
+Lemma unitl3: ∏ e : tt = tt, e = idpath tt.
+Proof.
+  intros.
+
+  assert (e0 : unitl0 (idpath tt) = unitl0 e).
+  { simple refine (connectedcoconustot _ _). }
+
+  set (e1 := maponpaths unitl1 e0).
+
+  exact (! (unitl2 e) @ (! e1) @ (unitl2 (idpath _))).
+Defined.
+
+Theorem iscontrpathsinunit (x x' : unit) : iscontr (x = x').
+Proof.
+  intros.
+  split with (isProofIrrelevantUnit x x').
+  intros e'.
+  induction x.
+  induction x'.
+  simpl.
+  apply unitl3.
+Qed.
+
+Lemma ifcontrthenunitl0 (e1 e2 : tt = tt) : e1 = e2.
+Proof.
+  intros.
+  simple refine (proofirrelevancecontr _ _ _).
+  exact (iscontrpathsinunit tt tt).
+Qed.
+
+Section isweqcontrtounit.
+
+  Universe i.
+
+  (* To see the bug, run it both with and without this constraint: *)
+
+  (* Constraint uu0 < i. *)
+
+  (* Without this constraint, we get i = uu0 in the next definition *)
+  Lemma isweqcontrtounit@{} {T : Type@{i}} (is : iscontr@{i} T) : isweq@{i} (λ _:T, tt).
+  Proof.
+    intros. intro y. induction y.
+    induction is as [c h].
+    split with (hfiberpair@{i i i} _ c (idpath tt)).
+    intros ha.
+    induction ha as [x e].
+    simple refine (two_arg_paths_f (h x) _).
+    simple refine (ifcontrthenunitl0 _ _).
+  Defined.
+
+  (*
+     Explanation of the bug:
+
+     With the constraint uu0 < i above we get:
+
+            |= uu0 <= bug.3
+               uu0 <= i
+               uu1 <= i
+               i <= bug.3
+
+     from this print statement: *)
+
+         Print isweqcontrtounit.
+
+  (*
+
+     Without the constraint uu0 < i above we get:
+
+            |= i <= bug.3
+               uu0 = i
+
+     Since uu0 = i is not inferred when we impose the constraint uu0 < i,
+     it is invalid to infer it when we don't.
+
+   *)
+
+  Context (X : Type@{uu1}).
+
+  Check (@isweqcontrtounit X). (* detect a universe inconsistency *)
+
+End isweqcontrtounit.
diff --git a/test-suite/bugs/closed/6775.v b/test-suite/bugs/closed/6775.v
new file mode 100644
index 000000000..206df23bc
--- /dev/null
+++ b/test-suite/bugs/closed/6775.v
@@ -0,0 +1,43 @@
+(* Issue caused and fixed during the lifetime of #6775: unification
+   failing on partially applied cumulative inductives. *)
+
+Set Universe Polymorphism.
+
+Set Polymorphic Inductive Cumulativity.
+
+Unset Elimination Schemes.
+
+Inductive paths@{i} {A : Type@{i}} (a : A) : A -> Type@{i} :=
+  idpath : paths a a.
+
+Arguments idpath {A a} , [A] a.
+
+Notation "x = y :> A" := (@paths A x y) : type_scope.
+Notation "x = y" := (x = y :>_) : type_scope.
+
+Definition inverse {A : Type} {x y : A} (p : x = y) : y = x
+  := match p with idpath => idpath end.
+
+Arguments inverse {A x y} p : simpl nomatch.
+
+Definition concat {A : Type} {x y z : A} (p : x = y) (q : y = z) : x = z :=
+  match p, q with idpath, idpath => idpath end.
+
+Arguments concat {A x y z} p q : simpl nomatch.
+
+Notation "1" := idpath.
+
+Reserved Notation "p @ q" (at level 20).
+Notation "p @ q" := (concat p q).
+
+Reserved Notation "p ^" (at level 3, format "p '^'").
+Notation "p ^" := (inverse p).
+
+Definition concat_pV_p {A} {x y z : A} (p : x = z) (q : y = z) :
+  (p @ q^) @ q = p
+  :=
+  (match q as i return forall p, (p @ i^) @ i = p with
+    idpath =>
+    fun p =>
+      match p with idpath => 1 end
+  end) p.
diff --git a/test-suite/coqchk/cumulativity.v b/test-suite/coqchk/cumulativity.v
index d63a3548e..034684054 100644
--- a/test-suite/coqchk/cumulativity.v
+++ b/test-suite/coqchk/cumulativity.v
@@ -25,7 +25,7 @@ Section ListLower.
 
 End ListLower.
 
-Lemma LowerL_Lem@{i j} (A : Type@{j}) (l : List@{i} A) : l = LowerL l.
+Lemma LowerL_Lem@{i j|j<i+} (A : Type@{j}) (l : List@{i} A) : l = LowerL@{j i} l.
 Proof. reflexivity. Qed.
 (*
 I disable these tests because cqochk can't process them when compiled with
diff --git a/test-suite/success/cumulativity.v b/test-suite/success/cumulativity.v
index 4dda36042..dfa305dc6 100644
--- a/test-suite/success/cumulativity.v
+++ b/test-suite/success/cumulativity.v
@@ -10,40 +10,16 @@ Set Printing Universes.
 
 Inductive List (A: Type) := nil | cons : A -> List A -> List A.
 
-Section ListLift.
-  Universe i j.
-
-  Constraint i < j.
-
-  Definition LiftL {A} : List@{i} A -> List@{j} A := fun x => x.
-
-End ListLift.
+Definition LiftL@{k i j|k <= i, k <= j} {A:Type@{k}} : List@{i} A -> List@{j} A := fun x => x.
 
 Lemma LiftL_Lem A (l : List A) : l = LiftL l.
 Proof. reflexivity. Qed.
 
-Section ListLower.
-  Universe i j.
-
-  Constraint i < j.
-
-  Definition LowerL {A : Type@{i}} : List@{j} A -> List@{i} A := fun x => x.
-
-End ListLower.
-
-Lemma LowerL_Lem@{i j} (A : Type@{j}) (l : List@{i} A) : l = LowerL l.
-Proof. reflexivity. Qed.
-
 Inductive Tp := tp : Type -> Tp.
 
-Section TpLift.
-  Universe i j.
-
-  Constraint i < j.
-
-  Definition LiftTp : Tp@{i} -> Tp@{j} := fun x => x.
+Definition LiftTp@{i j|i <= j} : Tp@{i} -> Tp@{j} := fun x => x.
 
-End TpLift.
+Fail Definition LowerTp@{i j|j < i} : Tp@{i} -> Tp@{j} := fun x => x.
 
 Record Tp' := { tp' : Tp }.
 
@@ -51,22 +27,12 @@ Definition CTp := Tp.
 (* here we have to reduce a constant to infer the correct subtyping. *)
 Record Tp'' := { tp'' : CTp }.
 
-Definition LiftTp'@{i j|i < j} : Tp'@{i} -> Tp'@{j} := fun x => x.
-Definition LiftTp''@{i j|i < j} : Tp''@{i} -> Tp''@{j} := fun x => x.
+Definition LiftTp'@{i j|i <= j} : Tp'@{i} -> Tp'@{j} := fun x => x.
+Definition LiftTp''@{i j|i <= j} : Tp''@{i} -> Tp''@{j} := fun x => x.
 
 Lemma LiftC_Lem (t : Tp) : LiftTp t = t.
 Proof. reflexivity. Qed.
 
-Section TpLower.
-  Universe i j.
-
-  Constraint i < j.
-
-  Fail Definition LowerTp : Tp@{j} -> Tp@{i} := fun x => x.
-
-End TpLower.
-
-
 Section subtyping_test.
   Universe i j.
   Constraint i < j.
@@ -82,14 +48,8 @@ Record B (X : A) : Type := { b : X; }.
 NonCumulative Inductive NCList (A: Type)
   := ncnil | nccons : A -> NCList A -> NCList A.
 
-Section NCListLift.
-  Universe i j.
-
-  Constraint i < j.
-
-  Fail Definition LiftNCL {A} : NCList@{i} A -> NCList@{j} A := fun x => x.
-
-End NCListLift.
+Fail Definition LiftNCL@{k i j|k <= i, k <= j} {A:Type@{k}}
+  : NCList@{i} A -> NCList@{j} A := fun x => x.
 
 Inductive eq@{i} {A : Type@{i}} (x : A) : A -> Type@{i} := eq_refl : eq x x.
 
@@ -114,7 +74,7 @@ Fail Definition arrow_lift@{i i' j j' | i' < i, j < j'}
   : Arrow@{i j} -> Arrow@{i' j'}
   := fun x => x.
 
-Definition arrow_lift@{i i' j j' | i' = i, j < j'}
+Definition arrow_lift@{i i' j j' | i' = i, j <= j'}
   : Arrow@{i j} -> Arrow@{i' j'}
   := fun x => x.
 
@@ -155,3 +115,16 @@ Definition checkcumul :=
 (* They can only be compared at the highest type *)
 Fail Definition checkcumul' :=
   eq_refl _ : @eq twotys@{i k l} (twoconstr@{i j k} Tyi Tyi) (twoconstr@{j i k} Tyi Tyi).
+
+(* An inductive type with an irrelevant universe *)
+Inductive foo@{i} : Type@{i} := mkfoo { }.
+
+Definition bar := foo.
+
+(* The universe on mkfoo is flexible and should be unified with i. *)
+Definition foo1@{i} : foo@{i} := let x := mkfoo in x. (* fast path for conversion *)
+Definition foo2@{i} : bar@{i} := let x := mkfoo in x. (* must reduce *)
+
+(* Rigid universes however should not be unified unnecessarily. *)
+Definition foo3@{i j|} : foo@{i} := let x := mkfoo@{j} in x.
+Definition foo4@{i j|} : bar@{i} := let x := mkfoo@{j} in x.