Change the ordering use for types during constraint generation with one which is…

Change the ordering use for types during constraint generation with one which is compatible with subtyping, when types are comparable.

types/type_tallying.ml

@@ -15,13 +15,14 @@ exception UnSatConstr of string
 
 module CS = struct
 
-    (* we require that types are semantically equivalent and not structurally
-     * equivalent *)
   let semantic_compare t1 t2 =
-    let c = Types.compare t1 t2 in
-    if c = 0 then 0 else
-      if equiv t1 t2 then 0
-      else c
+    let inf12 = Types.subtype t1 t2 in
+    let inf21 = Types.subtype t2 t1 in
+    if inf12 && inf21 then 0
+    else if inf12 then -1 else if inf21 then 1 else
+	let c = Types.compare t1 t2 in
+	assert (c <> 0);
+	c
 
     (* constraint set : map to store constraints of the form (s <= alpha <= t) *)
   module M = struct
@@ -753,7 +754,7 @@ let apply_raw delta s t =
 
   NormMemoHash.clear memo_norm;
   let s = Substitution.kind delta Var.function_kind s in
-  let t = Substitution.kind delta Var.argument_kind t in
+  let t = Substitution.kind delta Var.argument_kind t in 
   let vgamma = Var.mk "Gamma" in
   let gamma = var vgamma in
   let cgamma = cons gamma in