We discussed in the past (see #5985 (comment) for example ) a more general feature,

new type <params> <tyname>
new type <params> <tyname> = <tyexpr>

In the second case, the type is defined to be convertible from and to the given <tyexpr>, but distinct from it (and from other new types defined in the same way): this is the minimal form of minimal types that one could consider. (The first case is equivalent to first defining a local abstract type and then taking a new nominal copy of it.)

Thank you for finding the reference.
However, new type alone does not solve the problem of creating incompatible types, i.e. types that are guaranteed to be distinct internally even if you got them from an opaque module. Interestingly, the only way I see to do that in the absence of a global namespace is structural rather than nominal.
I believe we already discussed unique types in the past, and there was maybe even a concrete proposal, but it was faster to just make a new proposal (that can be edited as you wish).

If only types of the form new type t (= tyexpr) can be given the interface new type t, then we know that the interface

new type t1
new type t2

must be implemented with

new type t1 (= ty1)
new type t2 (= ty2)

and therefore t1, t2 must be distinct, right?

You're meaning that they cannot be copied from one module to another?
This kind of defeats the power of the module system.
That is, the first definition of your type has to be in a public interface, or you're stuck, because you have no way to export it.

As a result, any unique type is incompatible with any non-abstract type, and two abstract types with different identifiers are incompatible.

How is this different from:

type zero = private Zero

For one thing, type zero = private Zero can be abstracted as type zero [@@immediate], which is (presumably) not the case with unique types.

But unique types do seem rather like "extra-private" types, with no constructors, no destructors, and no visible representation.

I'd missed this part:

As a result predefined types such as float or char are not treated specially, just declared unique.

So now I think I see what @garrigue is aiming for.

I've always thought that the problem with float and char was that we lacked "datatype definition kinds" (currently just "variant", "record" and "extensible variant") for those internal types, and that the right solution was just to add them. So extending:

and type_kind =
    Type_abstract
  | Type_record of label_declaration list  * record_representation
  | Type_variant of constructor_declaration list
  | Type_open

to

and type_kind =
    Type_abstract
  | Type_record of label_declaration list  * record_representation
  | Type_variant of constructor_declaration list
  | Type_open
  | Type_float
  | Type_string

However, the same basic issue arises for other forms of datatype. For example, Int32.t or Int64.t or anything using a custom block representation. So perhaps the correct thing to do is to allow external type declarations much like external value declarations.:

type float = external "float"

This is basically what @garrigue is proposing, but with what I think is a more intuitive syntax.

Reading back the discussion on new types, I've beefed up this proposal.
Now we also allow unique datatypes; i.e. anything that is nominal can be made unique when it is defined.

type 'a stack = {mutable c : 'a list} [@@unique]

Then it can be turned into a unique abstract type in the interface.

type 'a stack [@@unique "stack"]

To still guarantee than unique abstract types are incompatible with (non unique) datatypes, I require that the definition is forgotten together with the identity. I.e., the following is illegal:

module Stack : sig type 'a stack = {mutable c : 'a list} end =
  struct type 'a stack = {mutable c : 'a list} [@@unique] end

Additionally, uniqueness implies injectivity. Since all unique types are nominal from the start, they are by definition injective. This allows to define types that were not allowed before:

type _ t = T : 'a -> 'a Queue.t t

since Queue.t is marked as unique in the standard library. Before, there was an error message:

Error: In this definition, a type variable cannot be deduced
       from the type parameters.

See https://github.com/garrigue/ocaml/tree/unique-types/testsuite/tests/typing-unique for more examples.

Using @@unique for injectivity is an interesting idea. Is it supported for functor-abstracted types -- e.g. does the following work?

module F(X: sig type 'a t [@@unique] end) = ...

What is the use case for type 'a stack = {mutable c : 'a list} [@@unique]? From my perspective it doesn't make much sense.

Can we try and describe what [@@unique] semantically actually means rather than just listing its properties?

Is it supported for functor-abstracted types

I hope not. If we want to have abstraction over injective types then we should have specific syntax to mean "injective type" -- just like we do for say "covariant type".

I think the semantics are: "unique" means "generative". The name (string) refers to the generated identifier, which there's currently no way of mentioning in programs. So a generative type definition now has both an optional identifier and an optional representation.

That also means unique doesn't cover all use cases of injectivity. For example, type 'a t [@@unique] can't be instantiated with the injective definition type 'a t = 'a list because type aliases aren't generative.

