Polymorphic variant type gets restricted when try with is used

Learning
1

In the following code:

type t = [`A | `B]

let foo : (unit, [> t]) result = failwith "todo"

exception Ex of t

let bar : (unit, [> t]) result =
  try Ok (failwith "todo")
  with Ex t -> Error t

type of bar is inferred as (unit, t) result instead of (unit, [>t]) result. Is there a reason for this?

2

This is probably normal, because if your exception Ex is made to hold a type t, then Error also recieves a t.

If you write [> t] it means more than t.

For example here f can only recieve A or B, but you can see that g can recieve more than t: it can also recieve C:

type t = [`A | `B]

let f v = (v : t)

let g v = (v : [> t])

g `C ;;
3

Note that you can get an earlier error by adding an explicit polymorphic annotation

let bar : 'r. (unit, [> t] as 'r) result =
  try Ok (failwith "todo")
  with Ex t -> Error t

will fail with

5 |   with Ex t -> Error t
                         ^
Error: The value t has type t but an expression was expected of type [> t ]
      The second variant type is bound to the universal type variable 'a,
      it cannot be closed

(There is a small regression in the error message there)

If you want to reopen the polymorphic variant types, you can either add an explicit subtyping coercion

let bar :'r. (unit, [> t] as 'r) result =
  try Ok (failwith "todo")
  with Ex t -> Error (t:t:>[> t])

or use an as pattern over a polymorphic variant pattern:

let bar :'r. (unit, [> t] as 'r) result =
  try Ok (failwith "todo")
  with Ex (#t as e) -> Error e

here the #t pattern stands expand the type definition t into the pattern `A|`B and using an as pattern #t as e ensure that the type of e in the expression side is the most general type that fits the patter #t, which is [> t ] in this case.

1 Like