Re: [Caml-list] Equality between abstract type definitions

[Andreas Rossberg <rossberg@mpi-sws.org>]

On Oct 25, 2013, at 01:23 , Jacques Garrigue <garrigue@math.nagoya-u.ac.jp> wrote:
> In OCaml, type variables used in type annotations are just unification variables:
> the type checker is allowed to merge them or instantiate them.
> This is useful when you want to indicate that two things have the same type,
> without writing the type by hand.

Jacques, do you think there is any chance that this will ever be changed? I think this keeps being one of the most annoying pitfalls in the OCaml type system, not what most people expect, and in 98% of the cases, not what they want either -- especially since there often is no convenient way to actually express what they want.

A simple proposal, which I'm sure has been made many times before, would be to interpret type variables of the form 'a, 'b as proper universal variables, and only ones of the form '_a, '_b as unification variables. That matches the notation that OCaml has always been using in its output. More expressive and clearer signalling of intent.

Obviously, such a change would break some code, code that actually relies on 'a being just a unification variable. But my optimistic guess is that such code is rather rare. And it would be trivial to adapt.

It would also break code that assumed the wrong behaviour and only compiled by accident (such as the Peter's example). But arguably, that's a good thing, because it uncovers actual bugs.

Anyway, just dreaming aloud… :)

/Andreas