Unify returns result rather than raising an exception #14425

samsa1 · 2025-12-18T08:27:14Z

I have noticed that almost all calls to unify are directly wrapped inside an exception handler. The cases where we don't have a direct exception handler are the exception that most of the time just expect the unification to never fail.

As such I propose to replace the exception by returning a result. As such the type-checker will help prevent in any future evolution any uncaught exception.

In order to stay as close as possible to the actual semantic I introduced a unify_ex (and a unify_var_ex) that returns an exception for the few cases where we didn't have a direct exception handler. A futur improvement might be to remove this function from the interface of ctype.ml and adding assertions in places we expect that the unification will never fail.

This PR is reviewed on top of #14422

…rather than an exception

gasche · 2025-12-18T08:29:26Z

I would prefer _exn as the exception prefix, as that convention already exists in some parts of the compiler codebase.

johnyob · 2025-12-18T08:32:20Z

I would prefer _exn as the exception prefix, as that convention already exists in some parts of the compiler codebase.

Was literally writing the same comment 😅

johnyob · 2025-12-18T08:34:38Z

typing/ctype.mli

+val unify_ex: Env.t -> type_expr -> type_expr -> unit
        (* Unify the two types given. Raise [Unify] if not possible. *)
+val unify: Env.t -> type_expr -> type_expr ->
+        (unit, Errortrace.unification_error) Result.t


nit: prefer result over Result.t

I would cite that this is consistent with the compiler codebase, but the compiler uses both result and Result.t haphazardly ://

A side question is do we want to define a local allias for the type ('a, Errortrace.unification_error) Result.t such as ' unification_result ?

This would also be a nice pattern to use within the compiler :) e.g. 'a Errortrace.unification_result

johnyob · 2025-12-18T08:39:58Z

typing/typeclass.ml

+  if Result.is_error (Ctype.unify env self_type sign.csig_self) then
+    raise(Error(sty.ptyp_loc, env, Pattern_type_clash self_type));


My first reaction to this pattern was 'there must be a Result.ok_or_else combinator for this', but I was wrong

Also this PR uses match ... with Ok () -> () | Error err -> raise ... a lot, why switch it up here?

gasche

After looking at the patch, I believe that it is correct but I am also not fully convinced that the change is necessary / obviously an improvement. The fact that unify returned unit before made some patterns convenient, for example

try unify <args>
with Unify err -> <error case>

becomes the more boilerplate-y

match unify <args> with
| Ok () -> ()
| Error err -> <error case>

This is not a negative vote, but let's say I would be waiting for someone else to express clear support.

gasche · 2025-12-18T08:37:16Z

utils/misc.ml

+        ([], []) -> Ok ()
+      | (a1::l1, a2::l2) ->
+        Result.bind (f a1 a2) (fun () -> iter2_result f l1 l2)
+      | (_, _) -> raise (Invalid_argument "iter2_result")


I feel slightly nervous about the fact that these functions are not self-recursive on the nose: they are tail-recursive but go via an indirect call by the higher-order function Result.bind, so they are not going to be tail-recursive with js_of_ocaml. This may or may not be something we care about depending on the usage and circumstances (this is not a stdlib addition), but in this case it's trivial to make this issue go away by inlining the call to Result.bind. Could you do this?

Alternatively, the iter and iter2 functions could be used with a local exception that is raised and caught on the error path? Not entirely sure what this would look like on js_of_ocaml, but has the benefit of reusing the Stdlib iter and iter2?

gasche · 2025-12-18T08:39:06Z

toplevel/topprinters.ml

+          (make_printer_type ty_arg)
+          (Ctype.instance ty)
+      in
+      unify_res, ty_arg


Conceptually this is a bit ugly because the ty_arg argument makes no sense in the error case. I would prefer:

let open Result.Syntax in let ty_arg = Ctype.newvar () in let+ () = Ctype.unify ... in ty_arg

gasche · 2025-12-18T08:43:59Z

typing/typecore.ml

+  | Error err ->
      raise(Error(loc, env, Expr_type_clash(err, None, None)))
