Define and use UGraph.enforce_leq_alg for subtyping inference

Not sure if worth using in other places.

4 files changed, 48 insertions, 4 deletions

diff --git a/kernel/constr.ml b/kernel/constr.ml
index 418229330..e68f906ec 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -828,8 +828,10 @@ let leq_constr_univs_infer univs m n =
 	let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in
 	if UGraph.check_leq univs u1 u2 then true
 	else
-	  (cstrs := Univ.enforce_leq u1 u2 !cstrs; 
-	   true)
+          (try let c, _ = UGraph.enforce_leq_alg u1 u2 univs in
+            cstrs := Univ.Constraint.union c !cstrs;
+            true
+          with Univ.UniverseInconsistency _ -> false)
     in
     let rec eq_constr' nargs m n =
       m == n || compare_head_gen eq_universes eq_sorts eq_constr' nargs m n
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index f4af31386..2c61b7a01 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -693,8 +693,8 @@ let infer_eq (univs, cstrs as cuniv) u u' =
 let infer_leq (univs, cstrs as cuniv) u u' =
   if UGraph.check_leq univs u u' then cuniv
   else
-    let cstrs' = Univ.enforce_leq u u' cstrs in
-      univs, cstrs'
+    let cstrs', _ = UGraph.enforce_leq_alg u u' univs in
+      univs, Univ.Constraint.union cstrs cstrs'
 
 let infer_cmp_universes env pb s0 s1 univs =
   let open Sorts in
diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index 4a9467de5..bc624ba56 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -747,6 +747,45 @@ let check_constraint g (l,d,r) =
 let check_constraints c g =
   Constraint.for_all (check_constraint g) c
 
+let leq_expr (u,m) (v,n) =
+  let d = match m - n with
+    | 1 -> Lt
+    | diff -> assert (diff <= 0); Le
+  in
+  (u,d,v)
+
+let enforce_leq_alg u v g =
+  let enforce_one (u,v) = function
+    | Inr _ as orig -> orig
+    | Inl (cstrs,g) as orig ->
+      if check_smaller_expr g u v then orig
+      else
+        (let c = leq_expr u v in
+         match enforce_constraint c g with
+         | g -> Inl (Constraint.add c cstrs,g)
+         | exception (UniverseInconsistency _ as e) -> Inr e)
+  in
+  (* max(us) <= max(vs) <-> forall u in us, exists v in vs, u <= v *)
+  let c = Universe.map (fun u -> Universe.map (fun v -> (u,v)) v) u in
+  let c = List.cartesians enforce_one (Inl (Constraint.empty,g)) c in
+  (* We pick a best constraint: smallest number of constraints, not an error if possible. *)
+  let order x y = match x, y with
+    | Inr _, Inr _ -> 0
+    | Inl _, Inr _ -> -1
+    | Inr _, Inl _ -> 1
+    | Inl (c,_), Inl (c',_) ->
+      Int.compare (Constraint.cardinal c) (Constraint.cardinal c')
+  in
+  match List.min order c with
+  | Inl x -> x
+  | Inr e -> raise e
+
+(* sanity check wrapper *)
+let enforce_leq_alg u v g =
+  let _,g as cg = enforce_leq_alg u v g in
+  assert (check_leq g u v);
+  cg
+
 (* Normalization *)
 
 (** [normalize_universes g] returns a graph where all edges point
diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli
index e6dd629e4..8c2d877b0 100644
--- a/kernel/uGraph.mli
+++ b/kernel/uGraph.mli
@@ -42,6 +42,9 @@ val merge_constraints : Constraint.t -> t -> t
 val check_constraint  : t -> univ_constraint -> bool
 val check_constraints : Constraint.t -> t -> bool
 
+(** Picks an arbitrary set of constraints sufficient to ensure [u <= v]. *)
+val enforce_leq_alg : Universe.t -> Universe.t -> t -> Constraint.t * t
+
 (** Adds a universe to the graph, ensuring it is >= or > Set.
    @raise AlreadyDeclared if the level is already declared in the graph. *)