Polymorphic variants: upper/lower bounds and implicit type variables?

Learning
1

I’m trying to make sense of one aspect of upper and lower bounds for polymorphic variants.

On one hand, you can write:

let x:  [< `Red | `Green] = `Red;

On the other hand, you cannot give the type of x an alias:

type t = [< `Red | `Green];

Only the following works:

type 'a t = [< `Red | `Green] as 'a;
let x: 'a t = `Red;

Apparently, there are implicit type variables in play. Is there any material that fully explains how constraints are inferred and propagated; and how they interact with non-constraint types? Thanks!

2

The closest I can find to what the type parameter means in the context of a polymorphic variant type, is a passage in the manual ( https://caml.inria.fr/pub/docs/manual-ocaml-4.06/lablexamples.html#sec48 ):

Then, since x is returned as is, input and return types are identical. The notation as 'a denotes such type sharing.

This seems to indicate that the type parameter is used to capture the overall type of the open polymorphic variant, possibly to be used later.

To get to the point, the following type:

[< `Red | `Green]

Seems to be a syntax sugar for:

[< `Red | `Green] as 'a

You can confirm this by running:

let x: [< `Red | `Green] as 'a = `Red

So x actually is polymorphic with a type parameter 'a. In a value definition OCaml automatically qualifies the type with whatever type parameter you use, but in a type definition it needs to be explicit. Hence, you need to explicitly write:

type 'a t = [< `Red | `Green] as 'a
2 Likes
3

I figured it out: http://2ality.com/2018/01/polymorphic-variants-reasonml.html

Even the as is syntactic sugar:

# type t('a) = [> `Red] as 'a;
type t('a) = 'a constraint 'a = [> `Red ];
2 Likes