Merge PR #890: Global universe declarations

5 files changed, 211 insertions, 23 deletions

diff --git a/test-suite/bugs/closed/4390.v b/test-suite/bugs/closed/4390.v
index a96a13700..c069b2d9d 100644
--- a/test-suite/bugs/closed/4390.v
+++ b/test-suite/bugs/closed/4390.v
@@ -8,16 +8,16 @@ Universe i.
 End foo.
 End M.
 
-Check Type@{i}.
+Check Type@{M.i}.
 (* Succeeds *)
 
 Fail Check Type@{j}.
 (* Error: Undeclared universe: j *)
 
-Definition foo@{j} : Type@{i} := Type@{j}.
+Definition foo@{j} : Type@{M.i} := Type@{j}.
 (* ok *)
 End A.
-
+Import A. Import M.
 Set Universe Polymorphism.
 Fail Universes j.
 Monomorphic Universe j.
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index f69379a57..d6d410d1a 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -44,26 +44,45 @@ bar@{u} = nat
 bar is universe polymorphic
 foo@{u Top.17 v} = 
 Type@{Top.17} -> Type@{v} -> Type@{u}
-     : Type@{max(u+1, Top.17+1, v+1)}
+     : Type@{max(u+1,Top.17+1,v+1)}
 (* u Top.17 v |=  *)
 
 foo is universe polymorphic
-Monomorphic mono = Type@{u}
-     : Type@{u+1}
-(* {u} |=  *)
+Monomorphic mono = Type@{mono.u}
+     : Type@{mono.u+1}
+(* {mono.u} |=  *)
 
 mono is not universe polymorphic
+mono
+     : Type@{mono.u+1}
+Type@{mono.u}
+     : Type@{mono.u+1}
+The command has indeed failed with message:
+Universe u already exists.
+monomono
+     : Type@{MONOU+1}
+mono.monomono
+     : Type@{mono.MONOU+1}
+monomono
+     : Type@{MONOU+1}
+mono
+     : Type@{mono.u+1}
+The command has indeed failed with message:
+Universe u already exists.
+bobmorane = 
+let tt := Type@{tt.v} in let ff := Type@{ff.v} in tt -> ff
+     : Type@{max(tt.u,ff.u)}
 The command has indeed failed with message:
 Universe u already bound.
 foo@{E M N} = 
 Type@{M} -> Type@{N} -> Type@{E}
-     : Type@{max(E+1, M+1, N+1)}
+     : Type@{max(E+1,M+1,N+1)}
 (* E M N |=  *)
 
 foo is universe polymorphic
 foo@{Top.16 Top.17 Top.18} = 
 Type@{Top.17} -> Type@{Top.18} -> Type@{Top.16}
-     : Type@{max(Top.16+1, Top.17+1, Top.18+1)}
+     : Type@{max(Top.16+1,Top.17+1,Top.18+1)}
 (* Top.16 Top.17 Top.18 |=  *)
 
 foo is universe polymorphic
@@ -88,9 +107,10 @@ The command has indeed failed with message:
 This object does not support universe names.
 The command has indeed failed with message:
 Cannot enforce v < u because u < gU < gV < v
-Monomorphic bind_univs.mono = Type@{u}
-     : Type@{u+1}
-(* {u} |=  *)
+Monomorphic bind_univs.mono = 
+Type@{bind_univs.mono.u}
+     : Type@{bind_univs.mono.u+1}
+(* {bind_univs.mono.u} |=  *)
 
 bind_univs.mono is not universe polymorphic
 bind_univs.poly@{u} = Type@{u}
@@ -99,12 +119,12 @@ bind_univs.poly@{u} = Type@{u}
 
 bind_univs.poly is universe polymorphic
 insec@{v} = Type@{u} -> Type@{v}
-     : Type@{max(u+1, v+1)}
+     : Type@{max(u+1,v+1)}
 (* v |=  *)
 
 insec is universe polymorphic
 insec@{u v} = Type@{u} -> Type@{v}
-     : Type@{max(u+1, v+1)}
+     : Type@{max(u+1,v+1)}
 (* u v |=  *)
 
 insec is universe polymorphic
@@ -125,28 +145,28 @@ inmod@{u} = Type@{u}
 inmod is universe polymorphic
 Applied.infunct@{u v} = 
 inmod@{u} -> Type@{v}
