gadt_any.ml

type _ ty =
  | TBool : bool ty
  | TInt  :  int ty

type _ value =
  | Bool : bool -> bool value
  | Int  : int -> int value

type _ expr =
  | Value : 'a value -> 'a expr
  | If : bool expr * 'a expr * 'a expr -> 'a expr
  | Eq : 'a expr * 'a expr -> bool expr
  | Lt : int expr * int expr -> bool expr

type any = 
  | Any : _ expr -> any

let rec type_from_expr: type a. a expr -> a ty = function
    | Value(Bool _) -> TBool
    | Value(Int _)  -> TInt
    | Eq(l, r)      -> TBool
    | Lt(l, r)      -> TBool
    | If(c, tb, _) -> type_from_expr tb


let rec expr_from_any: type a. a ty -> any -> a expr = fun t a ->
  match t, a with
  | TBool, Any(Value(Bool b)) -> Value (Bool b)
  | TInt, Any(Value(Int n))   -> Value (Int n)
  | TBool, Any(Eq(l, r))      -> Eq(l, r)
  | TBool, Any(Lt(l, r))      -> Lt(l, r)
  | t, Any(If(c,l, r)) ->
    let l' = expr_from_any t (Any l) in
    let r' = expr_from_any t (Any r) in
    If (c, l', r')
  | _ -> failwith "Type mismatch"

(* everything above works, but that is not what I wanted to achieve *)

(* the function below, does not typecheck *)
let unany: type a. any -> a expr = fun x ->
  try
    expr_from_any TBool x     (* this expression has type 'a expr, but an expression was expected of type a expr *) 
  with Failure s
    -> expr_from_any TInt x   (* same as above *)