diff --git a/lib/common/ident.ml b/lib/common/ident.ml
index 9c9628d..80f83e0 100644
--- a/lib/common/ident.ml
+++ b/lib/common/ident.ml
@@ -27,3 +27,5 @@ let create ~(hint : string) =
   (!index, hint)
 
 let rename (_, name) = create ~hint:name
+
+let to_string x = Printf.sprintf "%s/%d" (snd x) (fst x)
diff --git a/lib/common/ident.mli b/lib/common/ident.mli
index 446c346..fb295c0 100644
--- a/lib/common/ident.mli
+++ b/lib/common/ident.mli
@@ -7,3 +7,5 @@ val from : string -> t
 val create : hint:string -> t
 
 val rename : t -> t
+
+val to_string : t -> string
diff --git a/lib/syntax/parsetree.ml b/lib/syntax/parsetree.ml
index 074d109..fc8883f 100644
--- a/lib/syntax/parsetree.ml
+++ b/lib/syntax/parsetree.ml
@@ -61,6 +61,7 @@ and type_paras = string list [@@deriving sexp]
 and type_def =
   | TDAdt of string * type_paras * variant list
   | TDAlias of string * type_expr
+  | TDRecord of string * type_paras * (string * type_expr) list
 [@@deriving sexp]
 
 and mod_body = top_level list [@@deriving sexp]
diff --git a/lib/typing/check.ml b/lib/typing/check.ml
index ba069ab..4ee8159 100644
--- a/lib/typing/check.ml
+++ b/lib/typing/check.ml
@@ -1,6 +1,21 @@
 [@@@warning "-27"]
 
-type ty = Syntax.Parsetree.type_expr
+open Types
+module T = Tree
+module U = Unify
+open Typedtree
+
+let tv_index = ref 0
+
+let make_tv () =
+  tv_index := !tv_index + 1;
+  let name = Printf.sprintf "'_t_%d" !tv_index in
+  T.TVar (Printf.sprintf "'_%s__%d" name !tv_index)
+
+let make_tv_of hint =
+  tv_index := !tv_index + 1;
+  let name = Printf.sprintf "'_%s_%d" hint !tv_index in
+  T.TVar (Printf.sprintf "'_%s__%d" name !tv_index)
 
 let dealias (t : ty) env : ty = raise Not_found
 
@@ -8,3 +23,52 @@ let normalize t env = dealias t env
 
 let eq (t1 : ty) (t2 : ty) env =
   if t1 == t2 then true else normalize t1 env = normalize t2 env
+
+let inst (t : bind_ty) : ty =
+  let qvs, te = t in
+  let new_tvs = List.map make_tv_of qvs in
+  te |> U.make_subst_lst qvs new_tvs
+
+let generalize (t : ty) : bind_ty = failwith "todo"
+
+let rec type_check (e : T.expr) (env : Env.t) : expr * U.t =
+  match e with
+  | T.EConst c -> tc_const c
+  | T.EVar x -> tc_var x env
+  | T.ELet (x, e0, e1) -> tc_let x e0 e1
+  | T.ELetrec (binds, body) -> tc_letrec binds body
+  | T.ELam (para, body) -> tc_lambda para body
+  | T.EIf (c, e0, e1) -> tc_if_else c e0 e1
+  | T.ECase (e, bs) -> tc_cases e bs
+  | T.EApp (e0, e1) -> tc_app e0 e1
+  | T.EAnn (e, te) -> tc_ann e te
+  | T.ETuple es -> tc_tuple es
+  | T.EField (p, x) -> tc_field p x
+
+and tc_const c =
+  match c with
+  | T.CBool _ -> (EConst (c, bool_ty), U.identity)
+  | T.CInt _ -> (EConst (c, int_ty), U.identity)
+  | T.CString _ -> (EConst (c, string_ty), U.identity)
+
+and tc_var x env =
+  let t = Env.get_value_type x env |> inst in
+  (EVar (x, t), U.identity)
+
+and tc_let x e0 e1 = failwith ""
+
+and tc_letrec binds body = failwith ""
+
+and tc_lambda para body = failwith ""
+
+and tc_if_else c e1 e2 = failwith ""
+
+and tc_cases e bs = failwith ""
+
+and tc_app e0 e1 = failwith ""
+
+and tc_ann e te = failwith ""
+
+and tc_tuple es = failwith ""
+
+and tc_field p x = failwith ""
diff --git a/lib/typing/dune b/lib/typing/dune
index 6b3aab6..6be17b6 100644
--- a/lib/typing/dune
+++ b/lib/typing/dune
@@ -1,6 +1,6 @@
 (library
  (name typing)
- (libraries sexplib syntax)
+ (libraries sexplib syntax common)
  (preprocess
   (pps ppx_sexp_conv)))
 
