Deconstructing polymorphic variant type

Is it possible to deconstruct a polymorphic variant type such that this does what you would intuit it should?

let foo = function
  | `OK a -> Ok a
  | otherwise -> Error otherwise

And the pseudo code for the type would be:

val foo : [> `OK of 'a | 'b ] -> ('a, 'b) result

The closest thing I’ve been able to do includes the OK variable on on the Error side of the result.

I tried something like:

type ('a, 'b) foo = [> `OK of 'a | 'b ] -> ('a, 'b) result

But this fails because 'b can be anything, so I would need a way to constrain it to just polymorphic variants

Do you have tried to input this snippet in a toplevel?

It gives me the following:

val foo : ([> `OK of 'b ] as 'a) -> ('b, 'a) result = <fun>

That includes the `OK constructor on the Error side as well, which is what I’m trying to get around.

This is indeed not possible (and you would need to constraint 'b to a polymorphic variant that does not contain `Ok rather than a constraint-free polymorphic variants).

1 Like

Thank you @octachron .

I don’t know much about type systems: is what I’m asking theoretically not possible or is it just a feature that Ocaml hasn’t implemented?

This is a deliberate limitation of the OCaml type system compared to the underlying theory. When objects and polymorphic variants were added to OCaml, the type system was deliberately designed to ensure that the complicated row type variables were never visible to the users.