-     : Type@{max(u+1, v+1)}
+     : Type@{max(u+1,v+1)}
 (* u v |=  *)
 
 Applied.infunct is universe polymorphic
-axfoo@{i Top.33 Top.34} : Type@{Top.33} -> Type@{i}
-(* i Top.33 Top.34 |=  *)
+axfoo@{i Top.41 Top.42} : Type@{Top.41} -> Type@{i}
+(* i Top.41 Top.42 |=  *)
 
 axfoo is universe polymorphic
 Argument scope is [type_scope]
 Expands to: Constant Top.axfoo
-axbar@{i Top.33 Top.34} : Type@{Top.34} -> Type@{i}
-(* i Top.33 Top.34 |=  *)
+axbar@{i Top.41 Top.42} : Type@{Top.42} -> Type@{i}
+(* i Top.41 Top.42 |=  *)
 
 axbar is universe polymorphic
 Argument scope is [type_scope]
 Expands to: Constant Top.axbar
-axfoo' : Type@{Top.36} -> Type@{i}
+axfoo' : Type@{Top.44} -> Type@{axbar'.i}
 
 axfoo' is not universe polymorphic
 Argument scope is [type_scope]
 Expands to: Constant Top.axfoo'
-axbar' : Type@{Top.36} -> Type@{i}
+axbar' : Type@{Top.44} -> Type@{axbar'.i}
 
 axbar' is not universe polymorphic
 Argument scope is [type_scope]
diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v
index 116d5e5e9..266d94ad9 100644
--- a/test-suite/output/UnivBinders.v
+++ b/test-suite/output/UnivBinders.v
@@ -1,6 +1,6 @@
 Set Universe Polymorphism.
 Set Printing Universes.
-Unset Strict Universe Declaration.
+(* Unset Strict Universe Declaration. *)
 
 (* universe binders on inductive types and record projections *)
 Inductive Empty@{u} : Type@{u} := .
@@ -25,14 +25,59 @@ Print wrap.
 Instance bar@{u} : Wrap@{u} Set. Proof. exact nat. Qed.
 Print bar.
 
+Unset Strict Universe Declaration.
 (* The universes in the binder come first, then the extra universes in
    order of appearance. *)
 Definition foo@{u +} := Type -> Type@{v} -> Type@{u}.
 Print foo.
+Set Strict Universe Declaration.
 
 (* Binders even work with monomorphic definitions! *)
 Monomorphic Definition mono@{u} := Type@{u}.
 Print mono.
+Check mono.
+Check Type@{mono.u}.
+
+Module mono.
+  Fail Monomorphic Universe u.
+  Monomorphic Universe MONOU.
+
+  Monomorphic Definition monomono := Type@{MONOU}.
+  Check monomono.
+End mono.
+Check mono.monomono. (* qualified MONOU *)
+Import mono.
+Check monomono. (* unqualified MONOU *)
+Check mono. (* still qualified mono.u *)
+
+Monomorphic Constraint Set < Top.mono.u.
+
+Module mono2.
+  Monomorphic Universe u.
+End mono2.
+
+Fail Monomorphic Definition mono2@{u} := Type@{u}.
+
+Module SecLet.
+  Unset Universe Polymorphism.
+  Section foo.
+    (* Fail Let foo@{} := Type@{u}. (* doesn't parse: Let foo@{...} doesn't exist *) *)
+    Unset Strict Universe Declaration.
+    Let tt : Type@{u} := Type@{v}. (* names disappear in the ether *)
+    Let ff : Type@{u}. Proof. exact Type@{v}. Qed. (* if Set Universe Polymorphism: universes are named ff.u and ff.v. Otherwise names disappear into space *)
+    Definition bobmorane := tt -> ff.
+  End foo.
+  Print bobmorane. (*
+                     bobmorane@{Top.15 Top.16 ff.u ff.v} =
+                     let tt := Type@{Top.16} in let ff := Type@{ff.v} in tt -> ff
+                     : Type@{max(Top.15,ff.u)}
+                     (* Top.15 Top.16 ff.u ff.v |= Top.16 < Top.15
+                     ff.v < ff.u
+                    *)
+
+                    bobmorane is universe polymorphic
+                    *)
+End SecLet.
 
 (* fun x x => foo is nonsense with local binders *)
 Fail Definition fo@{u u} := Type@{u}.
