Hey there! I’d like to know if there is a way to properly write or type handle_a so that the type system acknowledges the “subtraction” of the `A case handled by the function, while still propagating everything else—both known variants (like `B) and unknown ones.
module PV = struct
type a = [ `A ]
type b = [ `B ]
let handle_a : type x.
(unit -> x) ->
[> a | b ] ->
(x, [> b ]) result
= fun handler -> function
| `A -> Ok (handler ())
| `B -> Error `B
| rest -> Error rest
end
The inferred type is:
x. (unit -> 'x) -> ([> `A | `B ] as 'a) -> ('x, 'a) result
So there is just one implicit variable for the input variant, which gets propagated to the output instead of being refined as I manually typed it.
If the row variable were directly manipulable, I imagine the function could be typed something like this:
module PV = struct
type a = [ `A ]
type b = [ `B ]
let handle_a : type x row.
(unit -> x) ->
[a | b | row] ->
(x, [b | row]) result
= fun handler -> function
| `A -> Ok (handler ())
| `B -> Error `B
| rest -> Error rest
end
