diff options
| author | Gaetan Gilbert | 2017-04-12 13:29:16 +0200 |
|---|---|---|
| committer | Gaetan Gilbert | 2017-05-03 13:37:56 +0200 |
| commit | 4361c1ed9ac5646055f9f0eecc4a003d720c1994 (patch) | |
| tree | 773a5acaa5099e447eca5a62bd9d3e478a4a8e89 | |
| parent | e9b745af47ba3386724b874e3fd74b6dad33b015 (diff) | |
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).
| -rw-r--r-- | pretyping/pretyping.ml | 3 | ||||
| -rw-r--r-- | 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@{_ _}. |