It's not just a "name" field alongside the representation and equation though, because that wouldn't imply injectivity.

So far I don't see why we would prefer this to adding an additional external case to the representation.

Sorry, I started with something that was probably just your external proposal, and then looked at new types, and remembered the problem about the abstraction of concrete types.

I'll try to write a full explanation shortly, but to give you the gist of it, while I added it as an extra field in type_declaration, this is rather intended as a new case of type_manifest, aside of None and Some ty. I was just afraid of the extent of changes if I changed that type in the implementation.

It's not just a "name" field alongside the representation and equation though, because that wouldn't imply injectivity.

Answering my own implicit question, it is a name field alongside the representation and equation together with a requirement that any equations respect the name field (just as they currently respect the representation field). That is why you can't have non-injective types with a name.

Let me try to explain the current status, since it changed a bit since the original external type proposal.

Concept

The basic idea is to add a new case to type_manifest, between Some and None, adding a name that is only used when checking incompatibility of types in mcomp.
Two abstract or concrete datatypes with different names are incompatible, and additionally a named abstract type is incompatible with all unnamed datatypes, to preserve backward compatibility.
At this point, I do not allow refining a named abstract type during GADT unification, but this would probably be meaningful if they share the same name.

Introduction

This name must be introduced since the first definition of the type, either pure abstract (i.e. an abstract type defined in an implementation), or a datatype.

type 'a t [@@unique "foo"]
type 'u ab = A | B [@@unique "bar"]

Those types are indeed generative, but only in the sense that they are nominal.
Since the name appears in the source code (explicitly or implicitly), if such a type appears in the body of a generative functor, all its instances will be compatible (except if some other structural part of the type allows to distinguish them).

module F(X : sig type t end)() = struct type t = T of X.t [@@unique "F.t"] end

An aside of their being generative, is that they are injective in all their type parameters: there is no way to expand them.

One can define abbreviations of named types, public or private, that will still be recognized as named.
A special case is redefinition of datatypes with an equation. In that case, uniqueness must be indicated explicitly:

type 'a t = 'a ab = A | B [@@unique "bar"]

The reason for this repetition is that allowing writing the above without requiring uniqueness could result in forgetting it, if ab becomes abstract through hiding of its cmi for instance. So this is only a repetition of the information in ab, and not a change to the idea that we are extending type_manifest.

Subtyping

Uniqueness can be kept through subtyping. Aside of reflexivity, the following are allowed

type ('a1,...,'an) t = ('b1,...,'bm) u <: type ('a1,...,'an) t [@@unique s]
       if u is [@@unique s] and ('a1,...,'an) \subset ('b1,...,'bm)
type 'a t = A | B [@@unique s] <: type 'a t [@@unique s]
type 'a t = 'a u = A | B [@@unique s] <: type 'a t [@@unique s]
type 'a t = 'a u = A | B [@@unique s] <: type 'a t = A | B [@@unique s]

The inclusion condition is needed to preserve injectivity (it could be relaxed more).
Private types are expanded (i.e. u is actually the result of expanding the manifest type with expand_head_opt).
One important case is prohibited:

type 'a t = A | B [@@unique s] <\: type 'a t = A | B

is not allowed, because it would break the invariant that named abstract types and unnamed datatypes are always incompatible.

The above subtyping rules seem sufficient to support usual programming patterns. For instance:

module M : sig type b [@@unique "M.b"] end = struct
  module M1 = struct type a = A [@@unique "M.b"] end
  type b = M1.a
end

Note that since exporting through aliases is allowed, it would indeed be possible to pass a unique type to a functor. However, since the functor would also need to give an expected name, this does not seem that useful. It would be more usable if we had a notion "unique type without name" as a supertype of "unique type", but I'm not sure there is much demand for that.

Conclusion and syntax

Modulo the need for explicit names, this seems to solve at once the problem of the uniqueness and injectivity of abstract types, both for external ones and for those implemented by datatypes. Those implemented by type abbreviations are not directly supported, but one can still wrap them. We could also have injectivity annotations on individual type variables, but the improvement would be minor.

The syntax is yet to define. @Drup suggested to use longidents rather than strings for names, maybe with a mechanism to retrieve them automatically from the context. A real syntax would be nice. Maybe something like

