feat: improve the Arrow solver.

In the arrow solver, if there is only 1 argument, it was considered as a tuples, adding more equation to the AC solver. But it should not be treated as such and more should had the correct equality.
Drup · Oct 28, 2024 · 76380fd · 76380fd
1 parent 99f6d1d
commit 76380fd
Show file tree

Hide file tree

Showing 4 changed files with 26 additions and 33 deletions.
diff --git a/lib/unification/ArrowTerm.ml b/lib/unification/ArrowTerm.ml
@@ -1,5 +1,5 @@
 type t = {
-  args: ACTerm.t;
+  args: Type.NSet.t;
   ret: Type.t;
 }
 
@@ -12,7 +12,7 @@ let make args ret : t = {args; ret}
 
 let pp ppf self =
   Fmt.pf ppf "%a -> %a"
-    Fmt.(array ~sep:(any " * ") Type.pp) self.args
+    Fmt.(array ~sep:(any " * ") Type.pp) (Type.NSet.as_array self.args)
     Type.pp self.ret
 
 let make_problem left right = {left; right}

diff --git a/lib/unification/ArrowTerm.mli b/lib/unification/ArrowTerm.mli
@@ -1,7 +1,7 @@
 (** Term and Problem for arrows *)
 
 type t = {
-  args: ACTerm.t;
+  args: Type.NSet.t;
   ret: Type.t;
 }
 
@@ -10,7 +10,7 @@ type problem = {
   right: t;
 }
 
-val make : Type.t array -> Type.t -> t
+val make : Type.NSet.t -> Type.t -> t
 val pp : t Fmt.t [@@ocaml.toplevel_printer]
 val make_problem : t -> t -> problem
 val pp_problem : problem Fmt.t [@@ocaml.toplevel_printer]
diff --git a/lib/unification/Syntactic.ml b/lib/unification/Syntactic.ml
@@ -126,8 +126,8 @@ and insert_rec env stack (t1 : Type.t) (t2 : Type.t) : return =
       debug (fun m -> m "Arrow|Arrow");
       (* TODO: if ret1 and ret2 for sure cannot be unified with an arrow, we can decompose
          the problem already *)
-      Env.push_arrow env (ArrowTerm.make (Type.NSet.as_array arg1) ret1)
-                         (ArrowTerm.make (Type.NSet.as_array arg2) ret2);
+      Env.push_arrow env (ArrowTerm.make arg1 ret1)
+                         (ArrowTerm.make arg2 ret2);
       process_stack env stack
   (* Two tuples, (s₁,...,sₙ) ≡ (t₁,...,tₙ) *)
   | Tuple s, Tuple t ->

diff --git a/lib/unification/Unification.ml b/lib/unification/Unification.ml
@@ -30,6 +30,9 @@ let rec solve_tuple_problems env0 =
 and solve_arrow_problem env0 { ArrowTerm.left; right } =
   (* AL -> BL ≡? AR -> BR *)
   let pb = CCFormat.sprintf "%a" ArrowTerm.pp_problem {ArrowTerm.left; right} in
