After playing around with this for a little while, it looks to me like

    type t = []

isn't defining t as a synonym for the empty polyvariant, but rather
defining t to be an ADT with one constructor, []. In particular, note that

    type t = []
    type s = []

    let f (x : s) : t = x (* does not typecheck *)

    type r = t = [] (* parses fine, showing [] is a constructor *)

    let f [] = () (* no exhaustivity warnings, inferred type is f : r ->
unit *)

It's odd that [] is a valid constructor name, but I suppose we want it so
for lists, and might as well let other people reuse it.

On 25 November 2016 at 16:39, Julien Blond <julien.blond@gmail.com> wrote:

> Hi,
>
> Let's try something :
>
> $ ocaml
>         OCaml version 4.03.0
>
> # let _ : [] list = [];;
> Characters 9-10:
>   let _ : [] list = [];;
>
> Error: Syntax error
> # type empty = [];;
> type empty = []
> # let _ : empty list = [];;
> - : empty list = []
> #
>
> Does anyone know if there is a reason to forbid the empty polymorphic
> variant set in type expressions or if it's a bug ?
>
> Regards,
>
> -- Julien Blond
>