Вот мое игрушечное выражение GADT:

type _ expr =
  | Num : int -> int expr
  | Add : int expr * int expr -> int expr
  | Sub : int expr * int expr -> int expr
  | Mul : int expr * int expr -> int expr
  | Div : int expr * int expr -> int expr
  | Lt  : int expr * int expr -> bool expr
  | Gt  : int expr * int expr -> bool expr
  | And : bool expr * bool expr -> bool expr
  | Or  : bool expr * bool expr -> bool expr

Функция оценки:

let rec eval : type a. a expr -> a = function
  | Num n -> n
  | Add (a, b) -> (eval a) + (eval b)
  | Sub (a, b) -> (eval a) - (eval b)
  | Mul (a, b) -> (eval a) * (eval b)
  | Div (a, b) -> (eval a) / (eval b)
  | Lt  (a, b) -> (eval a) < (eval b)
  | Gt  (a, b) -> (eval a) > (eval b)
  | And (a, b) -> (eval a) && (eval b)
  | Or  (a, b) -> (eval a) || (eval b)

Создание выражения тривиально, когда мы ограниченыint expr:

let create_expr op a b =
  match op with
  | '+' -> Add (a, b)
  | '-' -> Sub (a, b)
  | '*' -> Mul (a, b)
  | '/' -> Div (a, b)
  | _ -> assert false

Вопрос в том, как поддержать обаint expr а такжеbool expr вcreate_expr функция.

Моя попытка:

type expr' = Int_expr of int expr | Bool_expr of bool expr

let concrete : type a. a expr -> expr' = function
  | Num _ as expr -> Int_expr expr
  | Add _ as expr -> Int_expr expr
  | Sub _ as expr -> Int_expr expr
  | Mul _ as expr -> Int_expr expr
  | Div _ as expr -> Int_expr expr
  | Lt  _ as expr -> Bool_expr expr
  | Gt  _ as expr -> Bool_expr expr
  | And _ as expr -> Bool_expr expr
  | Or  _ as expr -> Bool_expr expr

let create_expr (type a) op (a:a expr) (b:a expr) : a expr =
  match op, concrete a, concrete b with
  | '+', Int_expr  a, Int_expr  b -> Add (a, b)
  | '-', Int_expr  a, Int_expr  b -> Sub (a, b)
  | '*', Int_expr  a, Int_expr  b -> Mul (a, b)
  | '/', Int_expr  a, Int_expr  b -> Div (a, b)
  | '<', Int_expr  a, Int_expr  b -> Lt  (a, b)
  | '>', Int_expr  a, Int_expr  b -> Gt  (a, b)
  | '&', Bool_expr a, Bool_expr b -> And (a, b)
  | '|', Bool_expr a, Bool_expr b -> Or  (a, b)
  | _ -> assert false

Он по-прежнему не может возвращать значение обобщенного типа.

Ошибка: это выражение имеет типint expr но ожидалось выражение типаa expr Типint не совместим с типомa

ОБНОВИТЬ

Благодаря @gsg я смог реализовать оценщик безопасных типов. Здесь есть два трюка:

экзистенциальная оболочкаAnyтип пометки (TyInt а такжеTyBool), что позволяет нам сопоставить образецAny тип

увидеть

type _ ty =
  | TyInt : int ty
  | TyBool : bool ty

type any_expr = Any : 'a ty * 'a expr -> any_expr

let create_expr op a b =
  match op, a, b with
  | '+', Any (TyInt,  a), Any (TyInt,  b) -> Any (TyInt,  Add (a, b))
  | '-', Any (TyInt,  a), Any (TyInt,  b) -> Any (TyInt,  Sub (a, b))
  | '*', Any (TyInt,  a), Any (TyInt,  b) -> Any (TyInt,  Mul (a, b))
  | '/', Any (TyInt,  a), Any (TyInt,  b) -> Any (TyInt,  Div (a, b))
  | '<', Any (TyInt,  a), Any (TyInt,  b) -> Any (TyBool, Lt  (a, b))
  | '>', Any (TyInt,  a), Any (TyInt,  b) -> Any (TyBool, Gt  (a, b))
  | '&', Any (TyBool, a), Any (TyBool, b) -> Any (TyBool, And (a, b))
  | '|', Any (TyBool, a), Any (TyBool, b) -> Any (TyBool, Or  (a, b))
  | _, _, _ -> assert false

let eval_any : any_expr -> [> `Int of int | `Bool of bool] = function
  | Any (TyInt, expr) -> `Int (eval expr)
  | Any (TyBool, expr) -> `Bool (eval expr)