-  | Tags(l1,l2) ->
+  | exception Tags(l1,l2) ->


Ah, of course unify raises another possible exception, Tags ..., which is undocumented in the .mli, has an unclear status (it has its own error handler registered by the compiler... but is also rewrapped as another error in some cases), and remains raised as an exception rather than being part of the Error cases.

I think that the choice that you made to leave it as an exception is the correct one, and it's not your fault that it was never documented in the first place, but could you mention it in ctype.mli?

johnyob · 2025-12-18T08:46:15Z

typing/typecore.ml

                  Warnings.Ignored_extra_argument;
-              unify env ty_fun
-                (newty (Tarrow(lbl,ty_param,ty_res,commu_var ())));
+              Result.get_ok


Perhaps we should use set_type_desc here instead of unify?

johnyob · 2025-12-18T08:49:46Z

typing/typecore.ml

-              try unify env (type_option ty_default) ty_arg_mono
-              with Unify _ -> assert false;
-            end;
+            Result.get_ok (unify env (type_option ty_default) ty_arg_mono);


Shouldn't this be assert (Result.is_ok ...)?

As an occasionally -noassert-paranoid person, I would not recommend sticking important side-effects inside assertions.

My problem: the Invalid_argument raised by Result.get_ok will be less helpful than the original assert false in diagnosing any issue with the (undocumented) invariant here

johnyob · 2025-12-18T09:09:56Z

Agreeing with @gasche here, the patch looks correct. I do believe the change is an improvement (the use of a result here forces me to handle the error case, which I may forget about w/out LSP to quickly look at the documentation).

However, I also agree with @gasche that the translation of

try unify <args>
with Unify err -> <error case>

into the more boilerplate-y

match unify <args> with
| Ok () -> ()
| Error err -> <error case>

is unpleasant.

In Rust, you'd probably write something along the lines of Result.get_ok_or (unify <args>) ~else:(fun err -> <error case>) (with OCaml naming).

gasche · 2026-01-07T12:37:40Z

We discussed this again during the type-system meeting today. @samsa1 made the point that, even if it does not clearly improve the codebase, it does make it more approachable with newcomers. I find this a reasonable argument and will be happy to merge once the CI is green again.

garrigue · 2026-01-07T12:47:13Z

@gasche , you are a bit fast to approve.
Shouldn't the name exception version be changed to unify_exn at least ?
For the rest, I was planning to give it a look, but I suppose I can do it later (it is not going to break anything anyway).

garrigue · 2026-01-07T12:52:55Z

BTW, I found the place I was talking about.
This is expand_head_unif, in ctype.
This is one of the rare functions raising Unify, and it might benefit from the same change.

samsa1 added 4 commits December 16, 2025 15:31

Moved a match outside of an if in typetexp

fb3ec7a

Handled comments

f2ebfbd

Changed the interface of unify to return a result

e90ddb5

Changed the interface of unify_var and unify_gadt to return a result …

cfb788e

…rather than an exception

johnyob reviewed Dec 18, 2025

View reviewed changes

gasche reviewed Dec 18, 2025

View reviewed changes

johnyob reviewed Dec 18, 2025

View reviewed changes

gasche approved these changes Jan 7, 2026

View reviewed changes

nojb assigned gasche Jan 7, 2026

		if Result.is_error (Ctype.unify env self_type sign.csig_self) then
		raise(Error(sty.ptyp_loc, env, Pattern_type_clash self_type));

Unify returns result rather than raising an exception #14425

Are you sure you want to change the base?

Unify returns result rather than raising an exception #14425

Conversation

samsa1 commented Dec 18, 2025

Uh oh!

gasche commented Dec 18, 2025

Uh oh!

johnyob commented Dec 18, 2025

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

gasche left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

johnyob Dec 18, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

johnyob commented Dec 18, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

gasche commented Jan 7, 2026

Uh oh!

garrigue commented Jan 7, 2026

Uh oh!

garrigue commented Jan 7, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

johnyob Dec 18, 2025 •

edited

Loading

johnyob commented Dec 18, 2025 •

edited

Loading