Suppose I have a type consisting of multiple polymorphic variants (covariantly) such as the following:
[> `Ok of int | `Error of string]
Let's further suppose that I want to factor this definition into some kind of type constructor and a concrete type int. My first attempt was the following:
type 'a error = [> `Ok of 'a | `Error of string]
However, using a definition like this produces a really strange type error mentioning a type variable 'b that doesn't appear anywhere in the definition.
$ ocaml
OCaml version 4.07.0
# type 'a error = [> `Ok of 'a | `Error of string ];;
Error: A type variable is unbound in this type declaration.
In type [> `Error of string | `Ok of 'a ] as 'b the variable 'b is unbound
This 'b is an autogenerated name, adding an explicit 'b shifts the variable to 'c.
$ ocaml
OCaml version 4.07.0
# type ('a, 'b) error = [> `Ok of 'a | `Error of 'b ];;
Error: A type variable is unbound in this type declaration.
In type [> `Error of 'b | `Ok of 'a ] as 'c the variable 'c is unbound
Using the invariant construction [ `Thing1 of type1 | `Thing2 of type 2 ] appears to work fine in this context.
$ ocaml
OCaml version 4.07.0
# type 'a error = [ `Ok of 'a | `Error of string ] ;;
type 'a error = [ `Error of string | `Ok of 'a ]
#
However, explicitly marking the type parameter as covariant does not salvage the original example.
$ ocaml
OCaml version 4.07.0
# type +'a error = [> `Ok of 'a | `Error of string];;
Error: A type variable is unbound in this type declaration.
In type [> `Error of string | `Ok of 'a ] as 'b the variable 'b is unbound
And, just for good measure, adding a contravariance annotation also does not work.
$ ocaml
OCaml version 4.07.0
# type -'a error = [> `Ok of 'a | `Error of string];;
Error: A type variable is unbound in this type declaration.
In type [> `Error of string | `Ok of 'a ] as 'b the variable 'b is unbound
Attempting to guess the name that the compiler will use for the unbound type variable and adding it as a parameter on the left also does not work and produces a very bizarre error message.
$ ocaml
OCaml version 4.07.0
# type ('a, 'b) string = [> `Ok of 'a | `Error of string] ;;
Error: The type constructor string expects 2 argument(s),
but is here applied to 0 argument(s)
Is there a way of making a type constructor that can effectively "substitute different types" for int in [> `Ok of int | `Error of string]?
This isn't an issue of variance, or parametric polymorphism, but of row polymorphism. When you add > or < it also adds an implicit type variable, the row variable, that will hold the "full" type. You can see this type variable made explicit in the error:
[> `Error of string | `Ok of 'a ] as 'b
Note the as 'b part at the end.
In order to alias the type you have to make the type variable explicit, so you can reference it as a type parameter on the alias:
type ('a, 'r) error = [> `Ok of 'a | `Error of string ] as 'r
Note also, in case you have or when you will, run into objects, that this applies there as well. An object type with .. has an implicit type variable that you need to make explicit in order to alias it:
type 'r obj = < foo: int; .. > as 'r