OCaml的静态类型检查器上的错误

2010210088这是一个扩展名：Implementing type equation generator in OCaml

type exp = 
  | CONST of int
  | VAR of var
  | ADD of exp * exp
  | SUB of exp * exp
  | ISZERO of exp
  | IF of exp * exp * exp
  | LET of var * exp * exp
  | PROC of var * exp
  | CALL of exp * exp
and var = string

(* raise this exception when the program is determined to be ill-typed *)
exception TypeError

(* type *)
type typ = TyInt | TyBool | TyFun of typ * typ | TyVar of tyvar
and tyvar = string

(* type equations are represented by a list of "equalities" (ty1 = ty2)  *)
type typ_eqn = (typ * typ) list

(* generate a fresh type variable *)
let tyvar_num = ref 0
let fresh_tyvar () = (tyvar_num := !tyvar_num + 1; (TyVar ("t" ^ string_of_int !tyvar_num)))

(* type environment : var -> type *)
module TEnv = struct
  type t = var -> typ
  let empty = fun _ -> raise (Failure "Type Env is empty")
  let extend (x,t) tenv = fun y -> if x = y then t else (tenv y)
  let find tenv x = tenv x
end

(* substitution *)
module Subst = struct
  type t = (tyvar * typ) list
  let empty = []
  let find x subst = List.assoc x subst

  (* walk through the type, replacing each type variable by its binding in the substitution *)
  let rec apply : typ -> t -> typ
  =fun typ subst ->
    match typ with
    | TyInt -> TyInt
    | TyBool -> TyBool 
    | TyFun (t1,t2) -> TyFun (apply t1 subst, apply t2 subst)
    | TyVar x -> 
      try find x subst
      with _ -> typ

  (* add a binding (tv,ty) to the subsutition and propagate the information *)
  let extend tv ty subst = 
    (tv,ty) :: (List.map (fun (x,t) -> (x, apply t [(tv,ty)])) subst)
end

let rec gen_equations : TEnv.t -> exp -> typ -> typ_eqn 
=fun tenv e ty -> match e with
| CONST n -> [(ty, TyInt)]
| VAR x -> [(ty, TEnv.find tenv x)]
| ADD (e1,e2) ->
    let l1 = [(ty, TyInt)] in
    let l2 = gen_equations tenv e1 TyInt in
    let l3 = gen_equations tenv e2 TyInt in
    l1@l2@l3
| SUB (e1,e2) ->
    let l1 = [(ty, TyInt)] in
    let l2 = gen_equations tenv e1 TyInt in
    let l3 = gen_equations tenv e2 TyInt in
    l1@l2@l3
| ISZERO e ->
    let l1 = [(ty, TyBool)] in
    let l2 = gen_equations tenv e TyInt in
    l1@l2
| IF (e1,e2,e3) ->
    let l1 = gen_equations tenv e1 TyBool in
    let l2 = gen_equations tenv e2 ty in
    let l3 = gen_equations tenv e3 ty in
    l1@l2@l3
| LET (x,e1,e2) ->
    let t = fresh_tyvar () in
    let l1 = gen_equations tenv e1 t in
    let l2 = gen_equations (TEnv.extend (x,t) tenv) e2 ty in
    l1@l2
| PROC (x,e) ->
    let t1 = fresh_tyvar () in
    let t2 = fresh_tyvar () in
    let l1 = [(ty, TyFun (t1,t2))] in
    let l2 = gen_equations (TEnv.extend (x,t1) tenv) e t2 in
    l1@l2
| CALL (e1,e2) ->
    let t = fresh_tyvar () in
    let l1 = gen_equations tenv e1 (TyFun (t,ty)) in
    let l2 = gen_equations tenv e2 t in
    l1@l2
| _ -> raise TypeError

(* this is where the error comes up *)
let solve : typ_eqn -> Subst.t
=fun eqn -> unifyall eqn Subst.empty

let rec unify : typ -> typ -> Subst.t -> Subst.t
=fun t1 t2 s -> match (t1,t2) with
| (TyInt,TyInt) -> s
| (TyBool,TyBool) -> s
| (t,TyVar a) -> unify (TyVar a) t s
| (TyVar t1,t2) -> Subst.extend t1 t2 s
| (TyFun (t1,t2), TyFun (t1',t2')) ->
    let s' = unify t1 t1' s in
    let t1'' = Subst.apply t2 s' in
    let t2'' = Subst.apply t2' s' in
    unify t1'' t2'' s'

let rec unifyall : typ_eqn -> Subst.t -> Subst.t
=fun eqn s -> match eqn with
| [] -> s
| (t1,t2)::u ->
    let s' = unify (Subst.apply t1 s) (Subst.apply t2 s) s in
    unifyall u s'

let typeof : exp -> typ 
=fun exp -> 
  let new_tv = fresh_tyvar () in
  let eqns = gen_equations TEnv.empty exp new_tv in
  let subst = solve eqns in
  let ty = Subst.apply new_tv subst in
    ty

这是来自OCaml中的过程函数的静态类型检查器 . 除“解决”功能部分外，所有功能都运行良好 . 错误说，

错误：此表达式的类型为typ_eqn / 3404 =（typ / 3398 * typ / 3398）列表但是表达式类型为typ_eqn / 3179 =（typ / 3173 * typ / 3173）列表类型typ / 3398与type typ / 3173

/ mark旁边的那个大数字是什么？为什么不运作？