Polymorphic variant being generalised

@jjb’s reply is excellent, but let’s give a couple extra details. Your example boils down to something like:

apply : (unit -> [> error]) -> [> error])

When you write [> error], you have to understand this as a universal quantification: an instance of [> error] is any type which contains at least error (for example [ error ] or [ error | `Foo | `Bar ]. As with polymorphic type variables in signature, the caller gets to choose the instance they want at function application time. The two separate occurrences of [> error] correspond to two distinct/independent quantifications.

So the caller could instantiate this to, for example:

apply : (unit -> [ error | `Foo ]) -> [ error | `Bar ]

and clearly this is incorrect (with the “obvious” implementation fun f -> f ()): if the function parameter returns `Foo, then the return type must allow `Foo. In other words, the two occurrences of [> error] must be instantiated with the same type. This corresponds to the following, less general (and more correct) signature:

val apply : (unit -> ([> error ] as 'a)) -> ([> error ] as 'a)

which can also be written

val apply : (unit -> ([> error ] as 'a)) -> 'a
4 Likes