type 'a t = new
type 'a t = new M.t
type 'a t = new M.t = A | B
type 'a t = new M.t = 'a ab = A | B

but I'm not really convinced (the last case is particularly ugly, and is only needed for a technical reason)

Side remark: if you look at the code, I have added uniqueness annotations in the standard library. This is good for examples, but I'm not sure all of them are useful, in particular those in Set or Map. It would be good to have feedback from people who actually do intentional type analysis (@alainfrisch ?) to understand their needs w.r.t. to the compatibility relation.

An interesting remark, which I found in a discussion with @Ekdohibs, is that by restricting a bit the current proposal to allow only exporting named types with the same arity, it would be possible to make identically named types whose names are identical incompatible when their parameters are incompatible.
For instance

type 'a t [@@unique "M.t"]
type 'a u [@@unique "M.t"]

would allow to deduce that int t and bool u are incompatible.
The reasoning here is

• either t and u were originally the same type, and since it is injective, int t is incompatible with bool t
• or t and u were different types which just happen to share the same name, and they are incompatible.

It would still be possible to export a completely instantiated type with no parameters:

module M : sig type x [@@unique "M.t"] = struct type x = int t end

since x has no parameters to inject, but the following would have to be illegal:

module M : sig type 'a t [@@unique "M.t"] type 'a u [@@unique "M.t"] end = struct
   type ('a,'b) s [@@unique "M.t"]
   type 'a t = ('a,bool) s
   type 'a u = (int, 'a) s
end

since int t and bool u are actually equal.

A consequence is that, for Set.Make(X).t for instance, by including the key as a phantom constraint in it, it would be possible to create a composite identity, with name "Set.t" of x where x is the substituted name of X.t (if it has one). The interface looks like that:

module type S = sig
  type key
  type 'a t1 constraint 'a = key
  type t = key t1
  ...
end

Again, I'm not really suggesting to modify the standard library in this direction, this just demonstrates a useful expressive power.

This tension between uniqueness and injectivity suggests that, as @lpw25 said, the two concepts would be more precisely handled as separate (eventhough incompatibility requires both).
If we want only uniqueness, there is no need to track parameters, while if we want injectivity, we need them, and we might even want to track it for each variable.
On the other hand, from a language point of view, I'm not sure that this would be practical. Being able to extract all properties from a single qualifier makes designing interfaces simpler.

Thanks for the new summary. I have some thoughts on the details of the design and some thoughts about the general approach.

Details

From your description of the desired behaviour and subtyping relation, I think that it is best to think of this proposal as a change to the type's representation rather than its manifest. It is essentially equivalent to replacing:

and type_kind =
  | Type_abstract
  | Type_record of label_declaration list  * record_representation
  | Type_variant of constructor_declaration list
  | Type_open

with

and type_kind =
  | Type_abstract
  | Type_concrete of { name : string; repr : type_representation option }

and type_representation =
  | Type_record of label_declaration list  * record_representation
  | Type_variant of constructor_declaration list
  | Type_open

with the expected subtyping relation of Type_concrete :> Type_abstract and Some repr :> None. Ctype.is_datatype would now return true for any Type_concrete and Typedecl.check_coherence would enforce coherence for any Type_concrete.

That should be sufficient to get the behaviour you are after and it avoids changing anything around manifests. I think messing with manifests is more dubious proposition -- see for example the issues where private types cause equations to be lost.

I don't know what the best syntax for your proposal is, but I think that "unique" is quite a loaded term. I would prefer something like [@named "foo"]. I would also prefer not to have the [@unique] form and make people specify the name themselves.

I strongly oppose using longidents rather than strings: these labels have no structure to them and certainly no notion of binding, we should not pretend that they do.

Overall approach

All in all, I'm still not convinced by this proposal as compared to your original external-style proposal. Here you are adding a new component to OCaml's notion of type, whereas before you where just adding a new form of representation. The former seems quite invasive semantically for quite a small benefit.

In particular, I'm think your proposal creates a new question that must be answered for each new type the user creates: "What should its name be?". I don't see a simple systematic way for users to answer that question and that worries me.

In my experience, GADTs are either proper GADTs -- in which case the indices are ordinary types and their compatibility doesn't really matter -- or they are poor-mans indexed types -- in which case some fake types are created to encode some form of data and the external version would be sufficient to control their compatibility. I have not yet seen real examples that need the more invasive version of your proposal.

