Actually use the hints for Matching.

lib/db/MatchFeat.ml

@@ -29,17 +29,13 @@ module Const : S = struct
 
   let compare = CSet.compare
 
-  let subset ~small:t1 t2 =
-    let check_mem b cnt ty = b && cnt <= CSet.count t2 ty in
-    CSet.fold t1 true check_mem
-
   (*compatible t1 t2 returns false if t1 cannot match with t2 in the sense t1 <= t2*)
   let compatible t1 t2 : Acic.hint =
-    match subset ~small:t1 t2, subset t1 ~small:t2 with
+    match CSet.contains t2 t1, CSet.contains t1 t2 with
     | true, true -> Unsure
-    | false, false -> Uncompatible
-    | true, false -> Not_smaller
-    | false, true -> Not_bigger
+    | false, false -> Incompatible
+    | true, false -> Maybe_bigger
+    | false, true -> Maybe_smaller
 end
 
 let all = [ (module Const : S) ]
@@ -61,7 +57,7 @@ let compatible (t1 : Type.t) (t2 : Type.t) =
   CCList.fold_left check_feat Unsure feats
 
 let compare env t1 t2 =
-  if not (Feature.compatible t1 t2) then Acic.Uncomparable
+  if not (Feature.compatible t1 t2) then Acic.Incomparable
   else
     let hint = compatible t1 t2 in
     Acic.compare ~hint env t1 t2

lib/db/Poset.ml

@@ -234,7 +234,7 @@ let add ({ env; graph; tops; bottoms; _ } as poset) tyid_0 ~range =
     if TypeId.check tyid range then
       MatchFeat.compare env (TypeId.ty tyid) ty_0
     else
-      Uncomparable
+      Incomparable
   in
   let rec visit_down already_seen ~prev ~current =
     debug (fun m ->
@@ -253,7 +253,7 @@ let add ({ env; graph; tops; bottoms; _ } as poset) tyid_0 ~range =
         l;
       Changes.add_upper_bound ch poset.graph current;
       visit_next already_seen
-    | Uncomparable ->
+    | Incomparable ->
       incr uncomparable;
       visit_next already_seen
     | Smaller ->
@@ -271,7 +271,7 @@ let add ({ env; graph; tops; bottoms; _ } as poset) tyid_0 ~range =
     | Bigger ->
       incr bigger;
       visit_next already_seen
-    | Uncomparable ->
+    | Incomparable ->
       incr uncomparable;
       visit_next already_seen
     | Smaller ->

lib/unification/Acic.mli

@@ -8,11 +8,11 @@
 
 (** {1 Matching} *)
 
-type ord = Uncomparable | Smaller | Bigger | Matching_equiv
+type ord = Incomparable | Smaller | Bigger | Matching_equiv
 
 val pp_ord : Format.formatter -> ord -> unit
 
-type hint = Uncompatible | Not_smaller | Not_bigger | Unsure
+type hint = Incompatible | Maybe_bigger | Maybe_smaller | Unsure
 
 val pp_hint : hint Fmt.t
 val combine_hint : hint -> hint -> hint

lib/unification/Matching.ml

@@ -5,51 +5,55 @@ let test env t1 ~freeze:t2 =
         t1 Type.pp t2);
   Unification.unifiable env t1 t2
 
-type ord = Uncomparable | Smaller | Bigger | Matching_equiv
+type ord = Incomparable | Smaller | Bigger | Matching_equiv
 
 let pp_ord fmt c =
   match c with
-  | Uncomparable -> Format.fprintf fmt "Uncomparable"
+  | Incomparable -> Format.fprintf fmt "Incomparable"
   | Smaller -> Format.fprintf fmt "Smaller"
   | Bigger -> Format.fprintf fmt "Bigger"
   | Matching_equiv -> Format.fprintf fmt "Equal"
 
-type hint = Uncompatible | Not_smaller | Not_bigger | Unsure
+type hint = Incompatible | Maybe_bigger | Maybe_smaller | Unsure
 
 let combine_hint h1 h2 =
   match (h1, h2) with
-  | Uncompatible, _
-  | _, Uncompatible
-  | Not_bigger, Not_smaller
-  | Not_smaller, Not_bigger ->
-      Uncompatible
-  | Not_bigger, Not_bigger | Not_bigger, Unsure | Unsure, Not_bigger ->
-      Not_bigger
-  | Not_smaller, Not_smaller | Not_smaller, Unsure | Unsure, Not_smaller ->
-      Not_smaller
+  | Incompatible, _
+  | _, Incompatible
+  | Maybe_smaller, Maybe_bigger
+  | Maybe_bigger, Maybe_smaller ->
+      Incompatible
+  | Maybe_smaller, Maybe_smaller
+  | Maybe_smaller, Unsure
+  | Unsure, Maybe_smaller ->
+      Maybe_smaller
+  | Maybe_bigger, Maybe_bigger
+  | Maybe_bigger, Unsure
+  | Unsure, Maybe_bigger ->
+      Maybe_bigger
   | Unsure, Unsure -> Unsure
 
 let pp_hint fmt = function