+  let solve_args env args1 args2 =
+    insert env (Type.tuple (Env.tyenv env) args1) (Type.tuple (Env.tyenv env) args2)
+  in
   Trace.wrap_iter ~__FUNCTION__ ~__FILE__ ~__LINE__ __FUNCTION__
     ~data:(fun () ->
       [
@@ -46,40 +49,34 @@ and solve_arrow_problem env0 { ArrowTerm.left; right } =
           (* AL ≡? AR  ∧  BL ≡? BR *)
           Trace.with_span ~__FUNCTION__ ~__FILE__ ~__LINE__
             "AL ≡? AR  ∧  BL ≡? BR" (fun _sp ->
-              Env.push_tuple env left.args right.args;
+              let* () = solve_args env left.args right.args in
               let* () = insert env ret_type left.ret in
-              insert env ret_type right.ret) );
+              insert env ret_type right.ret
+          ) );
       ( "AL * αL ≡? AR  ∧  BL ≡? αL -> BR",
         fun env () ->
           (* AL * αL ≡? AR  ∧
              BL ≡? αL -> BR
           *)
           Trace.with_span ~__FUNCTION__ ~__FILE__ ~__LINE__
             "AL * αL ≡? AR  ∧  BL ≡? αL -> BR" (fun _sp ->
-              let var_arg_left = Env.gen Variable.Flags.empty env in
-              Env.push_tuple env
-                (ACTerm.add left.args (Type.var (Env.tyenv env) var_arg_left))
-                right.args;
+              let ty_arg_left = Type.var (Env.tyenv env) (Env.gen Variable.Flags.empty env) in
+              let* () = solve_args env (Type.NSet.add ty_arg_left left.args) right.args in
               let* () = insert env ret_type right.ret in
               insert env left.ret
-                (Type.arrow (Env.tyenv env)
-                   (Type.var (Env.tyenv env) var_arg_left)
-                   right.ret) ) );
+                (Type.arrow (Env.tyenv env) ty_arg_left right.ret) ) );
       ( "AL ≡? AR * αR  ∧  αR -> BL ≡? BR",
         fun env () ->
           (* AL ≡? AR * αR  ∧
              αR -> BL ≡? BR
           *)
           Trace.with_span ~__FUNCTION__ ~__FILE__ ~__LINE__
             "AL ≡? AR * αR  ∧  αR -> BL ≡? BR" (fun _sp ->
-              let var_arg_right = Env.gen Variable.Flags.empty env in
-              Env.push_tuple env left.args
-                (ACTerm.add right.args (Type.var (Env.tyenv env) var_arg_right));
+              let ty_arg_right = Type.var (Env.tyenv env) (Env.gen Variable.Flags.empty env) in
+              let* () = solve_args env left.args (Type.NSet.add ty_arg_right right.args) in
               let* () = insert env ret_type left.ret in
               insert env right.ret
-                (Type.arrow (Env.tyenv env)
-                   (Type.var (Env.tyenv env) var_arg_right)
-                   left.ret) ) );
+                (Type.arrow (Env.tyenv env) ty_arg_right left.ret) ) );
       ( "AL * αL ≡? AR * αR  ∧  BL ≡? αL -> β  ∧  αR -> β ≡? BR",
         fun env () ->
           (* AL * αL ≡? AR * αR  ∧
@@ -88,23 +85,19 @@ and solve_arrow_problem env0 { ArrowTerm.left; right } =
           *)
           Trace.with_span ~__FUNCTION__ ~__FILE__ ~__LINE__
             "AL * αL ≡? AR * αR  ∧  BL ≡? αL -> β  ∧  αR -> β ≡? BR" (fun _sp ->
-              let var_arg_left = Env.gen Variable.Flags.empty env in
-              let var_arg_right = Env.gen Variable.Flags.empty env in
+              let ty_arg_left = Type.var (Env.tyenv env) (Env.gen Variable.Flags.empty env) in
+              let ty_arg_right = Type.var (Env.tyenv env) (Env.gen Variable.Flags.empty env) in
               (* TOCHECK *)
-              Env.push_tuple env
-                (ACTerm.add left.args (Type.var (Env.tyenv env) var_arg_left))
-                (ACTerm.add right.args (Type.var (Env.tyenv env) var_arg_right));
+              let* () =
+                solve_args env (Type.NSet.add ty_arg_left left.args)
+                (Type.NSet.add ty_arg_right right.args)
+              in
               let* () =
                 insert env left.ret
-                  (Type.arrow (Env.tyenv env)
-                     (Type.var (Env.tyenv env) var_arg_left)
-                     ret_type)
+                  (Type.arrow (Env.tyenv env) ty_arg_left ret_type)
               in
               insert env
-                (Type.arrow (Env.tyenv env)
-                   (Type.var (Env.tyenv env) var_arg_right)
-                   ret_type)
-                right.ret ) );
+                (Type.arrow (Env.tyenv env) ty_arg_right ret_type) right.ret) );
     ]
   in
   potentials |> Iter.of_list