Re: [Caml-list] typing problem with sexplib and mutually recursive polymorphic types

[Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>]

From: Markus Mottl <markus.mottl@gmail.com>
> On Wed, Mar 11, 2009 at 12:16, Damien Doligez <damien.doligez@inria.fr> wrote:
> > That is not quite true any more.  For example, I changed the
> > type-checker a few years ago to start with the user-provided type
> > when typing a let rec, in order to be able to debug my large
> > recursive definitions.  Note that I didn't do that from scrach,
> > I used an infrastructure that was already present for seeding the
> > type inference in some cases.  IIRC, it is there for some object-
> > oriented reason.
> 
> Interesting, this change seems to have passed unobserved by me and is
> certainly a great debugging aid.  Does this mean that eventually
> polymorphic recursion might be supported by OCaml?  What's still
> missing for that feature?

Actually I added universal type annotations and polymorphic recursion
in a branch a few years ago. The idea was to provide a basis for
implementing GADTs. But since the GADT work was not finished, it was
never merged in the main trunk.

So it would be very easy to have polymorphic recursion in ocaml.
The real question is whether it is that useful in the absence of
GADTs, knowing that you can already do it in a somewhat verbose way.

Cheers,

Jacques Garrigue