+fun multiApp (f, loc, args) =
+ foldl (fn (arg, e) => (EApp (e, arg), loc)) f args
+
+datatype unification_error =
+ UnifyPred of pred * pred
+ | UnifyTyp of typ * typ
+ | UnifyOccurs of string * typ
+
+exception Unify of unification_error
+
+datatype type_error =
+ WrongType of string * exp * typ * typ * unification_error option
+ | WrongForm of string * string * exp * typ * unification_error option
+ | UnboundVariable of string
+ | WrongPred of string * pred * pred
+