Comment author: @garrigue

Fixed for upcoming 3.12.

Ctype.non_recursive_abbrev and Ctype.cyclic_abbrev should use try_expand_once_opt
and expand_abbrev_opt, as later phases of the compiler may have to expand a type
using those operations.

Comment author: yziquel

I noticed that this issue has been closed. Upgrading to 3.12, I understood that "closed" meant that this recursive subtyping is simply disallowed, and fails with "the type abbreviation tau is cyclic" error message.

I would dearly like to be able to do such a recursive subtyping. Is there any deep reason to disallow this? Could I expect to see such subtyping to be allowed in the future?

In my specific case, this is really useful, as it allows me to play very nicely with the possibly very horrible type systems of dynamically typed languages when binding interpreters of foreign languages. Just say "subtype to" is really cleaner than using Obj.magic or similar %identity functions when switching type systems...

Comment author: @garrigue

I noticed that this issue has been closed. Upgrading to 3.12, I understood that "closed" meant that this recursive subtyping is simply disallowed, and fails with "the type abbreviation tau is cyclic" error message.

I would dearly like to be able to do such a recursive subtyping. Is there any deep reason to disallow this? Could I expect to see such subtyping to be allowed in the future?

Well, "simply disallowing" it required to track it down...

More seriously, the compiler is allowed internally to expand private
abbreviations (this is the whole of their being "private" rather than
"abstract"). Since your wrapped expands to sexp which expands to
wrapped, it is not well-founded, and this is not allowed (even if
you use the -rectypes option).

So, sorry, I don't see how we could allow that.

Comment author: yziquel

This is perhaps too far fetched, but perhaps the issue is precisely that "private" means "expanding".

In a sense, if expanding simply means "rewrite", then yes, if you have recursive subtyping between a and b, they should naturally be identified (I guess), and there wouldn't be any need to do recursive subtyping.

However, it could perhaps be argued that "expanding" / "rewriting" is too strong. In the case of recursive subtyping, for instance of 'a t1 to t2 and of t2 to 'a t1, we could ask to allow only one subtyping, or both, depending on what we want to do. To do that, we should let the compiler know that there are two types and one-way subtyping, or equality. But it shouldn't be handled by syntactic rewriting but perhaps on a more logical level.

Perhaps I'm missing the whole point here, but I'd appreciate your view on that.

The whole point here is to be able to implement cleanly "type-inference barriers".

Comment author: @garrigue

I agree with you that there are times when one would like to be able
to define completely opaque type abbreviations.
You can already to this by writing
type -'a wrapped = private Wrap of sexp
Of course this means that the internal representation of sexp and
wrapped is going to differ, but I would say this is a compiler problem,
not a type system one.
Another appraoch might be to make private abbreviations completely
opaque (never expanded), but this goes against another of their goals,
which is to make them transparent enough to allow optimizations, which
in turn requires to be able to expand them.