This series of blog post aims to give a short weekly glimpse into my (Florian Angeletti) daily work on the OCaml compiler. This week, the focus is on compiler messages and backward compatibility.

A tag for quoting inline code

Last week, while I was investigating the breaking change in behavior for polymorphic variants, I have also started a much more boring change: uniformizing the quoting style for inline code in the compiler messages.

Currently, this quoting style is mostly left to the appreciation of authors of every compiler messages. This has lead the OCaml compiler messages to be quite heterogeneous, with different messages using "...", other '...', or `...', depending on the preference of the initial author.

To make the compiler message, I spent the time to introduce a new inline_code tag in the set of Format tags used by the compiler.

With this new tag, the compiler message

fprintf ppf "The external function `%s' is not available" s

can be rewritten as

fprintf ppf "The external function %a is not available" Style.inline_code s

which has the advantage of centralizing the styling of inline code fragment in a single location. In particular, this means that we could adapt the styling to the rendering medium (fancy terminal could use fancy styling while basic terminal use a textual quote).

My proposal with this change is currently available as a pull request.

Cleaning-up error messages

Adding an inline_code tag was also a good occasion to spot small mistakes in error messages. For example, the error message for non-overriding inheritance

class empty = object end
class also_empty = object inherit! empty end

lost a word at some point it time, yielding the following error message

Error: This inheritance does not override any method instance variable

which may confuse reader wondering what is a method instance variable. The sentence is quite easier to read once we add back the missing and and plurals

Error: This inheritance does not override any methods or instance variables.

Backward compatibility and polymorphic variants

As discussed last week, I have been working with Gabriel Scherer on a way to preserve backward compatibility for programs that mix open polymorphic variant types and explicit polymorphic annotation in OCaml 5.1:

let f : 'a. [> `X of 'a ] -> 'a = function (`X x) -> x | _ -> assert false

The backward compatibility hack that we came up with last week is to automatically add the missing annotations:

let f : 'a 'r. ( [> `X of 'a ] as 'r ) -> 'a = function (`X x) -> x | _ -> assert false

However, while writing a description of this hack in my pull request, I realized that this change was breaking backward compatibility in another corner case:

let f: 'b. [> `Foo ] -> 'b -> 'b = fun (`Bar|_) x -> x

Here the issue is that writing such type annotation let the typechecker infers that the real type of the row variable is [> `Foo | `Bar` ]

let f: 'b. [> `Foo | `Bar ] -> 'b -> 'b = fun (`Bar|_) x -> x

and not just [> `Foo ]. However, with our hack, this code will be converted to

let f: 'b 'r. ([> `Foo  ] as 'r) -> 'b -> 'b =  fun (`Bar|_) x -> x

where suddenly we cannot widen [> `Foo ] to [> `Foo | `Bar` ]. And thus the line above fails to compile with

Error: This pattern matches values of type [? `Bar ]
       but a pattern was expected which matches values of type [> `Foo ]
       The second variant type is bound to the universal type variable 'a,
       it may not allow the tag(s) `Bar

To avoid this regression, Jacques Garrigue proposed to only add annotations to polymorphic variant types that contains references to universal type variables. In other words, with this updated rule

let f: 'b. [> `Foo ] -> 'b -> 'b = fun (`Bar|_) x -> x

is kept unchanged because [> `Foo ] does not point to 'b (or any universally quantified type variables).

Contrarily

let f : 'a. [> `X of 'a ] -> 'a = function (`X x) -> x | _ -> assert false

is transformed into

let f : 'a 'r. ([> `X of 'a ] as 'r) -> 'a = function (`X x) -> x | _ -> assert false

because [> `X of 'a ] refers to the explicitly quantified type variable 'a.

Moreover, this rule is still well behaved in presence of nested explicitly polymorphic annotations. For instance, looking at

let nested: 'a.
  <m: 'b.
     <n:'irr. ('irr -> unit) * ([> `X of 'a | `Y of 'b ] -> 'a) >
  > -> 'a  = fun o -> (snd o#m#n) (`Y 0)

we can see that the nearest explicit annotation where all universal variables involved in [> `X of 'a | `Y of 'b] are bound is the one the method m. Thus the type above is equivalent with the new rule to:

let nested : 'a.
  < m : 'r 'b.
      < n : 'irr. ('irr -> unit) * (([> `X of 'a | `Y of 'b ] as 'r) -> 'a) >
> -> 'a = ...

On the one hand, I am not sure if the restoration of backward compatibility in OCaml 5.1 is really worth the complexity of this new rule. On the other hand, the new rule is conservative enough that we could use it to emit warnings or hint messages with a sensible resolution if the missing feature for constrained abstract types lands in OCaml.