-  | Not_bigger -> Fmt.pf fmt "Not_bigger"
-  | Not_smaller -> Fmt.pf fmt "Not_smaller"
+  | Maybe_smaller -> Fmt.pf fmt "Maybe_smaller"
+  | Maybe_bigger -> Fmt.pf fmt "Maybe_bigger"
   | Unsure -> Fmt.pf fmt "Unsure"
-  | Uncompatible -> Fmt.pf fmt "Uncompatible"
+  | Incompatible -> Fmt.pf fmt "Incompatible"
 
 let compare ?(hint = Unsure) env (t1 : Type.t) (t2 : Type.t) =
   Logs.debug (fun m ->
       m "Trying match %a %a with hint %a" Type.pp t1 Type.pp t2 pp_hint hint);
-  (* let hint = Unsure in *)
-  let _maybe_smaller, _maybe_bigger =
-    match hint with
-    | Unsure -> (true, true)
-    | Not_bigger -> (true, false)
-    | Not_smaller -> (false, true)
-    | Uncompatible -> (false, false)
-  in
-  let is_smaller = (*maybe_smaller &&*) test env ~freeze:t1 t2 in
-  let is_bigger = (*maybe_bigger &&*) test env t1 ~freeze:t2 in
-  match (is_smaller, is_bigger) with
-  | true, true -> Matching_equiv
-  | false, false -> Uncomparable
-  | true, false -> Smaller
-  | false, true -> Bigger
+  match hint with
+  | Unsure ->
+    let is_smaller = test env ~freeze:t1 t2 in
+    let is_bigger = test env t1 ~freeze:t2 in
+    begin match (is_smaller, is_bigger) with
+      | true, true -> Matching_equiv
+      | false, false -> Incomparable
+      | true, false -> Smaller
+      | false, true -> Bigger
+    end
+  | Maybe_smaller ->
+    if test env ~freeze:t1 t2 then Smaller else Incomparable
+  | Maybe_bigger ->
+    if test env t1 ~freeze:t2 then Bigger else Incomparable
+  | Incompatible -> Incomparable

lib/unification/Matching.mli

@@ -1,8 +1,8 @@
-type ord = Uncomparable | Smaller | Bigger | Matching_equiv
+type ord = Incomparable | Smaller | Bigger | Matching_equiv
 
 val pp_ord : Format.formatter -> ord -> unit
 
-type hint = Uncompatible | Not_smaller | Not_bigger | Unsure
+type hint = Incompatible | Maybe_bigger | Maybe_smaller | Unsure
 
 val pp_hint : hint Fmt.t
 val combine_hint : hint -> hint -> hint

test/unit_tests/test_matching.ml

@@ -41,7 +41,7 @@ let matching =
   CCList.map (make_test Matching_equiv) equal_tests
   @ CCList.map (make_test Smaller) smaller_tests
   @ CCList.map (make_test Bigger) bigger_tests
-  @ CCList.map (make_test Uncomparable) uncomparable_tests
+  @ CCList.map (make_test Incomparable) uncomparable_tests
 
 let () = add_tests "Acic.compare" matching
 
@@ -51,20 +51,22 @@ let unsure =
     ("int * bool -> int", "bool -> int -> int");
   ]
 
-let not_bigger =
+let maybe_smaller =
   [
     ("int * int -> int -> float", "(int -> int) -> float");
     ("int * bool -> int", "'a -> int");
   ]
 
-let not_smaller =
+let maybe_bigger =
   [
     ("(int -> int) -> float", "int * int * 'a -> float * int");
     ("'a -> 'b", "float list");
+    ("'b -> 'a", "int -> 'a");
+    ("int -> 'a", "float * int -> 'a");
     ("'a -> 'b", "int * float list -> 'a");
   ]
 
-let uncompatible = [ ("float", "int"); ("'a -> 'a * int list", "float list") ]
+let incompatible = [ ("float", "int"); ("'a -> 'a * int list", "float list") ]
 let comp' = Alcotest.testable Acic.pp_hint ( = )
 
 let match_feat =
@@ -80,9 +82,9 @@ let match_feat =
     Alcotest.test_case (CCInt.to_string !test_cnt) `Quick test
   in
   CCList.map (make_test Unsure) unsure
-  @ CCList.map (make_test Uncompatible) uncompatible
-  @ CCList.map (make_test Not_bigger) not_bigger
-  @ CCList.map (make_test Not_smaller) not_smaller
+  @ CCList.map (make_test Incompatible) incompatible
+  @ CCList.map (make_test Maybe_smaller) maybe_smaller
+  @ CCList.map (make_test Maybe_bigger) maybe_bigger
 
 let () = add_tests "MatchFeat.compatible" match_feat