type t =
    TInt
  | TFunc of t * t
type expr =
    Int of int
  | Var of string
  | Func of string * t * expr
  | App of expr * expr
type env = (string * t) list
let rec tc (a : env) (e : expr) : t = match e with
  Int _ -> TInt
| Var x -> List.assoc x a
| Func (x, xt, e') ->
    let t' = tc ((x, xt)::a) e' in
    TFunc (xt, t')
| App (e1, e2) ->
    let t1 = tc a e1 in
    let t2 = tc a e2 in
    match t1 with
      TFunc (t1', t1'') -> 
	begin
	  if t1' = t2 then t1''
	  else failwith "type error"
	end
    | _ -> failwith "type error"