@@ -61,7 +106,7 @@ Monomorphic Universes gU gV. Monomorphic Constraint gU < gV.
 Fail Lemma foo@{u v|u < gU, gV < v, v < u} : nat.
 
 (* Universe binders survive through compilation, sections and modules. *)
-Require bind_univs.
+Require TestSuite.bind_univs.
 Print bind_univs.mono.
 Print bind_univs.poly.
 
diff --git a/test-suite/prerequisite/bind_univs.v b/test-suite/prerequisite/bind_univs.v
index f17c00e9d..e834fde11 100644
--- a/test-suite/prerequisite/bind_univs.v
+++ b/test-suite/prerequisite/bind_univs.v
@@ -3,3 +3,5 @@
 Monomorphic Definition mono@{u} := Type@{u}.
 
 Polymorphic Definition poly@{u} := Type@{u}.
+
+Monomorphic Universe reqU.
diff --git a/test-suite/success/unidecls.v b/test-suite/success/unidecls.v
new file mode 100644
index 000000000..c4a1d7c28
--- /dev/null
+++ b/test-suite/success/unidecls.v
@@ -0,0 +1,121 @@
+Set Printing Universes.
+
+Module unidecls.
+  Universes a b.
+End unidecls.
+
+Universe a.
+
+Constraint a < unidecls.a.
+
+Print Universes.
+
+(** These are different universes *)
+Check Type@{a}.
+Check Type@{unidecls.a}.
+
+Check Type@{unidecls.b}.
+
+Fail Check Type@{unidecls.c}.
+
+Fail Check Type@{i}.
+Universe foo.
+Module Foo.
+  (** Already declared globaly: but universe names are scoped at the module level  *)
+  Universe foo.
+  Universe bar.
+
+  Check Type@{Foo.foo}.
+  Definition bar := 0.
+End Foo.
+
+(** Already declared in the module *)
+Universe bar.
+
+(** Accessible outside the module: universe declarations are global *)
+Check Type@{bar}.
+Check Type@{Foo.bar}.
+
+Check Type@{Foo.foo}.
+(** The same *)
+Check Type@{foo}.
+Check Type@{Top.foo}.
+
+Universe secfoo.
+Section Foo'.
+  Fail Universe secfoo.
+  Universe secfoo2.
+  Check Type@{Foo'.secfoo2}.
+  Constraint secfoo2 < a.
+End Foo'.
+
+Check Type@{secfoo2}.
+Fail Check Type@{Foo'.secfoo2}.
+Fail Check eq_refl : Type@{secfoo2} = Type@{a}.
+
+(** Below, u and v are global, fixed universes *)
+Module Type Arg.
+  Universe u.
+  Parameter T: Type@{u}.
+End Arg.
+
+Module Fn(A : Arg).
+  Universes v.
+
+  Check Type@{A.u}.
+  Constraint A.u < v.
+
+  Definition foo : Type@{v} := nat.
+  Definition bar : Type@{A.u} := nat.
+
+  Fail Definition foo(A : Type@{v}) : Type@{A.u} := A.
+End Fn.
+
+Module ArgImpl : Arg.
+  Definition T := nat.
+End ArgImpl.
+
+Module ArgImpl2 : Arg.
+  Definition T := bool.
+End ArgImpl2.
+
+(** Two applications of the functor result in the exact same universes *)
+Module FnApp := Fn(ArgImpl).
+
+Check Type@{FnApp.v}.
+Check FnApp.foo.
+Check FnApp.bar.
+
+Check (eq_refl : Type@{ArgImpl.u} = Type@{ArgImpl2.u}).
+
+Module FnApp2 := Fn(ArgImpl).
+Check Type@{FnApp2.v}.
+Check FnApp2.foo.
+Check FnApp2.bar.
+
+Import ArgImpl2.
+(** Now u refers to ArgImpl.u and ArgImpl2.u *)
+Check FnApp2.bar.
+
+(** It can be shadowed *)
+Universe u.
+
+(** This refers to the qualified name *)
+Check FnApp2.bar.
+
+Constraint u = ArgImpl.u.
+Print Universes.
+
+Set Universe Polymorphism.
+
+Section PS.
+  Universe poly.
+
+  Definition id (A : Type@{poly}) (a : A) : A := a.
+End PS.
+(** The universe is polymorphic and discharged, does not persist *)
+Fail Check Type@{poly}.
+
+Print Universes.
+Check id nat.
+Check id@{Set}.