From 1311a2bf08ac1deb16f0b3064bc1164d75858a97 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Wed, 13 Jun 2018 14:16:49 +0200 Subject: Remove hack skipping comparison of algebraic universes in subtyping. When inferring [u <= v+k] I replaced the exception and instead add [u <= v]. This is trivially sound and it doesn't seem possible to have the one without the other (except specially for [Set <= v+k] which was already handled). I don't know an example where this used to fail and now succeeds (the point was to remove an anomaly, but the example ~~~ Module Type SG. Definition DG := Type. End SG. Module MG : SG. Definition DG := Type : Type. Fail End MG. ~~~ now fails with universe inconsistency. Fix #7695 (soundness bug!). --- kernel/univ.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/univ.ml') diff --git a/kernel/univ.ml b/kernel/univ.ml index 2b4a1c50c..311477dac 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -666,7 +666,7 @@ let constraint_add_leq v u c = else (* j >= 1 *) (* m = n + k, u <= v+k *) if Level.equal x y then c (* u <= u+k, trivial *) else if Level.is_small x then c (* Prop,Set <= u+S k, trivial *) - else anomaly (Pp.str"Unable to handle arbitrary u <= v+k constraints.") + else Constraint.add (x,Le,y) c (* u <= v implies u <= v+k *) let check_univ_leq_one u v = Universe.exists (Expr.leq u) v -- cgit v1.2.3