When type checking goes wrong, but keeps going
Senior Software Engineer
Merlin, the foundational library that underpins the reference implementation of the OCaml Language Server Protocol, provides a wide range of practical features, including commands, code completion, and much more. It also implements more subtle mechanisms that are essential to delivering a smooth and responsive editing experience. Indeed, the editing environment for a programming language closely resembles the front-end of its compiler. However, whereas a compiler operates on complete, syntactically valid programs, an editor must continuously cope with programs that are incomplete, temporarily inconsistent, and often ill-typed.
To handle these transient states, Merlin vendors a modified version of the OCaml compiler front-end (primarily the parser and the type checker), extending it with two recovery mechanisms:
-
Parsing Recovery, which synthesizes AST nodes to allow parsing to continue even in the presence of syntax errors.
-
Typing Recovery, which synthesizes typed AST nodes, allowing type checking to continue even when type errors are encountered. In this article, we will focus specifically on this second mechanism.
These two mechanisms are possible because Merlin vendors a modified version of the OCaml compiler's front-end. Their behavior is easy to observe in practice. Consider, for example, the following OCaml program:
let x = "ten"
let y = x + 20
let z = (y + (2 * x)) && true
Here, we are faced with three type errors. First, we attempt to add
x and 20, which makes no sense since x has type string. Next,
we attempt to multiply x (once again) by 2, which is also
invalid. Finally, the expression (y + (2 * x)), which is expected to
have type int, is instead used as a boolean value.
When compiling this program, the OCaml compiler reports only the first type error in the compilation unit:
File "lib/test.ml", line 2, characters 8-9:
2 | let y = x + 20
^
Error: The value x has type string but an expression was expected of type int
This is a very sensible design choice. Although OCaml has a highly sophisticated type system, the language's pervasive type inference means that a single mistake can easily trigger a cascade of secondary errors, obscuring the compiler's primary goal: ensuring correctness.
However, applying the same strategy in a code editor raises two major (and closely related) issues:
-
An editor that reported errors one at a time would provide a rather poor user experience.
-
More importantly, if type checking or parsing stopped at the first syntax or type error, every feature provided by Merlin that relies on compiler artifacts—namely the parsetree and the typedtree—would immediately become unavailable. This would be particularly frustrating because, while actively editing a file, the program is almost always in a temporarily invalid state, whether syntactically, semantically, or both.
For these reasons, the modified version of the OCaml compiler front-end embedded in Merlin always produces valid ASTs and typed ASTs, allowing the subsequent analysis phases to continue operating on programs that are still being written:
"
These two mechanisms, although arguably among the most interesting features of the language server, are also one of the main reasons why upgrading Merlin to support a new OCaml release is such a challenging process. This effort, known as OCaml Release Readiness, will be the subject of a future blog post. For now, let's take a closer look at why this is the case by focusing specifically on Typing Recovery.
Adapting Typing Recovery Across OCaml Versions
Without going into too much detail, upgrading Merlin to a new OCaml version involves applying patches coming from two different sources:
- compiler patches, corresponding to the various changes made to OCaml over time;
- Merlin patches, which introduce the recoveries.
Because Typing Recovery is deeply intertwined with the various modules involved in OCaml's type checking process, applying patches from two different sources (with different development cycles) makes version upgrades particularly tedious and introduces two major challenges:
-
each upgrade takes time, because the vendored version of the compiler front-end must be adapted while preserving all recovery information and fixing the analysis issues naturally introduced by the evolution of OCaml;
-
handling new recovery cases can be tedious for the people responsible for the upgrade process. Indeed, it is common to apply patches from the compiler side without having a complete understanding of their underlying rationale. For example, OCaml
5.5recently introduced a new feature that was highly anticipated by the community: module dependent functions. This addition changes how function parameters are handled and requires careful consideration of how recovery should behave in these new situations.
For these reasons, Typing Recovery could become unstable (within reasonable scenarios, of course), sometimes introducing small regressions and sometimes lacking support for newly introduced features.
Reducing the Differences Between Merlin and OCaml
Reducing the differences between Merlin's vendored version of the front-end and the one maintained by OCaml is therefore a crucial task. It not only helps reduce Merlin's maintenance burden, but also gives OCaml maintainers more control over how they want recovery to be handled within the type checker.
Of course, this represents an additional responsibility for the maintainers (another one!), but in practice, developers introducing new features in the type checker usually have both a deep understanding of their implementation and a good intuition about how recovery should behave in the presence of errors.
Integrating Typing Recovery into the Compiler
At the time of writing this blog post, the Typing Recovery mechanism has been merged into the compiler. In this section, we will briefly describe its redesign and direct integration into the compiler's type checker.
Typing Recovery has been part of Merlin since its very beginning. Although its implementation relies on a very clever encoding, it has aged over time, and its underlying design has become increasingly difficult to understand. Integrating it into the compiler therefore provided an opportunity to rethink the mechanism, clean it up, and make its behavior easier to understand. The goal was to enable a non-intrusive integration, giving maintainers the tools they need to confidently evolve and maintain it in the future.
How Recovery Works, at a High Level
The core of the OCaml type-checker is implemented as a set of recursive functions responsible for typing the different syntactic categories of the language, notably expressions, patterns, type declarations, modules, and classes. When a type error is encountered, these functions propagate an exception that interrupts the construction of the typing derivation. The compiler thus adopts a first-failure reporting strategy, consisting in reporting only the first encountered error. This approach is particularly well suited to OCaml, whose type system based on inference makes it difficult to continue analysis without risking the propagation of imprecise diagnostics. This approach is particularly well suited to OCaml, whose type system based on inference makes it difficult to continue analysis without risking the propagation of imprecise diagnostics.
To go beyond the first-failure reporting strategy, Merlin instruments the main recursive functions of the type-checker in order to intercept typing exceptions. When an exception is raised, it is caught so that it can be recorded, and typing then resumes at the recursive call level (locally) on the other independent subterms of the program. Thus, even if the typing of a subexpression fails, independent subtrees can still be analyzed, which makes it possible to report multiple typing errors within a single analysis.
Resuming recursion allows new errors to be discovered, but is not
sufficient to produce an exploitable Typedtree. When a
sub-derivation fails, Merlin synthesizes an artificial Typedtree
node whose typing judgment is that expected by the context in which it
is inserted, while also preserving the fragments of the derivation
that could be constructed before the typing failure, even if their
attachment to the rest of the tree is no longer known. These nodes
help preserve the structure of the Typedtree returned by the
type-checker and maintain language server functionality despite the
presence of errors.
However, these generic mechanisms are not sufficient to cover all language constructs. Some phases of the type-checker perform preliminary checks before recursively typing their subterms. When these checks fail, recursion is never engaged and no partial derivation is produced. For example, record expressions:
{ my_fst_field = e1;
my_snd_field = e2 }
The type-checker first attempts to resolve my_fst_field and
my_snd_field. If, for instance, my_fst_field does not exist, it
gives up without attempting to type e1 and e2. This strategy is
suboptimal: subexpressions are never analyzed even though they could
contain useful information or independent errors. To address this
issue, Merlin delays the error by assuming that the field exists.
Merlin then temporarily adapts the type-checker by considering that an unknown label is not necessarily a fatal error, but may correspond to a field that will be added later. Typing then proceeds under this assumption, which makes it possible to produce partial derivations for subexpressions and to improve the quality of diagnostics.
An other API for raising Type Errors
In order to make error handling explicit, we introduce two functions
intended to replace direct calls to raise in the type-checker. When
the -typing-recovery flag is not enabled, these functions behave
exactly like raise. In Typing Recovery mode, they record the
exception in a dedicated structure, which will then be processed by
the recovery handler.
-
Typing_recovery.log_and_raiserecords the exception before re-raising it. It is used when processing cannot continue locally and captures the general case; -
Typing_recovery.log_or_raiserecords the exception without re-raising it when the context is able to perform local recovery, for example by synthesizing an artificial node or by continuing the typing of other subterms; it captures more fine-grained cases.
This distinction makes explicit the points where recovery is possible and those where the exception must necessarily be propagated. The API thus guides the implementation of the type-checker and makes recovery decisions visible when adding or modifying typing rules.
Today, we do not have a formal criterion to systematically determine which function to use. The integration into the OCaml type-checker was therefore guided by a large set of unit tests and empirical validation. In practice, the choice between the two functions depends on the expected behavior of recovery and is validated by observing the produced diagnostics. This lack of a general criterion aligns with the observations of the paper Merlin: A Language Server for OCaml (Experience Report), who note that recovery policies would benefit from a more systematic theoretical framework.
Forcing User-Facing Error Reporting
In Merlin’s historical implementation, the selection of exceptions eligible to trigger a Typing Recovery scenario was mainly based on an empirical approach. The reimplementation in the compiler made it possible to identify a simple design invariant: only exceptions intended to be reported to the user (user-facing errors) should be recorded by the recovery mechanism. Conversely, internal type-checker exceptions, as well as simply re-raised exceptions (reraise), must not be captured.
To introduce recovery as a systematic approach, we aim to channel
user-facing exceptions so that they are always handled through a
pair of functions log_and_raise and log_or_raise. To achieve this,
we rely on a property of the OCaml language: exceptions are
represented by the extensible type
exn. This
representation makes it possible to control the introduction of new
exception constructors via module interfaces. By making certain
exception constructors private in a module signature, it becomes
possible to forbid their construction outside this module, while still
allowing them to be deconstructed through pattern matching or
exception handlers. This technique thus makes it possible to structure
the flow of user-facing errors and to enforce a systematic passage
through the associated logging functions.
- exception Error of error
+ module Error : sig
+ type exn += private In_context of error
+ end = struct
+ type exn += In_context of error
+
+ let log_or_raise err =
+ Type_recovery.log_or_raise (In_context err)
+
+ let log_and_raise err =
+ Type_recovery.log_and_raise (In_context err)
+ end
This transformation also makes it straightforward to rely on the compiler to guide the implementation by identifying and handling every possible recovery case individually and give a precise API to deal with recovery with resumption or not.
Closing words and Acknowledgments
Although there are still some differences between Merlin's vendored
front-end and the one maintained by OCaml, this change has already
significantly reduced the number of Merlin patches that need to be
applied. In the future, this will greatly simplify the process of
upgrading to new OCaml versions. We recently provided a Merlin
branch that anticipates the
5.6 release and relies on the new Typing Recovery mechanism!
Although the next version of OCaml will expose the -typing-recovery
flag to enable this mechanism, the goal is not for developers to use
it directly, but rather for it to be leveraged by tools such as
Merlin.
Historically, Typing Recovery was designed and maintained by Merlin's two creators, Frédéric Bour and Thomas Refis. It was also maintained over the years by Ulysse Gérard. The integration into the compiler was funded by Jane Street. The review, conducted by Thomas Refis (who contributed greatly to knowledge transfer and design discussions), was funded by The OCaml Software Foundation. We would also like to thank Florian Angeletti for his quick review, guidance, and detailed explanations.
This work is part of the broader effort to reduce the gap between OCaml and Merlin, and it is probably one of the most significant steps in that direction. We believe that the integration was carried out in a smooth and non-intrusive way, minimizing the impact on maintenance work while drastically reducing the difficulty of future version upgrades. This will allow us to focus on delivering the best possible experience and continuously improving the OCaml code editing experience.
Stay Tuned.
Stay In Touch!
Tried out the new update? Connect with us on Bluesky, Mastodon, Threads, and LinkedIn or sign up for our mailing list to stay updated on our latest projects. You can also connect with other OCaml users on Discuss. We look forward to hearing your thoughts!
Open-Source Development
Tarides champions open-source development. We create and maintain key features of the OCaml language in collaboration with the OCaml community. To learn more about how you can support our open-source work, discover our page on GitHub.
Explore Commercial Opportunities
We are always happy to discuss commercial opportunities around OCaml. We provide core services, including training, tailor-made tools, and secure solutions. Tarides can help your teams realise their vision
Stay Updated on OCaml and MirageOS!
Subscribe to our mailing list to receive the latest news from Tarides.
By signing up, you agree to receive emails from Tarides. You can unsubscribe at any time.