@lpw25 Thanks for looking at the proposal.

Concerning the representation, I really think this is a question of point of view.
However, the problem with vanishing type definitions (i.e. definition + equation case) suggests that I'm not going to touch to type_manifest anyway.
I'm not too enthusiastic about touching to type_kind either. While your encoding probably works, it would require changing lots of unrelated code. Anyway, we can consider that later. I think that at least we share the same understanding.

For the syntax, I have no strong opinion, but indeed, while playing with this branch, it became clear that unique is not a very good name (i.e., it doesn't really fit the explanation anymore).
named is fine with me. Actually it should be distinguishing name, but it's a bit long.
The important point here is that there can be at most one name.
People seem to have strong opinions about using an attribute for types or not. I don't.

More importantly, about the need of being able to name defined abstract types.
I share your analysis of two cases, ordinary types and type-level values, but I don't think that compatibility and injectivity do not matter for ordinary types, and conversely we can already handle fake types by using normal datatypes.
There are two typical cases using normal types: type witnesses and typed expressions

1. injectivity is required to obtain information about a type parameter in a witness

module M : sig type +'a t [@@unique "M.t"] end =
  struct type 'a t = Nil | Cons of 'a * 'a t [@@unique "M.t"] end
type _ ty = M : 'a ty -> 'a M.t ty;; (* error without [@@unique] *)

There is a workaround, but it is particularly clumsy:

module M : sig type +'a t0  and 'a t = M_t of 'a t0 end =
  struct type 'a t0 = Nil | Cons of 'a * 'a t0 and 'a t = M_t of 'a t0 end
type _ ty = M : 'a ty -> 'a M.t ty;;

2. For an expression, we may want to use type information to remove unneeded cases

module M : sig type +'a t [@@unique "M.t"] val create : 'a list -> 'a t end = struct
  type 'a t = Nil | Cons of 'a * 'a t [@@unique "M.t"]
  let rec create = function [] -> Nil | a::l -> Cons (a, create l)
end
type _ exp = M : 'a list -> 'a M.t exp | Int : int -> int exp
let eval_int : int exp -> int = function Int x -> x;;

So yes, I think this is useful, exactly in the same way as it is useful for external data.
Additionally, from a language design point of view, it is much nicer to be able to do the same thing for abstract data defined in OCaml and in C.

Last, and orthogonal, on whether to use quoted strings or paths.
I have no strong opinion, but one advantage of restricting to paths is to have a more homogeneous naming. Namely, abstract types exported from a library are expected to appear at some path in the environment. Encouraging programmers to use this path rather than an arbitrary string avoids involuntary collisions.

Implemented the nominal types RFC.

• [@@unique "s"] -> [@@nominal "s"]
• [@@nominal] alone implies just injectivity

Modulo the need for explicit names, this seems to solve at once the problem of the uniqueness and injectivity of abstract types, both for external ones and for those implemented by datatypes.

I'm not sure that the current proposal completely solves the injectivity question. One situation in which injectivity often crops up is where one type is defined as a specialization of another injective type. For example, the type constructor for the environment/reader monad is defined as a particular type of function type:

type 'a t = s -> 'a

Although t is injective in its parameter, it seems that under the current proposal it isn't a valid implementation of the monad interface:

module type monad = sig type +'a t [@@nominal] ... end

I think the recent paper "Higher-order Type-level Programming in Haskell" (Csongor Kiss et al, ICFP '19) might be relevant here. What's called "unique" / "nominal" here is called "generative" there, and they say a type constructor is "matchable" if both generative and injective. It's Haskell, so they're starting from the opposite position (in Haskell 98, all type constructors are matchable), but the problem looks similar.

@yallop Indeed, I do not attempt to support type abbreviations (when they are not simple re-exports). While it is technically possible to infer injectivity independently of nominality, I'm afraid this would have only a limited impact: you can always rewrap your abbreviation inside a nominal type definition.
And I do not expect many functors to require it. The idea is not to have all nominal types explicitly marked so, but just when the need is clear enough.

@stedolan Thanks for the pointer. This looks relevant enough. Generative could be a better name, but I was a bit afraid of the confusion with generative functors.

Generative could be a better name, but I was a bit afraid of the confusion with generative functors.

Agreed! I mentioned "generative" only to explain the relationship to that paper, I think we should not use the same term here.

Rebased on trunk (3.12) on 2020-08-07.