Cleaning up the implementation of module subtyping in the kernel.

We export a function in UGraph to check that a polymorphic instance is
a subtype of another, instead of rolling up our own in module code.

We also add a few tests for module subtyping in presence of polymorphic
constants.

1 files changed, 12 insertions, 0 deletions

diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index 487257a77..9793dd881 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -830,6 +830,18 @@ let sort_universes g =
   in
   normalize_universes g
 
+(** Subtyping of polymorphic contexts *)
+
+let check_subtype univs ctxT ctx =
+  if AUContext.size ctx == AUContext.size ctx then
+    let (inst, cst) = UContext.dest (AUContext.repr ctx) in
+    let cstT = UContext.constraints (AUContext.repr ctxT) in
+    let push accu v = add_universe v false accu in
+    let univs = Array.fold_left push univs (Instance.to_array inst) in
+    let univs = merge_constraints cstT univs in
+    check_constraints cst univs
+  else false
+
 (** Instances *)
 
 let check_eq_instances g t1 t2 =