diff --git a/lib/typing/env.ml b/lib/typing/env.ml
index 5221145..a5747c6 100644
--- a/lib/typing/env.ml
+++ b/lib/typing/env.ml
@@ -1,7 +1,7 @@
 open Types
 
 type t = {
-  values : (string * ty) list;
+  values : (string * bind_ty) list;
   types : ty_def list;
   modules : (string * mod_ty) list;
 }
@@ -20,6 +20,7 @@ let get_type_def tn env =
   List.find
     (function
       | Syntax.Parsetree.TDAdt (x, _, _)
-      | TDAlias (x, _) ->
+      | TDAlias (x, _)
+      | TDRecord (x, _, _) ->
           x = tn)
     env.types
diff --git a/lib/typing/typedtree.ml b/lib/typing/typedtree.ml
index e69de29..5e270ed 100644
--- a/lib/typing/typedtree.ml
+++ b/lib/typing/typedtree.ml
@@ -0,0 +1,40 @@
+open Types
+module T = Tree
+
+type constant = T.constant
+
+type pattern =
+  | PVal of constant
+  | PCons of string * pattern list
+  | PVar of string
+
+type path = T.path
+
+type expr =
+  | EConst of constant * ty
+  | EVar of string * ty
+  | ELet of pattern * expr * expr * ty
+  | ELetrec of (string * lambda_typed) list * expr * ty
+  | ELam of lambda_typed
+  | EIf of expr * expr * expr * ty
+  | ECase of expr * (pattern * expr) list * ty
+  | EApp of expr * expr * ty
+  | EAnn of expr * ty
+  | ETuple of expr list * ty
+  | EField of path * ty
+
+and lambda_typed = string * expr * ty
+
+let get_ty = function
+  | EConst (_, ty)
+  | EVar (_, ty)
+  | ELet (_, _, _, ty)
+  | ELetrec (_, _, ty)
+  | ELam (_, _, ty)
+  | EIf (_, _, _, ty)
+  | ECase (_, _, ty)
+  | EApp (_, _, ty)
+  | EAnn (_, ty)
+  | ETuple (_, ty)
+  | EField (_, ty) ->
+      ty
diff --git a/lib/typing/types.ml b/lib/typing/types.ml
index 7468aee..00585b5 100644
--- a/lib/typing/types.ml
+++ b/lib/typing/types.ml
@@ -1,5 +1,15 @@
-type ty = Syntax.Parsetree.type_expr
+module Tree = Syntax.Parsetree
 
-type mod_ty = Syntax.Parsetree.mod_type
+type ty = Tree.type_expr
 
-type ty_def = Syntax.Parsetree.type_def
+type mod_ty = Tree.mod_type
+
+type ty_def = Tree.type_def
+
+type bind_ty = string list * ty
+
+let int_ty = Tree.TCons ("int", [])
+
+let string_ty = Tree.TCons ("string", [])
+
+let bool_ty = Tree.TCons ("bool", [])
diff --git a/lib/typing/unify.ml b/lib/typing/unify.ml
new file mode 100644
index 0000000..5760866
--- /dev/null
+++ b/lib/typing/unify.ml
@@ -0,0 +1,24 @@
+open Types
+
+type t = ty -> ty
+
+let compose (u0 : t) (u1 : t) : t = fun t -> t |> u0 |> u1
+
+let identity x = x
+
+let ( <$> ) = compose
+
+let apply_lst : t -> ty list -> ty list = List.map
+
+let apply_env u (env : Env.t) : Env.t =
+  {
+    values = List.map (fun (x, te) -> (x, u te)) env.values;
+    (* types and modules have no space for inference *)
+    types = env.types;
+    modules = env.modules;
+  }
+
+let[@warning "-27"] unify (t0 : ty) (t1 : ty) : t = failwith "todo"
+
+let[@warning "-27"] make_subst x t : t = failwith "todo"
+let [@warning "-27"] make_subst_lst xs ts: t = failwith "todo"