Do I need polymorphic variants?

Learning
8

Using many features (objects, polymorphic variants, recursive types, GADT) and some known tricks I ended up with a way to encode deterministic finite state machine with heterogenously typed states (so that only allowed transitions are accepted by the type checker), but it’s a bit heavy (just an example for 3 states, 3 operations and 7 allowed transitions):

type state0 =
  < trans0 : state1;
    trans1 : state2;
    trans2 : [`forbidden];
    id     : [`_0] >
and state1 =
  < trans0 : state2;
    trans1 : state0;
    trans2 : state2;
    id     : [`_1] >
and state2 =
  < trans0 : state0;
    trans1 : [`forbidden];
    trans2 : state2;
    id     : [`_2] >

type data0 =
  {
    field0 : int;
    field1 : string
  }

type data1 = A | B of int

type data2 = int list option

type ('state, 'data) estate =
  | State0 : (state0, data0) estate
  | State1 : (state1, data1) estate
  | State2 : (state2, data2) estate

type 'state fsm_state = Ex : ('state, 'data) estate * 'data -> 'state fsm_state

let trans0 : type s0 s1 s2 id. < trans0 : s0; trans1 : s1; trans2 : s2; id : id > fsm_state -> s0 fsm_state =
  function
  | Ex (State0, { field0; field1 }) -> Ex (State1, if field0 < 0 && field1 = "" then A else B field0)
  | Ex (State1, A)                  -> Ex (State2, None)
  | Ex (State1 ,B i)                -> Ex (State2, Some [i])
  | Ex (State2, Some (x :: xs))     -> Ex (State0, { field0 = x; field1 = "" })
  | Ex (State2, (None | Some []))   -> Ex (State0, { field0 = 0; field1 = "" })

let trans1 :
  type s0 s10 s11 s12 s1i s2 id.
  < trans0 : s0; 
    trans1 : < trans0 : s10; trans1 : s11; trans2 : s12; id : s1i > as 'u;
    trans2 : s2;
    id : id > fsm_state -> 'u fsm_state =
  function
  | Ex (State0, { field0; field1 }) -> Ex (State2, if field0 < 0 && field1 = "" then Some [field0] else None)
  | Ex (State1, A)                  -> Ex (State0, { field0 = 0; field1 = "" })
  | Ex (State1 ,B i)                -> Ex (State0, { field0 = i; field1 = string_of_int i})

let rec trans2 :
  type s0 s1 s20 s21 s22 s2i id.
  < trans0 : s0;
    trans1 : s1;
    trans2 : < trans0 : s20; trans1 : s21; trans2 : s22; id : s2i > as 'u;
    id : id > fsm_state -> 'u fsm_state =
  function
  | Ex (State1, A)                  -> trans2 @@ Ex (State1, B 0)
  | Ex (State1, B i)                -> Ex (State2, None)
  | Ex (State2, None)               -> Ex (State2, Some [])
  | Ex (State2, Some [])            -> Ex (State2, None)
  | Ex (State2, Some (x :: xs))     -> trans2 @@ Ex (State2, Some xs)

let r0 = Ex (State0, { field0 = 1; field1 = ""}) |> trans1 |> trans0
let r1 = Ex (State0, { field0 = 1; field1 = ""}) |> trans1 |> trans0 |> trans0
let r2 = Ex (State0, { field0 = 1; field1 = ""}) |> trans1 |> trans0 |> trans0 |> trans2

(* let re = Ex (State0, { field0 = 1; field1 = ""}) |> trans1 |> trans1 *) (* Type error *)