From 4361c1ed9ac5646055f9f0eecc4a003d720c1994 Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Wed, 12 Apr 2017 13:29:16 +0200
Subject: Type@{_} should not produce a flexible algebraic universe.

Otherwise [(fun x => x) (Type : Type@{_})] becomes
[(fun x : Type@{i+1} => x) (Type@{i} : Type@{i+1})]
breaking the invariant that terms do not contain algebraic universes
(at the lambda abstraction).
---
 pretyping/pretyping.ml            |  3 ++-
 test-suite/success/polymorphism.v | 10 +++++-----
 2 files changed, 7 insertions(+), 6 deletions(-)

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 767e4be35b..4886423bd0 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -229,7 +229,8 @@ let interp_universe ?loc evd = function
 	    evd, Univ.Universe.make l
   | l ->
     List.fold_left (fun (evd, u) l -> 
-        let evd', l = interp_universe_level_name ~anon_rigidity:univ_flexible_alg evd l in
+        (* [univ_flexible_alg] can produce algebraic universes in terms *)
+        let evd', l = interp_universe_level_name ~anon_rigidity:univ_flexible evd l in
 	(evd', Univ.sup u (Univ.Universe.make l)))
     (evd, Univ.Universe.type0m) l
 
diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v
index 0a58fe89a1..66ff55edcb 100644
--- a/test-suite/success/polymorphism.v
+++ b/test-suite/success/polymorphism.v
@@ -333,12 +333,12 @@ Module Anonymous.
   Definition anonid := (fun x => x) : Type -> Type@{_}.
   Check anonid@{_}.
 
-  Definition defaultalg := Type : Type.
-  Definition usedefaultalg := defaultalg@{_ _}.
+  Definition defaultalg := (fun x : Type => x) (Type : Type).
+  Definition usedefaultalg := defaultalg@{_ _ _}.
   Check usedefaultalg@{_ _}.
 
-  Definition anonalg := (fun x => x) (Type : Type@{_}).
-  Check anonalg@{_}.
+  Definition anonalg := (fun x : Type@{_} => x) (Type : Type).
+  Check anonalg@{_ _}.
 
   Definition unrelated@{i j} := nat.
   Definition useunrelated := unrelated@{_ _}.
@@ -346,7 +346,7 @@ Module Anonymous.
 
   Definition inthemiddle@{i j k} :=
     let _ := defaultid@{i j} in
-    defaultalg@{k j}.
+    anonalg@{k j}.
   (* i <= j < k *)
   Definition collapsethemiddle := inthemiddle@{i _ j}.
   Check collapsethemiddle@{_ _}.
-- 
cgit v1.2.3