作为执行级别参数的ocaml的gadt

我想写一个函数 run 获取参数以参数化其执行级别。我希望这个函数在给定的级别之后返回其输出。我用gadt来输出 运行 取决于它的输入。

代码如下:

type _ level_output =                                                                                                                   
  | FirstO  : int -> int level_output                                                                                                  
  | SecondO : float -> float level_output                                                                                              
  | ThirdO  : string -> string level_output                                                                                            

type _ run_level_g =                                                                                                                    
  | First  : int run_level_g                                                                                                           
  | Second : float run_level_g                                                                                                         
  | Third  : string run_level_g 

type run_level = Any : 'a run_level_g -> run_level

let first _ =
  (*do stuff*)
  1

let second _ =
  (*do stuff*)
  2.5

let third _ =
  (*do stuff*)
  "third"

let run1 (type a) (level:a run_level_g) data : a level_output =
  let out = first data in
  match level with
  | First -> FirstO out
  | Second ->
    let out = second out in
    SecondO out
  | Third ->
    let out = second out in
    let out = third out in
    ThirdO out


let run2 (type a) (level:a run_level_g) data : a level_output =
  let out = first data in
  if Any level = Any First
  then FirstO out
  else
    let out = second out in
    if Any level = Any Second
    then SecondO out
    else
      let out = third out in
      ThirdO out


type (_,_) eq = Eq : ('a,'a) eq

let eq_level (type a b) (x:a run_level_g) (y:b run_level_g) : (a, b) eq option =
  match x, y with
  | First, First -> Some Eq
  | Second, Second -> Some Eq
  | Third, Third -> Some Eq
  | _ -> None

let cast_output (type a b) (Eq:(a, b) eq) (v:a level_output) : b level_output = v

let run3 (type a) (level:a run_level_g) data : a level_output =
  let out = first data in
  let eq = eq_level First level in
  match eq with
  | Some eq -> cast_output eq (FirstO out)
  | None ->
    let out = second out in
    let eq = eq_level Second level in
    match eq with
    | Some eq -> cast_output eq (SecondO out)
    | None ->
      let out = third out in
      let eq = eq_level Third level in
      match eq with
      | Some eq -> cast_output eq (ThirdO out)
      | None -> failwith "this can't happen"

有三种版本 运行 . 第一个很好地工作,但是有代码重复,我想删除它。我希望我的功能看起来更像 run2 但这一个没有编译,因为类型检查器无法从if条件推断类型。这个问题的答案是 run3 但现在我有了这个笨重的 failwith 这种情况显然不可能发生。

我想知道是否有一种方法可以让我两全其美,一个没有代码重复和没有故障的函数?