remaining issues:

• tests/typing-extension-constructor/test.ml fails
• Ctype.mcomp needs to be carefully checked (seems to be still somewhat wrong)

For the record / historical note: I believe that this comes from RFC #4, and in particular #9042 (comment) from @lpw25.

I'm happy to review this / discuss the design here. My unfinished attempt at this is here. Glad to see this being added!

I am planning to separately PR the commit 478a177.

I am planning to separately PR the commit 478a177.

#13820

Just to make sure I understand: in this PR, is it allowed to have a nominal abstract type in the interface with a concrete type definition in the implementation? eg

module M : sig
  type t = external "t"
end = struct
  type t = A
end

?

Just to make sure I understand: in this PR, is it allowed to have a nominal abstract type in the interface with a concrete type definition in the implementation? eg

module M : sig
  type t = external "t"
end = struct
  type t = A
end

?

Incidentally, this PR looks like it could be useful for runtime types (see Section 3 of https://www.math.nagoya-u.ac.jp/~garrigue/papers/ocaml2013.pdf).

Just to make sure I understand: in this PR, is it allowed to have a nominal abstract type in the interface with a concrete type definition in the implementation? eg

module M : sig
  type t = external "t"
end = struct
  type t = A
end

?

A short answer is no:

# module M : sig
    type t = external "t"
  end = struct
    type t = A
  end;;
Error: Signature mismatch:
       Modules do not match:
         sig type t = A end
       is not included in
         sig type t = external "t" end
       Type declarations do not match:
         type t = A
       is not included in
         type t = external "t"
       The first is a variant, but the second is nominal "t".

But modifying includecore.ml to coerce a nominal type to an arbitrary type (except for another nominal) makes it possible. I am however not convinced if this is a plausible semantics @garrigue @goldfirere

diff --git a/typing/includecore.ml b/typing/includecore.ml
index 2db7b9532f..2fd381c084 100644
--- a/typing/includecore.ml
+++ b/typing/includecore.ml
@@ -1005,7 +1005,9 @@ let type_declarations ?(equality = false) ~loc env ~mark name
           labels1 labels2
           rep1 rep2
     | (Type_open, Type_open) -> None
-    | (Type_nominal n1, Type_nominal n2) when n1 = n2 -> None
+    | (Type_nominal n1, Type_nominal n2) when n1 <> n2 ->
+        Some (Kind (of_kind decl1.type_kind, of_kind decl2.type_kind))
+    | (_, Type_nominal _) -> None
     | (_, _) -> Some (Kind (of_kind decl1.type_kind, of_kind decl2.type_kind))
   in
   if err <> None then err else

Coercion from datatype to nominal type was in the nominal RFC, but this is not in this version, as it raises questions as to whether abstract type in libraries should be converted to nominal types, and with which name.

Note that in that case the name should already be given in the datatype definition, otherwise it becomes possible to export the same datatype with two different names, which is unsound.

Thanks for the response @t6s and @garrigue. Indeed I raised the question because this coercion was mentioned in #9042 (comment).

We discussed the feature at the last type-system meeting. We generally agree that this is a good feature to have, in particular to be able to disable the existing behavior on current-module abstract types which has more downsides than upsides. The plan is to merge the PR as soon as it is ready, and that some documentation is written in the reference manual -- @Octachron and myself have been looking at how to document this.

Naming

The feature is called "nominal types" here, coming from the RFC, but I think that "external types" makes more sense. The story is that these types are intended to be populated from the FFI (and possibly from unsafe casts/primitives), and their syntax precisely uses external.

Do you agree with this naming change suggestion? Should we use Type_external then?

Documentation

Here is our current plan for documentation:

• In the GADT chapter, describe how to get strong equalities on non-current-module types using type t = private Foo. Mention the 'legacy' behavior on the current-module types and explain that it is going to change.

  (Maybe: also show examples with parametrized types used as type-level term construcftors, and point out that an injectivity annotation is required.)

• A new extension chapter on external types: abstract types used for FFI purposes (in particular base/predefined type declarations).

Documentation

Here is our current plan for documentation:

• In the GADT chapter, describe how to get strong equalities on non-current-module types using type t = private Foo. Mention the 'legacy' behavior on the current-module types and explain that it is going to change.
  (Maybe: also show examples with parametrized types used as type-level term construcftors, and point out that an injectivity annotation is required.)
• A new extension chapter on external types: abstract types used for FFI purposes (in particular base/predefined type declarations).

I thought that we agreed to remove the previous behavior at once. So it is not "going to change", but "has changed".
Also, it would be fine to mention using external as an alternative to private for new code.

@gasche I think the renaming reasonable and have done that.

I am realizing now that the change in this PR has farther-reaching implications than I assumed. This is now rejected:

type t = A
type u = A

let test (x : (t, u) Type.eq) =
  match x with _ -> .

or this

type t = { x : int }
type u = { x : int }

let test (x : (t, u) Type.eq) =
  match x with _ -> .

I thought that this would only start being rejected for abstract types,

type t
type u

but in fact datatypes are also affected.

The same reasoning applies that these examples are not robust to being put under a module abstraction, and in fact we did discuss the impact on empty types type t = | a few years ago ( #8900 ), but I wish it had been clearer in the discussion that the compatibility-breaking behavior change does not just affect (fully) abstract types.

Well, yes, since now the compatibility check is purely structural, any two types with the same structure cannot be distinguished. This has always been the case when one of the types was coming from another module.

I can see opam-repo tests were run in 2019 in #8900 (comment) to test the implications of this backward incompatible change. Have something more recent been run? 🤔

I can see opam-repo tests were run in 2019 in #8900 (comment) to test the implications of this backward incompatible change. Have something more recent been run? 🤔

I believe this is because the backward compatibility issue only shows up as a warning since partial-match isn't an error by default (see #12475) and doesn't show up at all with dune's default set of warnings in release mode. I encountered this when building in dev/CI mode, see #14224

I don't want to bikeshed syntax, but I am worried that this feature isn't the right direction for exposing the 'generative' / 'nominal' behaviour of OCaml's datatypes.

The current syntax:

type t = external "name"

is misleading: it looks like a type alias for external "name". The syntax is also awkward to combine with the original intention of unique types. Consider
an external type, with a manifest type, and a datatype declaration:

type t = Foo.bar = external "t" = Foo | Bar

In his comment, @lpw25 suggested a more coherent approach: introduce an abstract nominal datatype, exploiting that datatypes are generative already. The idea is to refactor type_kind into something like:

type type_kind = 
  | Abstract
  | Datatype of  { kind : datatype_kind option }
  | Alias of { kind : alias_kind }

type datatype_kind = 
  | Variant of ...

type alias_kind = 
  | Expansion of { privacy : private_flag; expansion : type_expr }
  | Manifest of { manifest : Path.t; kind : datatype_kind }

This captures the semantics that Datatype more cleanly:

• Datatype is generative, Alias is not generative, Abstract is not generative
• Datatype { kind = None } represents an abstract generative datatype
• Datatype { kind = Some ... } covers the usual cases for nominal variants/records.

Subtyping already permits Alias / Datatype :> Abstract. With this representation, we can additionally give Datatype { kind = Some _ :> kind = None }.

Unfortunately, I'm not too sure what the syntax for such a construction should be. If we had the benefit of hindsight, perhaps Datatype would be new type and Abstract / Alias would be type and we would have:

type t (** maps to [Abstract] *)
type t = int (** maps to [Alias { kind = Expansion { ... } }] *)
type t = Foo.bar = Foo | Bar (** maps to [Alias { kind = Manifest { path = Foo.bar; ... } }] *)
new type t (** maps to [Datatype { kind = None }] *)
new type t = Foo | Bar (** maps to [Datatype { kind = Variant ... }] *)

In the case of external types, we would simply have:

new type float
new type int
...

I infact just noticed that @lpw25's comment doesn't correctly capture the erasure of a manifest type via subtyping (which would permit Alias :> Datatype):

module Foo = struct 
  type t = Foo | Bar
end

module Bar : sig 
  type t = Foo | Bar 
end = struct 
  type t = Foo.t = Foo | Bar
end

Perhaps the fix is to add a new kind for types: Abstract, Alias, Datatype, New_abstract, New_datatype?

type type_kind = 
   ... 
   | New_abstract
   | New_datatype of { kind : datatype_kind }

with syntax:

new type t (** maps to [New_abstract] *)
new type t = Foo | Bar (** maps to [New_datatype] *)