diff --git a/.github/workflows/PRformat.yml b/.github/workflows/PRformat.yml
index 08fba515e..029a3e729 100644
--- a/.github/workflows/PRformat.yml
+++ b/.github/workflows/PRformat.yml
@@ -4,6 +4,7 @@ on:
   pull_request:
     branches:
       - 'master'
+      - 'test-fix' #debug
 
 env:
   OPAMROOT: /home/user/.opam
@@ -35,15 +36,16 @@ jobs:
       ############# Detecting and compiling fp2024
       # Smart link about setting environment variables
       # https://docs.github.com/en/actions/reference/workflow-commands-for-github-actions#setting-an-environment-variable
-      - name: Detect latest changes
-        run: |
-          opam exec -- ocaml .github/detect_latest_pr.ml -v "pull/${{ steps.branch-name.outputs.ref_branch }}" -repo ${{ github.event.repository.name }} >> $GITHUB_ENV
-          echo "${{ env.latest }}"
+# DEBUG TO UNCOMMENT BEFORE PR
+#      - name: Detect latest changes
+#        run: |
+#          opam exec -- ocaml .github/detect_latest_pr.ml -v "pull/${{ steps.branch-name.outputs.ref_branch }}" -repo ${{ github.event.repository.name }} >> $GITHUB_ENV
+#          echo "${{ env.latest }}"
 
       - name: Naive linting
         run: |
           cd ${{ env.latest }}
-          python ../.github/lint_filesystem.py ${{ env.latest }}
+          find . -type l -name 'manytests' -prune -o -type f -exec python ../.github/lint_filesystem.py {} \;
 
 #      - name: Checking ocamlformat
 #        id: check-ocamlformat
@@ -59,7 +61,8 @@ jobs:
       - name: Checking ocamlformat
         run: |
           cd ${{ env.latest }}
-          opam exec -- dune build @fmt --profile=release
+          find . -type l -name 'manytests' -prune -o -type f -exec opam exec -- dune build @fmt --profile=release {} \;
+          
 
 
       # TODO: onfail post a comment how to fix it
diff --git a/FSharpActivePatterns/bin/REPL.ml b/FSharpActivePatterns/bin/REPL.ml
index 9f9e5870d..38a310dbd 100644
--- a/FSharpActivePatterns/bin/REPL.ml
+++ b/FSharpActivePatterns/bin/REPL.ml
@@ -4,6 +4,10 @@
 
 open FSharpActivePatterns.AstPrinter
 open FSharpActivePatterns.Parser
+open FSharpActivePatterns.Inferencer
+open FSharpActivePatterns.TypedTree
+open FSharpActivePatterns.TypesPp
+open FSharpActivePatterns.Ast
 open FSharpActivePatterns.PrettyPrinter
 open Stdlib
 
@@ -11,9 +15,8 @@ type input =
   | Input of string
   | EOF
 
-type 'a run_result =
-  | Result of 'a
-  | Fail
+type run_result =
+  | Result of (construction, string) result
   | Empty
   | End
 
@@ -41,44 +44,93 @@ let input_upto_sep sep ic =
   fill_buffer buffer
 ;;
 
+let input_with_indents ic =
+  let take_line () = In_channel.input_line ic in
+  let rec fill_buffer b =
+    let start_pos = pos_in ic in
+    let line = take_line () in
+    match line with
+    | None -> Input (Buffer.contents b)
+    | Some line ->
+      let is_empty = String.length line = 0 in
+      let is_continue =
+        List.exists (fun pref -> String.starts_with ~prefix:pref line) [ " "; "\t"; "\n" ]
+        || is_empty
+        || String.starts_with ~prefix:"and" (String.trim line)
+      in
+      (match is_continue with
+       | true ->
+        let newline = " " ^ line in
+         Buffer.add_string b newline;
+         Buffer.add_string b "\n";
+         fill_buffer b
+       | false ->
+         seek_in ic start_pos;
+         Buffer.add_string b "\n";
+         Input (Buffer.contents b))
+  in
+  let buffer = Buffer.create 1024 in
+  let first_line = take_line () in
+  match first_line with
+  | None ->
+    EOF
+  | Some first_line ->
+    Buffer.add_string buffer first_line;
+    fill_buffer buffer
+;;
+
 let run_single ic =
-  match input_upto_sep ";;" ic with
+  let input =
+    match ic with
+    | None -> input_upto_sep ";;" stdin
+    | Some ic -> input_with_indents ic
+  in
+  match input with
   | EOF -> End
   | Input input ->
     let trimmed_input = String.trim input in
-    if trimmed_input = ""
-    then Empty
-    else (
-      match parse trimmed_input with
-      | Some ast -> Result ast
-      | None -> Fail)
+    if trimmed_input = "" then Empty else Result (parse trimmed_input)
 ;;
 
 let run_repl dump_parsetree input_file =
   let ic =
     match input_file with
-    | None -> stdin
-    | Some n -> open_in n
+    | None -> None
+    | Some n -> Some (open_in n)
   in
-  let rec run_repl_helper run =
+  let rec run_repl_helper run env state =
     let open Format in
     match run ic with
-    | Fail -> fprintf err_formatter "Error occured\n"
+    | Result (Error e) -> fprintf err_formatter "%s\n" e
     | Empty ->
       fprintf std_formatter "\n";
       print_flush ();
-      run_repl_helper run
+      run_repl_helper run env state
     | End -> ()
-    | Result ast ->
+    | Result (Ok ast) ->
       (match dump_parsetree with
        | true -> print_construction std_formatter ast
        | false ->
-         fprintf std_formatter "- : ";
-         pp_construction std_formatter ast);
-      print_flush ();
-      run_repl_helper run
+         let result = infer ast env state in
+         (match result with
+          | new_state, Error err ->
+            fprintf err_formatter "Type checking failed: %a\n" pp_error err;
+            print_flush ();
+            run_repl_helper run env new_state
+          | new_state, Ok (env, names_and_types) ->
+            List.iter
+              (fun (n, t) -> fprintf std_formatter "%s : %a" n pp_typ t)
+              names_and_types;
+            print_flush ();
+            run_repl_helper run env new_state))
+  in
+  let env =
+    TypeEnvironment.extend
+      TypeEnvironment.empty
+      "print_int"
+      (Scheme (VarSet.empty, Arrow (int_typ, unit_typ)))
   in
-  run_repl_helper run_single
+  run_repl_helper run_single env 0
 ;;
 
 type opts =
diff --git a/FSharpActivePatterns/bin/dune b/FSharpActivePatterns/bin/dune
index 64ac7d7d3..1e10d57b2 100644
--- a/FSharpActivePatterns/bin/dune
+++ b/FSharpActivePatterns/bin/dune
@@ -1,6 +1,6 @@
 (executable
  (public_name repl)
  (name REPL)
- (libraries FSharpActivePatterns stdlib)
+ (libraries FSharpActivePatterns stdlib str)
  (instrumentation
   (backend bisect_ppx)))
diff --git a/FSharpActivePatterns/bin/input.txt b/FSharpActivePatterns/bin/input.txt
index 2fd54233d..b1312d900 100644
--- a/FSharpActivePatterns/bin/input.txt
+++ b/FSharpActivePatterns/bin/input.txt
@@ -1,7 +1,41 @@
-let rec even n = 
-    if n = 0 then true 
-    else odd (n - 1)
-and odd n : int = 
-    if n = 0 then false 
-    else even (n - 1)
-;;
\ No newline at end of file
+let rec length xs =
+  match xs with
+  | [] -> 0
+  | h::tl -> 1 + length tl
+
+let length_tail =
+  let rec helper acc xs =
+  match xs with
+  | [] -> acc
+  | h::tl -> helper (acc + 1) tl
+  in
+  helper 0
+
+let rec map f xs =
+  match xs with
+  | [] -> []
+  | a::[] -> [f a]
+  | a::b::[] -> [f a; f b]
+  | a::b::c::[] -> [f a; f b; f c]
+  | a::b::c::d::tl -> f a :: f b :: f c :: f d :: map f tl
+
+let rec append xs ys = match xs with [] -> ys | x::xs -> x::(append xs ys)
+
+let concat =
+  let rec helper xs =
+    match xs with
+    | [] -> []
+    | h::tl -> append h (helper tl)
+  in helper
+
+let rec iter f xs = match xs with [] -> () | h::tl -> let () = f h in iter f tl
+
+let rec cartesian xs ys =
+  match xs with
+  | [] -> []
+  | h::tl -> append (map (fun a -> (h,a)) ys) (cartesian tl ys)
+
+let main =
+  let () = iter print_int [1;2;3] in
+  let () = print_int (length (cartesian [1;2] [1;2;3;4])) in
+  0
diff --git a/FSharpActivePatterns/lib/ast.ml b/FSharpActivePatterns/lib/ast.ml
index 4ecb60612..1fe2a60af 100644
--- a/FSharpActivePatterns/lib/ast.ml
+++ b/FSharpActivePatterns/lib/ast.ml
@@ -3,9 +3,9 @@
 (** SPDX-License-Identifier: LGPL-3.0-or-later *)
 
 open KeywordChecker
+open TypedTree
 
-type ident = Ident of string * string option (** identifier *)
-[@@deriving show { with_path = false }]
+type ident = Ident of string (** identifier *) [@@deriving show { with_path = false }]
 
 let gen_varname =
   let open QCheck.Gen in
@@ -26,8 +26,8 @@ let gen_varname =
   loop >>= fun name -> if is_keyword name then loop else return name
 ;;
 
-let gen_ident = QCheck.Gen.map (fun s -> Ident (s, None)) gen_varname
-let gen_ident_small_list = QCheck.Gen.(list_size (0 -- 3) gen_ident)
+let gen_ident = QCheck.Gen.map (fun s -> Ident s) gen_varname
+(* let gen_ident_small_list = QCheck.Gen.(list_size (0 -- 3) gen_ident) *)
 
 let gen_escape_sequence =
   let open QCheck.Gen in
@@ -98,15 +98,21 @@ type pattern =
   | PConst of literal (** | [4] -> *)
   | PVar of ident (** pattern identifier *)
   | POption of pattern option
-    (*| Variant of (ident list[@gen gen_ident_small_list]) (** | [Blue, Green, Yellow] -> *) *)
+  (*| Variant of (ident list[@gen gen_ident_small_list]) (** | [Blue, Green, Yellow] -> *) *)
+  | PConstraint of pattern * (typ[@gen gen_typ_sized (n / 4)])
 [@@deriving show { with_path = false }, qcheck]
 
+let gen_typed_pattern_sized n = QCheck.Gen.(pair (gen_pattern_sized n) (return None))
+
 type is_recursive =
   | Nonrec (** let factorial n = ... *)
   | Rec (** let rec factorial n = ... *)
 [@@deriving show { with_path = false }, qcheck]
 
-type expr =
+type case = (pattern[@gen gen_pattern_sized n]) * (expr[@gen gen_expr_sized n])
+[@@deriving show { with_path = false }, qcheck]
+
+and expr =
   | Const of literal (** [Int], [Bool], [String], [Unit], [Null] *)
   | Tuple of
       (expr[@gen gen_expr_sized (n / 4)])
@@ -129,17 +135,15 @@ type expr =
       * expr (** fun x y -> x + y *)
   | Apply of (expr[@gen gen_expr_sized (n / 4)]) * (expr[@gen gen_expr_sized (n / 4)])
   (** [sum 1 ] *)
+  | Function of
+      (case[@gen gen_case_sized (n / 4)])
+      * (case list[@gen QCheck.Gen.(list_size (0 -- 2) (gen_case_sized (n / 20)))])
+  (** [function | p1 -> e1 | p2 -> e2 | ... |]*)
   | Match of
       (expr[@gen gen_expr_sized (n / 4)])
-      * (pattern[@gen gen_pattern_sized (n / 4)])
-      * (expr[@gen gen_expr_sized (n / 4)])
-      * ((pattern * expr) list
-        [@gen
-          QCheck.Gen.(
-            list_size
-              (0 -- 2)
-              (pair (gen_pattern_sized (n / 20)) (gen_expr_sized (n / 20))))])
-  (** [match x with | x -> ... | y -> ...] *)
+      * (case[@gen gen_case_sized (n / 4)])
+      * (case list[@gen QCheck.Gen.(list_size (0 -- 2) (gen_case_sized (n / 20)))])
+  (** [match x with | p1 -> e1 | p2 -> e2 | ...] *)
   | LetIn of
       is_recursive
       * let_bind
@@ -147,11 +151,14 @@ type expr =
         [@gen QCheck.Gen.(list_size (0 -- 2) (gen_let_bind_sized (n / 20)))])
       * expr (** [let rec f x = if (x <= 0) then x else g x and g x = f (x-2) in f 3] *)
   | Option of expr option (** [int option] *)
+  | EConstraint of expr * (typ[@gen gen_typ_sized (n / 4)])
 [@@deriving show { with_path = false }, qcheck]
 
 and let_bind =
-  | Let_bind of ident * (ident list[@gen gen_ident_small_list]) * expr
-  (** [and sum n m = n+m] *)
+  | Let_bind of
+      (pattern[@gen gen_pattern_sized (n / 2)])
+      * (pattern list[@gen QCheck.Gen.(list_size (0 -- 3) (gen_pattern_sized (n / 4)))])
+      * expr (** [let sum n m = n + m] *)
 [@@deriving show { with_path = false }, qcheck]
 
 let gen_expr =
diff --git a/FSharpActivePatterns/lib/astPrinter.ml b/FSharpActivePatterns/lib/astPrinter.ml
index 9d32c2b37..a0db5cabe 100644
--- a/FSharpActivePatterns/lib/astPrinter.ml
+++ b/FSharpActivePatterns/lib/astPrinter.ml
@@ -49,7 +49,7 @@ let rec print_pattern indent fmt = function
     fprintf fmt "%s| PCons:\n" (String.make indent '-');
     print_pattern (indent + 2) fmt l;
     print_pattern (indent + 2) fmt r
-  | PVar (Ident (name, _)) -> fprintf fmt "%s| PVar(%s)\n" (String.make indent '-') name
+  | PVar (Ident name) -> fprintf fmt "%s| PVar(%s)\n" (String.make indent '-') name
   | POption p ->
     fprintf fmt "%s| POption: " (String.make indent '-');
     (match p with
@@ -57,6 +57,7 @@ let rec print_pattern indent fmt = function
      | Some p ->
        fprintf fmt "Some:\n";
        print_pattern (indent + 2) fmt p)
+  | PConstraint (p, _) -> print_pattern indent fmt p
 ;;
 
 let print_unary_op indent fmt = function
@@ -64,19 +65,15 @@ let print_unary_op indent fmt = function
   | Unary_not -> fprintf fmt "%s| Unary negative\n" (String.make indent '-')
 ;;
 
-let tag_of_ident = function
-  | Ident (s, _) -> s
-;;
-
 let rec print_let_bind indent fmt = function
   | Let_bind (name, args, body) ->
-    let name = tag_of_ident name in
-    let args = List.map tag_of_ident args in
     fprintf fmt "%s| Let_bind:\n" (String.make indent '-');
     fprintf fmt "%sNAME:\n" (String.make (indent + 4) ' ');
-    fprintf fmt "%s| %s\n" (String.make (indent + 4) '-') name;
+    fprintf fmt "%s| %a\n" (String.make (indent + 4) '-') pp_pattern name;
     fprintf fmt "%sARGS:\n" (String.make (indent + 4) ' ');
-    List.iter (fun arg -> fprintf fmt "%s| %s\n" (String.make (indent + 2) '-') arg) args;
+    List.iter
+      (fun arg -> fprintf fmt "%s| %a\n" (String.make (indent + 2) '-') pp_pattern arg)
+      args;
     fprintf fmt "%sBODY:\n" (String.make (indent + 4) ' ');
     print_expr (indent + 2) fmt body
 
@@ -93,7 +90,16 @@ and print_expr indent fmt expr =
   | Tuple (e1, e2, rest) ->
     fprintf fmt "%s| Tuple:\n" (String.make indent '-');
     List.iter (print_expr (indent + 2) fmt) (e1 :: e2 :: rest)
-  | Match (value, pat1, expr1, cases) ->
+  | Function ((pat1, expr1), cases) ->
+    fprintf fmt "%s| Function:\n" (String.make indent '-');
+    List.iter
+      (fun (pat, expr) ->
+        fprintf fmt "%s| Pattern:\n" (String.make (indent + 2) '-');
+        print_pattern (indent + 4) fmt pat;
+        fprintf fmt "%s| Case expr:\n" (String.make (indent + 2) '-');
+        print_expr (indent + 4) fmt expr)
+      ((pat1, expr1) :: cases)
+  | Match (value, (pat1, expr1), cases) ->
     fprintf fmt "%s| Match:\n" (String.make indent '-');
     fprintf fmt "%s| Value:\n" (String.make (indent + 2) '-');
     print_expr (indent + 4) fmt value;
@@ -101,10 +107,10 @@ and print_expr indent fmt expr =
       (fun (pat, expr) ->
         fprintf fmt "%s| Pattern:\n" (String.make (indent + 2) '-');
         print_pattern (indent + 4) fmt pat;
-        fprintf fmt "%s| Inner expr:\n" (String.make (indent + 2) '-');
+        fprintf fmt "%s| Case expr:\n" (String.make (indent + 2) '-');
         print_expr (indent + 4) fmt expr)
       ((pat1, expr1) :: cases)
-  | Variable (Ident (name, _)) ->
+  | Variable (Ident name) ->
     fprintf fmt "%s| Variable(%s)\n" (String.make indent '-') name
   | Unary_expr (op, expr) ->
     fprintf fmt "%s| Unary expr(\n" (String.make indent '-');
@@ -125,12 +131,11 @@ and print_expr indent fmt expr =
     (match else_body with
      | Some body -> print_expr (indent + 2) fmt body
      | None -> fprintf fmt "%s| No else body\n" (String.make (indent + 2) '-'))
-  | Lambda (pat1, pat_list, body) ->
-    (*let args = List.map tag_of_ident args in*)
+  | Lambda (arg1, args, body) ->
     fprintf fmt "%s| Lambda:\n" (String.make indent '-');
     fprintf fmt "%sARGS\n" (String.make (indent + 2) ' ');
-    print_pattern (indent + 4) fmt pat1;
-    List.iter (fun pat -> print_pattern (indent + 4) fmt pat) pat_list;
+    print_pattern (indent + 4) fmt arg1;
+    List.iter (fun pat -> print_pattern (indent + 4) fmt pat) (arg1 :: args);
     fprintf fmt "%sBODY\n" (String.make (indent + 2) ' ');
     print_expr (indent + 4) fmt body
   | Apply (func, arg) ->
@@ -157,6 +162,7 @@ and print_expr indent fmt expr =
      | Some e ->
        fprintf fmt "%s| Option: Some\n" (String.make indent '-');
        print_expr (indent + 2) fmt e)
+  | EConstraint (e, _) -> print_expr indent fmt e
 ;;
 
 let print_statement indent fmt = function
@@ -186,6 +192,6 @@ let print_construction fmt = function
 ;;
 
 let print_p_res fmt = function
-  | Some expr -> print_construction fmt expr
-  | None -> fprintf fmt "Error occured"
+  | Ok ast -> print_construction fmt ast
+  | Error e -> fprintf fmt "%s\n" e
 ;;
diff --git a/FSharpActivePatterns/lib/astPrinter.mli b/FSharpActivePatterns/lib/astPrinter.mli
index db17ee820..c2a769e9c 100644
--- a/FSharpActivePatterns/lib/astPrinter.mli
+++ b/FSharpActivePatterns/lib/astPrinter.mli
@@ -6,4 +6,4 @@ open Ast
 open Format
 
 val print_construction : formatter -> construction -> unit
-val print_p_res : formatter -> construction option -> unit
+val print_p_res : formatter -> (construction, tag) result -> unit
diff --git a/FSharpActivePatterns/lib/dune b/FSharpActivePatterns/lib/dune
index 4977e20e4..9801e5d06 100644
--- a/FSharpActivePatterns/lib/dune
+++ b/FSharpActivePatterns/lib/dune
@@ -1,7 +1,15 @@
 (library
  (name FSharpActivePatterns)
  (public_name FSharpActivePatterns)
- (modules Ast Parser AstPrinter PrettyPrinter KeywordChecker)
+ (modules
+  Ast
+  Parser
+  AstPrinter
+  PrettyPrinter
+  KeywordChecker
+  Inferencer
+  TypedTree
+  TypesPp)
  (libraries angstrom base)
  (preprocess
   (pps ppx_deriving_qcheck ppx_deriving.show))
diff --git a/FSharpActivePatterns/lib/inferencer.ml b/FSharpActivePatterns/lib/inferencer.ml
new file mode 100644
index 000000000..9bbb3925b
--- /dev/null
+++ b/FSharpActivePatterns/lib/inferencer.ml
@@ -0,0 +1,755 @@
+(** Copyright 2024-2025, Ksenia Kotelnikova <xeniia.ka@gmail.com>, Gleb Nasretdinov <gleb.nasretdinov@proton.me> *)
+
+(** SPDX-License-Identifier: LGPL-3.0-or-later *)
+
+open Ast
+open TypedTree
+open TypesPp
+open Format
+open Base
+
+type error =
+  [ `Occurs_check
+  | `Undef_var of string
+  | `Unification_failed of typ * typ
+  | `Not_allowed_right_hand_side_let_rec
+  | `Not_allowed_left_hand_side_let_rec
+  | `Args_after_not_variable_let
+  ]
+
+let pp_error fmt : error -> _ = function
+  | `Occurs_check -> fprintf fmt "Occurs check failed"
+  | `Undef_var s -> fprintf fmt "Undefined variable '%s'" s
+  | `Unification_failed (fst, snd) ->
+    fprintf fmt "unification failed on %a and %a" pp_typ fst pp_typ snd
+  | `Not_allowed_right_hand_side_let_rec ->
+    fprintf fmt "This kind of expression is not allowed as right-hand side of `let rec'"
+  | `Not_allowed_left_hand_side_let_rec ->
+    fprintf fmt "Only variables are allowed as left-hand side of `let rec'"
+  | `Args_after_not_variable_let ->
+    fprintf fmt "Arguments in let allowed only after variable"
+;;
+
+(* for treating result of type inference *)
+module R : sig
+  (* signature, smth like interface before realization *)
+  type 'a t
+
+  (* val bind : 'a t -> f:('a -> 'b t) -> 'b t *)
+  val return : 'a -> 'a t
+  val fail : error -> 'a t
+
+  include Base.Monad.Infix with type 'a t := 'a t
+
+  module Syntax : sig
+    val ( let* ) : 'a t -> ('a -> 'b t) -> 'b t
+  end
+
+  module RList : sig
+    val fold_left : 'a list -> init:'b t -> f:('b -> 'a -> 'b t) -> 'b t
+  end
+
+  val fresh : int t
+  val run : 'a t -> int -> int * ('a, error) Result.t
+
+  module RMap : sig
+    val fold : ('a, 'b, 'c) Map.t -> init:'d t -> f:('a -> 'b -> 'd -> 'd t) -> 'd t
+  end
+end = struct
+  (* takes current state, runs smth, outputs new state and success / error *)
+  type 'a t = int -> int * ('a, error) Result.t
+
+  (* bind -- if applying new state to first arg is correct, then apply f to
+     new argument and new state, else output error and state that caused it *)
+  let ( >>= ) : 'a 'b. 'a t -> ('a -> 'b t) -> 'b t =
+    fun m f st ->
+    let last, r = m st in
+    match r with
+    | Result.Error x -> last, Error x
+    | Ok a -> f a last
+  ;;
+
+  (* is called to cover result in fail or ok constructions *)
+  let fail e st = st, Base.Result.fail e
+  let return x last = last, Base.Result.return x
+  let bind x ~f = x >>= f
+
+  (* is called from x, function and state. if applying state to x is correct,
+     then output applying f to x in constructor Ok, otherwise output error and
+     state that caused it *)
+  let ( >>| ) : 'a 'b. 'a t -> ('a -> 'b) -> 'b t =
+    fun x f st ->
+    match x st with
+    | st, Ok x -> st, Ok (f x)
+    | st, Result.Error e -> st, Result.Error e
+  ;;
+
+  module Syntax = struct
+    let ( let* ) x f = bind x ~f
+  end
+
+  (* for applying f to all elements x of list xs with check that everything is
+     correct. If it is, outputs accumulator of all applyings *)
+  module RList = struct
+    let fold_left xs ~init ~f =
+      Base.List.fold_left xs ~init ~f:(fun acc x ->
+        let open Syntax in
+        let* acc = acc in
+        f acc x)
+    ;;
+  end
+
+  (* analogically to list. let* acc = acc is to extract value from type t *)
+  module RMap = struct
+    let fold map ~init ~f =
+      Map.fold map ~init ~f:(fun ~key ~data acc ->
+        let open Syntax in
+        let* acc = acc in
+        f key data acc)
+    ;;
+  end
+
+  (* takes current state, returns state + 1 *)
+  let fresh : int t = fun last -> last + 1, Result.Ok last
+  let run m = m
+end
+
+type fresh = int
+
+(* module with all type methods *)
+module Type : sig
+  type t = typ
+
+  val occurs_in : fresh -> t -> bool
+  val free_vars : t -> binder_set
+end = struct
+  type t = typ
+
+  (* check that v is not inside of second type.
+     Runs during substitution to ensure that there are no cycles*)
+  let rec occurs_in v = function
+    | Primitive _ -> false
+    | Type_var b -> b = v
+    | Arrow (fst, snd) -> occurs_in v fst || occurs_in v snd
+    | Type_list typ -> occurs_in v typ
+    | Type_tuple (fst, snd, rest) ->
+      occurs_in v fst || occurs_in v snd || List.exists rest ~f:(occurs_in v)
+    | TOption t -> occurs_in v t
+  ;;
+
+  (* collects all type variables *)
+  let free_vars =
+    let rec helper acc = function
+      | Primitive _ -> acc
+      | Type_var b -> VarSet.add b acc
+      | Arrow (fst, snd) -> helper (helper acc fst) snd
+      | Type_list typ -> helper acc typ
+      | Type_tuple (fst, snd, rest) -> List.fold (fst :: snd :: rest) ~init:acc ~f:helper
+      | TOption t -> helper acc t
+    in
+    helper VarSet.empty
+  ;;
+end
+
+(* module of substitution *)
+
+module Substitution : sig
+  type t
+
+  val empty : t
+
+  (* val mapping : fresh -> typ -> (fresh * typ) R.t *)
+  val singleton : fresh -> typ -> t R.t
+
+  (* val find : t -> fresh -> typ option *)
+  val remove : t -> fresh -> t
+  val apply : t -> typ -> typ
+  val unify : typ -> typ -> t R.t
+  val compose : t -> t -> t R.t
+  val compose_all : t list -> t R.t
+  (* val pp : formatter -> t -> unit *)
+end = struct
+  open R
+  open R.Syntax
+
+  (* t in this module is map of key fresh to value typ. last arg specifies
+     keys as int values (see fresh def) *)
+  type t = (fresh, typ, Int.comparator_witness) Map.t
+
+  (* empty map *)
+  let empty = Map.empty (module Int)
+
+  (* let pp fmt s =
+     Map.iter_keys s ~f:(fun k ->
+     let v = Map.find_exn s k in
+     fprintf fmt "%d: %a" k pp_typ v)
+     ;; *)
+
+  (* perform mapping of fresh var to typ with occurs check, if correct,
+     output new pair *)
+  let mapping k v = if Type.occurs_in k v then fail `Occurs_check else return (k, v)
+
+  (* perform mapping, if correct, create map w 1 element as described in type t *)
+  let singleton k v =
+    let* k, v = mapping k v in
+    return (Map.singleton (module Int) k v)
+  ;;
+
+  (* aliases for Map actions *)
+  let find = Map.find
+  let remove = Map.remove
+
+  (* search for input in given map, if there is no match, output
+     input type, else output found typ value associated w this key.
+     Basically narrow given type to conditions given in substitution *)
+  let apply map =
+    let rec helper = function
+      | Type_var b as typ ->
+        (match find map b with
+         | None -> typ
+         | Some x -> x)
+      | Arrow (fst, snd) -> Arrow (helper fst, helper snd)
+      | Type_list t -> Type_list (helper t)
+      | Type_tuple (fst, snd, rest) ->
+        Type_tuple (helper fst, helper snd, List.map rest ~f:helper)
+      | Primitive t -> Primitive t
+      | TOption t -> TOption (helper t)
+    in
+    helper
+  ;;
+
+  (* check that two types are compatible. in third case put new pair of type_var
+     and type into context (map) *)
+  let rec unify fst snd =
+    match fst, snd with
+    | Primitive fst, Primitive snd when String.equal fst snd -> return empty
+    | Type_var f, Type_var s when Int.equal f s -> return empty
+    | Type_var b, t | t, Type_var b -> singleton b t
+    | Arrow (f1, s1), Arrow (f2, s2) ->
+      let* subst1 = unify f1 f2 in
+      let* subst2 = unify s1 s2 in
+      compose subst1 subst2
+    | Type_list t1, Type_list t2 -> unify t1 t2
+    | TOption t1, TOption t2 -> unify t1 t2
+    | Type_tuple (t1_1, t1_2, t1_rest), Type_tuple (t2_1, t2_2, t2_rest)
+      when List.length t1_rest = List.length t2_rest ->
+      let type_pairs = List.zip_exn (t1_1 :: t1_2 :: t1_rest) (t2_1 :: t2_2 :: t2_rest) in
+      let* substitutions =
+        List.fold type_pairs ~init:(return []) ~f:(fun acc (t1, t2) ->
+          let* acc = acc in
+          let* subst = unify t1 t2 in
+          return (subst :: acc))
+      in
+      let substitution_result = compose_all substitutions in
+      substitution_result
+    | _ -> fail (`Unification_failed (fst, snd))
+
+  (* if value associated w this key exists in map, try to unify them, otherwise
+     get old substitution, form new singleton, update map so in contains new info *)
+  and extend key value map =
+    match find map key with
+    | Some value2 ->
+      let* map2 = unify value value2 in
+      compose map map2
+    | None ->
+      let value = apply map value in
+      let* map2 = singleton key value in
+      RMap.fold map ~init:(return map2) ~f:(fun key value acc ->
+        let value = apply map2 value in
+        let* key, value = mapping key value in
+        return (Map.update acc key ~f:(fun _ -> value)))
+
+  (* compose two maps together *)
+  and compose map1 map2 = RMap.fold map2 ~init:(return map1) ~f:extend
+
+  (* compose list of maps together *)
+  and compose_all maps = RList.fold_left maps ~init:(return empty) ~f:compose
+end
+
+(* module for scheme treatment *)
+module Scheme : sig
+  type t = scheme
+
+  (* val occurs_in : fresh -> t -> bool *)
+  val apply : Substitution.t -> t -> t
+  val free_vars : t -> binder_set
+  (* val pp : formatter -> t -> unit *)
+end = struct
+  type t = scheme
+
+  (* occurs check for both type vars set and typ in sheme *)
+  (* let occurs_in value = function
+     | S (vars, t) -> (not (VarSet.mem value vars)) && Type.occurs_in value t
+     ;; *)
+
+  (* let pp fmt = function
+     | Scheme (binder_s, t) -> fprintf fmt "%a %a" VarSet.pp binder_s pp_typ t
+     ;; *)
+
+  (* take all vars that are not bound in typ *)
+  let free_vars = function
+    | Scheme (vars, t) -> VarSet.diff (Type.free_vars t) vars
+  ;;
+
+  (* take substitution and scheme, remove its free vars from substitution,
+     form new scheme according to substitution (apply it to typ) *)
+  let apply subst (Scheme (vars, t)) =
+    let subst2 = VarSet.fold (fun key s -> Substitution.remove s key) vars subst in
+    Scheme (vars, Substitution.apply subst2 t)
+  ;;
+
+  (* let pp = pp_scheme *)
+end
+
+module TypeEnvironment : sig
+  type t
+
+  val free_vars : t -> VarSet.t
+  val extend : t -> string -> scheme -> t
+  val extend_many : t -> (string * scheme) list -> t
+  val apply : Substitution.t -> t -> t
+  val empty : t
+  val find : t -> string -> scheme option
+  val find_exn : t -> string -> scheme
+  val find_typ_exn : t -> string -> typ
+  val find_typ : t -> string -> typ option
+  val remove_many : t -> string list -> t
+  (* val pp : formatter -> t -> unit *)
+end = struct
+  open Base
+
+  (* environment (context?) -- pairs of names and their types list *)
+  type t = (string, scheme, String.comparator_witness) Map.t
+
+  (* if pair (key, some old value) exists in map env, then replace old value
+     with new, else add pair (key, value) into map *)
+  let extend env key value = Map.update env key ~f:(fun _ -> value)
+
+  let extend_many env list =
+    List.fold list ~init:env ~f:(fun env (k, v) -> extend env k v)
+  ;;
+
+  let remove = Map.remove
+  let remove_many t keys = List.fold ~init:t keys ~f:(fun acc k -> remove acc k)
+  let empty = Map.empty (module String)
+
+  (* apply given substitution to all elements of environment *)
+  let apply subst env = Map.map env ~f:(Scheme.apply subst)
+  let find = Map.find
+  let find_exn = Map.find_exn
+
+  let find_typ env key =
+    match find env key with
+    | Some (Scheme (_, typ)) -> Some typ
+    | None -> None
+  ;;
+
+  let find_typ_exn env key =
+    match find_exn env key with
+    | Scheme (_, typ) -> typ
+  ;;
+
+  (* let pp fmt t =
+     Map.iter_keys t ~f:(fun k ->
+     let (Scheme (binder_s, typ)) = find_exn t k in
+     fprintf fmt "%s : %a %a" k VarSet.pp binder_s pp_typ typ)
+     ;; *)
+
+  (* collect all free vars from environment *)
+  let free_vars : t -> VarSet.t =
+    Map.fold ~init:VarSet.empty ~f:(fun ~key:_ ~data:s acc ->
+      VarSet.union acc (Scheme.free_vars s))
+  ;;
+end
+
+open R
+open R.Syntax
+
+let unify = Substitution.unify
+let make_fresh_var = fresh >>| fun n -> Type_var n
+
+(* replace all type vars with fresh ones *)
+let instantiate : scheme -> typ R.t =
+  fun (Scheme (vars, t)) ->
+  VarSet.fold
+    (fun name typ ->
+      let* typ = typ in
+      let* fr_var = make_fresh_var in
+      let* subst = Substitution.singleton name fr_var in
+      return (Substitution.apply subst typ))
+    vars
+    (return t)
+;;
+
+(* take free vars of type t and environment, put difference between them
+   in S constructor so all vars are context independent *)
+let generalize env typ =
+  let free = VarSet.diff (Type.free_vars typ) (TypeEnvironment.free_vars env) in
+  Scheme (free, typ)
+;;
+
+let infer_lt = function
+  | Int_lt _ -> return int_typ
+  | Bool_lt _ -> return bool_typ
+  | String_lt _ -> return string_typ
+  | Unit_lt -> return unit_typ
+;;
+
+let rec infer_pattern env ~shadow = function
+  | Wild ->
+    let* fresh_var = make_fresh_var in
+    return (env, fresh_var)
+  | PConst lt ->
+    let* t = infer_lt lt in
+    return (env, t)
+  | PVar (Ident name) ->
+    let* fresh = make_fresh_var in
+    let scheme = Scheme (VarSet.empty, fresh) in
+    let env, typ =
+      match shadow with
+      | true -> TypeEnvironment.extend env name scheme, fresh
+      | false ->
+        let typ = TypeEnvironment.find_typ env name in
+        env, Option.value typ ~default:fresh
+    in
+    return (env, typ)
+  | POption None ->
+    let* fresh_var = make_fresh_var in
+    return (env, TOption fresh_var)
+  | POption (Some p) ->
+    let* env, typ = infer_pattern env ~shadow p in
+    return (env, TOption typ)
+  | PList [] ->
+    let* fresh_var = make_fresh_var in
+    return (env, Type_list fresh_var)
+  | PList (hd :: tl) ->
+    let* env, typ1 = infer_pattern env ~shadow hd in
+    let* env, typ2 = infer_pattern env ~shadow (PList tl) in
+    let* subst = Substitution.unify typ2 (Type_list typ1) in
+    let env = TypeEnvironment.apply subst env in
+    return (env, Substitution.apply subst typ2)
+  | PCons (hd, tl) ->
+    let* env, typ1 = infer_pattern env ~shadow hd in
+    let* env, typ2 = infer_pattern env ~shadow tl in
+    let* subst = Substitution.unify typ2 (Type_list typ1) in
+    let env = TypeEnvironment.apply subst env in
+    return (env, Substitution.apply subst typ2)
+  | PTuple (fst, snd, rest) ->
+    let* env, typ1 = infer_pattern env ~shadow fst in
+    let* env, typ2 = infer_pattern env ~shadow snd in
+    let* env, typs_rest =
+      List.fold_right
+        rest
+        ~f:(fun p acc ->
+          let* env, types = acc in
+          let* env, typ = infer_pattern env ~shadow p in
+          return (env, typ :: types))
+        ~init:(return (env, []))
+    in
+    return (env, Type_tuple (typ1, typ2, typs_rest))
+  | PConstraint (p, t) ->
+    let* env, inferred_typ = infer_pattern env ~shadow p in
+    let* subst = unify t inferred_typ in
+    return (TypeEnvironment.apply subst env, Substitution.apply subst t)
+;;
+
+let infer_patterns env ~shadow patterns =
+  List.fold_right
+    patterns
+    ~init:(return (env, []))
+    ~f:(fun pat acc ->
+      let* old_env, typs = acc in
+      let* new_env, typ = infer_pattern old_env ~shadow pat in
+      return (new_env, typ :: typs))
+;;
+
+let extract_names_from_pattern pat =
+  let rec helper = function
+    | PVar (Ident name) -> [ name ]
+    | PList l -> List.concat (List.map l ~f:helper)
+    | PCons (hd, tl) -> List.concat [ helper hd; helper tl ]
+    | PTuple (fst, snd, rest) ->
+      List.concat [ helper fst; helper snd; List.concat (List.map rest ~f:helper) ]
+    | POption (Some p) -> helper p
+    | PConstraint (p, _) -> helper p
+    | POption None -> []
+    | Wild -> []
+    | PConst _ -> []
+  in
+  helper pat
+;;
+
+let extract_names_from_patterns pats =
+  List.fold pats ~init:[] ~f:(fun acc p ->
+    List.concat [ acc; extract_names_from_pattern p ])
+;;
+
+let extract_bind_names_from_let_binds let_binds =
+  List.concat
+    (List.map let_binds ~f:(function Let_bind (pat, _, _) ->
+       extract_names_from_pattern pat))
+;;
+
+let extract_bind_patterns_from_let_binds let_binds =
+  List.map let_binds ~f:(function Let_bind (pat, _, _) -> pat)
+;;
+
+let extend_env_with_bind_names env let_binds =
+  (* to prevent binds like let rec x = x + 1*)
+  let let_binds =
+    List.filter let_binds ~f:(function Let_bind (_, args, _) -> List.length args <> 0)
+  in
+  let bind_names = extract_bind_patterns_from_let_binds let_binds in
+  let* env, _ = infer_patterns env ~shadow:true bind_names in
+  return env
+;;
+
+let check_let_bind_correctness is_rec let_bind =
+  match let_bind, is_rec with
+  | Let_bind (PVar _, _, _), _ -> return let_bind
+  | Let_bind _, Rec -> fail `Not_allowed_left_hand_side_let_rec
+  | Let_bind (_, args, _), _ when List.length args <> 0 ->
+    fail `Args_after_not_variable_let
+  | _ -> return let_bind
+;;
+
+let rec infer_expr env = function
+  | Const lt ->
+    let* t = infer_lt lt in
+    return (Substitution.empty, t)
+  | Variable (Ident varname) ->
+    (match TypeEnvironment.find env varname with
+     | Some s ->
+       let* t = instantiate s in
+       return (Substitution.empty, t)
+     | None -> fail (`Undef_var varname))
+  | Unary_expr (op, e) ->
+    let* op_typ =
+      match op with
+      | Unary_minus -> return int_typ
+      | Unary_not -> return bool_typ
+    in
+    let* e_subst, e_typ = infer_expr env e in
+    let* subst = unify op_typ (Substitution.apply e_subst e_typ) in
+    let* subst_result = Substitution.compose_all [ e_subst; subst ] in
+    return (subst_result, Substitution.apply subst e_typ)
+  | Bin_expr (op, e1, e2) ->
+    let* subst1, typ1 = infer_expr env e1 in
+    let* subst2, typ2 = infer_expr (TypeEnvironment.apply subst1 env) e2 in
+    let* e1typ, e2typ, etyp =
+      match op with
+      | Logical_and | Logical_or -> return (bool_typ, bool_typ, bool_typ)
+      | Binary_add
+      | Binary_subtract
+      | Binary_multiply
+      | Binary_divide
+      | Binary_and_bitwise
+      | Binary_or_bitwise
+      | Binary_xor_bitwise -> return (int_typ, int_typ, int_typ)
+      | Binary_greater | Binary_greater_or_equal | Binary_less | Binary_less_or_equal ->
+        return (int_typ, int_typ, bool_typ)
+      | Binary_equal | Binary_unequal ->
+        let* fresh_var = make_fresh_var in
+        return (fresh_var, fresh_var, bool_typ)
+      | Binary_cons ->
+        let* fresh_var = make_fresh_var in
+        return (fresh_var, Type_list fresh_var, Type_list fresh_var)
+    in
+    let* subst3 = Substitution.unify (Substitution.apply subst2 typ1) e1typ in
+    let* subst4 = Substitution.unify (Substitution.apply subst3 typ2) e2typ in
+    let* subst_res = Substitution.compose_all [ subst1; subst2; subst3; subst4 ] in
+    return (subst_res, Substitution.apply subst_res etyp)
+  | Option None ->
+    let* fresh_typ = make_fresh_var in
+    return (Substitution.empty, TOption fresh_typ)
+  | Option (Some e) ->
+    let* subst, typ = infer_expr env e in
+    return (subst, TOption typ)
+  | Tuple (fst, snd, rest) ->
+    let* subst1, typ1 = infer_expr env fst in
+    let* subst2, typ2 = infer_expr env snd in
+    let* subst_rest, typs_rest =
+      List.fold_right
+        rest
+        ~f:(fun e acc ->
+          let* subst_acc, typs = acc in
+          let* subst, typ = infer_expr env e in
+          let* subst_acc = Substitution.compose subst_acc subst in
+          return (subst_acc, typ :: typs))
+        ~init:(return (Substitution.empty, []))
+    in
+    let* subst_result = Substitution.compose_all [ subst1; subst2; subst_rest ] in
+    return (subst_result, Type_tuple (typ1, typ2, typs_rest))
+  | List [] ->
+    let* fresh_var = make_fresh_var in
+    return (Substitution.empty, Type_list fresh_var)
+  | List (hd :: tl) ->
+    let* subst1, typ1 = infer_expr env hd in
+    let typ1 = Substitution.apply subst1 typ1 in
+    let* subst_unify, typ_unified =
+      List.fold
+        tl
+        ~f:(fun acc e ->
+          let* subst_acc, typ_acc = acc in
+          let* subst, typ = infer_expr env e in
+          let* subst_unify = unify typ_acc typ in
+          let typ_acc = Substitution.apply subst_unify typ_acc in
+          let* subst_acc = Substitution.compose_all [ subst; subst_acc; subst_unify ] in
+          return (subst_acc, typ_acc))
+        ~init:(return (subst1, typ1))
+    in
+    return (subst_unify, Type_list typ_unified)
+  | If_then_else (c, th, Some el) ->
+    let* subst1, typ1 = infer_expr env c in
+    let* subst2, typ2 = infer_expr (TypeEnvironment.apply subst1 env) th in
+    let* subst3, typ3 = infer_expr (TypeEnvironment.apply subst2 env) el in
+    let* subst4 = unify typ1 bool_typ in
+    let* subst5 = unify typ2 typ3 in
+    let* subst_result =
+      Substitution.compose_all [ subst1; subst2; subst3; subst4; subst5 ]
+    in
+    return (subst_result, Substitution.apply subst5 typ2)
+  | If_then_else (c, th, None) ->
+    let* subst1, typ1 = infer_expr env c in
+    let* subst2, typ2 = infer_expr (TypeEnvironment.apply subst1 env) th in
+    let* subst3 = unify typ1 bool_typ in
+    let* subst_result = Substitution.compose_all [ subst1; subst2; subst3 ] in
+    return (subst_result, Substitution.apply subst2 typ2)
+  | Apply (f, arg) ->
+    let* subst1, typ1 = infer_expr env f in
+    let* subst2, typ2 = infer_expr (TypeEnvironment.apply subst1 env) arg in
+    let typ1 = Substitution.apply subst2 typ1 in
+    let* fresh_var = make_fresh_var in
+    let* subst3 = unify typ1 (Arrow (typ2, fresh_var)) in
+    let* subst_result = Substitution.compose_all [ subst1; subst2; subst3 ] in
+    return (subst_result, Substitution.apply subst3 fresh_var)
+  | Lambda (arg, args, e) ->
+    let* env, arg_types = infer_patterns env ~shadow:true (arg :: args) in
+    let* subst, e_type = infer_expr env e in
+    return (subst, Substitution.apply subst (arrow_of_types arg_types e_type))
+  | LetIn (Rec, let_bind, let_binds, e) ->
+    let let_binds = let_bind :: let_binds in
+    let* env = extend_env_with_bind_names env let_binds in
+    let* env, subst1 = extend_env_with_let_binds env Rec let_binds in
+    let* subst2, typ = infer_expr env e in
+    let* subst_final = Substitution.compose subst1 subst2 in
+    return (subst_final, typ)
+  | LetIn (Nonrec, let_bind, let_binds, e) ->
+    let* env, subst1 = extend_env_with_let_binds env Nonrec (let_bind :: let_binds) in
+    let* subst2, typ = infer_expr env e in
+    let* subst_final = Substitution.compose subst1 subst2 in
+    return (subst_final, typ)
+  | Function ((p1, e1), rest) ->
+    let* arg_type = make_fresh_var in
+    let* return_type = make_fresh_var in
+    let* subst, return_type =
+      List.fold
+        ((p1, e1) :: rest)
+        ~init:(return (Substitution.empty, return_type))
+        ~f:(fun acc (pat, expr) ->
+          let* subst1, return_type = acc in
+          let* env, pat = infer_pattern env ~shadow:true pat in
+          let* subst2 = unify arg_type pat in
+          let env = TypeEnvironment.apply subst2 env in
+          let* subst3, expr_typ = infer_expr env expr in
+          let* subst4 = unify return_type expr_typ in
+          let* subst = Substitution.compose_all [ subst1; subst2; subst3; subst4 ] in
+          return (subst, Substitution.apply subst return_type))
+    in
+    return (subst, Arrow (Substitution.apply subst arg_type, return_type))
+  | Match (e, (p1, e1), rest) ->
+    let* subst_init, match_type = infer_expr env e in
+    let env = TypeEnvironment.apply subst_init env in
+    let* return_type = make_fresh_var in
+    let* subst, return_type =
+      List.fold
+        ((p1, e1) :: rest)
+        ~init:(return (subst_init, return_type))
+        ~f:(fun acc (pat, expr) ->
+          let* subst1, return_type = acc in
+          let* env, pat = infer_pattern env ~shadow:true pat in
+          let* subst2 = unify match_type pat in
+          let* subst12 = Substitution.compose subst1 subst2 in
+          let env = TypeEnvironment.apply subst12 env in
+          let* subst3, expr_typ = infer_expr env expr in
+          let* subst4 = unify return_type expr_typ in
+          let* subst = Substitution.compose_all [ subst12; subst3; subst4 ] in
+          return (subst, Substitution.apply subst return_type))
+    in
+    return (subst, return_type)
+  | EConstraint (e, t) ->
+    let* subst1, e_type = infer_expr env e in
+    let* subst2 = unify e_type (Substitution.apply subst1 t) in
+    let* subst_result = Substitution.compose subst1 subst2 in
+    return (subst_result, Substitution.apply subst2 e_type)
+
+and extend_env_with_let_binds env is_rec let_binds =
+  List.fold
+    let_binds
+    ~init:(return (env, Substitution.empty))
+    ~f:(fun acc let_bind ->
+      let* env, subst_acc = acc in
+      let* subst, names_schemes_list = infer_let_bind env is_rec let_bind in
+      let env = TypeEnvironment.extend_many env names_schemes_list in
+      let env = TypeEnvironment.apply subst env in
+      let* subst_acc = Substitution.compose subst_acc subst in
+      return (env, subst_acc))
+
+and infer_let_bind env is_rec let_bind =
+  let* (Let_bind (name, args, e)) = check_let_bind_correctness is_rec let_bind in
+  let* env, args_types = infer_patterns env ~shadow:true args in
+  let* subst1, rvalue_type = infer_expr env e in
+  let bind_type = Substitution.apply subst1 (arrow_of_types args_types rvalue_type) in
+  (* If let_bind is recursive, then bind_varname was already in environment *)
+  let* env, name_type =
+    match is_rec with
+    | Nonrec -> infer_pattern env ~shadow:true name
+    | Rec -> infer_pattern env ~shadow:false name
+  in
+  let* subst2 = unify (Substitution.apply subst1 name_type) bind_type in
+  let* subst = Substitution.compose subst1 subst2 in
+  let env = TypeEnvironment.apply subst env in
+  let names = extract_names_from_pattern name in
+  let arg_names = extract_names_from_patterns args in
+  let names_types = List.map names ~f:(fun n -> n, TypeEnvironment.find_typ_exn env n) in
+  let env = TypeEnvironment.remove_many env (List.concat [ names; arg_names ]) in
+  let names_schemes_list =
+    List.map names_types ~f:(fun (name, name_type) -> name, generalize env name_type)
+  in
+  return (subst, names_schemes_list)
+;;
+
+let infer_statement env = function
+  | Let (Rec, let_bind, let_binds) ->
+    let let_binds = let_bind :: let_binds in
+    let* env = extend_env_with_bind_names env let_binds in
+    let* env, _ = extend_env_with_let_binds env Rec let_binds in
+    let bind_names = extract_bind_names_from_let_binds let_binds in
+    let bind_names_with_types =
+      List.map bind_names ~f:(fun name ->
+        match TypeEnvironment.find_exn env name with
+        | Scheme (_, typ) -> name, typ)
+    in
+    return (env, bind_names_with_types)
+  | Let (Nonrec, let_bind, let_binds) ->
+    let let_binds = let_bind :: let_binds in
+    let* env, _ = extend_env_with_let_binds env Nonrec let_binds in
+    let bind_names = extract_bind_names_from_let_binds let_binds in
+    let bind_names_with_types =
+      List.map bind_names ~f:(fun name ->
+        match TypeEnvironment.find_exn env name with
+        | Scheme (_, typ) -> name, typ)
+    in
+    return (env, bind_names_with_types)
+;;
+
+let infer_construction env = function
+  | Expr exp ->
+    let* _, typ = infer_expr env exp in
+    return (env, [ "-", typ ])
+  | Statement s ->
+    let* env, names_and_types = infer_statement env s in
+    return (env, names_and_types)
+;;
+
+let infer c env state = run (infer_construction env c) state
diff --git a/FSharpActivePatterns/lib/inferencer.mli b/FSharpActivePatterns/lib/inferencer.mli
new file mode 100644
index 000000000..770439acc
--- /dev/null
+++ b/FSharpActivePatterns/lib/inferencer.mli
@@ -0,0 +1,31 @@
+(** Copyright 2024-2025, Ksenia Kotelnikova <xeniia.ka@gmail.com>, Gleb Nasretdinov <gleb.nasretdinov@proton.me> *)
+
+(** SPDX-License-Identifier: LGPL-3.0-or-later *)
+
+open Ast
+open TypedTree
+open Format
+
+module TypeEnvironment : sig
+  type t
+
+  val empty : t
+  val extend : t -> string -> scheme -> t
+end
+
+type error =
+  [ `Occurs_check
+  | `Undef_var of string
+  | `Unification_failed of typ * typ
+  | `Not_allowed_right_hand_side_let_rec
+  | `Not_allowed_left_hand_side_let_rec
+  | `Args_after_not_variable_let
+  ]
+
+val pp_error : formatter -> error -> unit
+
+val infer
+  :  construction
+  -> TypeEnvironment.t
+  -> int
+  -> int * (TypeEnvironment.t * (string * typ) list, error) result
diff --git a/FSharpActivePatterns/lib/keywordChecker.ml b/FSharpActivePatterns/lib/keywordChecker.ml
index 0e8fe5e00..ff3687d1f 100644
--- a/FSharpActivePatterns/lib/keywordChecker.ml
+++ b/FSharpActivePatterns/lib/keywordChecker.ml
@@ -17,6 +17,11 @@ let is_keyword = function
   | "and"
   | "Some"
   | "None"
+  | "function"
+  | "->"
+  | "|"
+  | ":"
+  | "::"
   | "_" -> true
   | _ -> false
 ;;
diff --git a/FSharpActivePatterns/lib/parser.ml b/FSharpActivePatterns/lib/parser.ml
index a85b8706a..4d83c29ab 100644
--- a/FSharpActivePatterns/lib/parser.ml
+++ b/FSharpActivePatterns/lib/parser.ml
@@ -6,6 +6,7 @@ open Angstrom
 open Ast
 open Base
 open KeywordChecker
+open TypedTree
 
 (* TECHNICAL FUNCTIONS *)
 
@@ -24,7 +25,13 @@ let peek_sep1 =
   match c with
   | None -> return None
   | Some c ->
-    if is_ws c || Char.equal c '(' || Char.equal c ')' || Char.equal c ','
+    if is_ws c
+       || Char.equal c '('
+       || Char.equal c ')'
+       || Char.equal c ','
+       || Char.equal c ']'
+       || Char.equal c ':'
+       || Char.equal c ';'
     then return (Some c)
     else fail "need a delimiter"
 ;;
@@ -93,16 +100,37 @@ let p_string =
 let p_string_expr = expr_const_factory p_string
 let p_string_pat = pat_const_factory p_string
 
-let p_type =
-  skip_ws
-  *> char ':'
-  *> skip_ws
-  *> (choice [ string "int"; string "bool" ] >>| fun var_type -> Some var_type)
-  <|> return None
+let p_inf_oper =
+  let* oper =
+    skip_ws
+    *> take_while1 (function
+      | '+'
+      | '-'
+      | '<'
+      | '>'
+      | '*'
+      | '|'
+      | '!'
+      | '$'
+      | '%'
+      | '&'
+      | '.'
+      | '/'
+      | ':'
+      | '='
+      | '?'
+      | '@'
+      | '^'
+      | '~' -> true
+      | _ -> false)
+  in
+  if is_keyword oper
+  then fail "keywords are not allowed as variable names"
+  else return (Ident oper)
 ;;
 
-let p_ident =
-  let find_string =
+let p_varname =
+  let* name =
     skip_ws
     *> lift2
          ( ^ )
@@ -113,13 +141,17 @@ let p_ident =
            | 'a' .. 'z' | 'A' .. 'Z' | '_' | '0' .. '9' -> true
            | _ -> false))
   in
-  find_string
-  >>= fun str ->
-  if is_keyword str
+  if is_keyword name
   then fail "keywords are not allowed as variable names"
-  else p_type >>| fun type_opt -> Ident (str, type_opt)
+  else return name
+;;
+
+let p_ident =
+  let* varname = p_varname in
+  return (Ident varname)
 ;;
 
+let p_type = skip_ws *> char ':' *> skip_ws *> p_varname >>| fun s -> Primitive s
 let p_var_expr = p_ident >>| fun ident -> Variable ident
 let p_var_pat = p_ident >>| fun ident -> PVar ident
 
@@ -179,15 +211,13 @@ let p_cons_list_pat p_pat =
 ;;
 
 let p_tuple make p =
-  skip_ws
-  *> string "("
-  *> lift3
-       make
-       p
-       (skip_ws *> string "," *> skip_ws *> p)
-       (many (skip_ws *> string "," *> skip_ws *> p))
-  <* skip_ws
-  <* string ")"
+  let tuple =
+    let* fst = p <* skip_ws <* string "," in
+    let* snd = p in
+    let* rest = many (skip_ws *> string "," *> p) in
+    return (make fst snd rest)
+  in
+  p_parens tuple <|> tuple
 ;;
 
 let p_tuple_pat p_pat = p_tuple make_tuple_pat p_pat
@@ -204,15 +234,42 @@ let p_if p_expr =
      <|> return None)
 ;;
 
-let p_let_bind p_expr =
+let p_option p make_option =
+  skip_ws *> string "None" *> peek_sep1 *> return (make_option None)
+  <|> let+ inner = skip_ws *> string "Some" *> peek_sep1 *> p in
+      make_option (Some inner)
+;;
+
+let make_option_expr expr = Option expr
+let make_option_pat pat = POption pat
+let p_wild_pat = skip_ws *> string "_" *> return Wild
+
+let p_pat_const =
+  choice [ p_int_pat; p_bool_pat; p_unit_pat; p_string_pat; p_var_pat; p_wild_pat ]
+;;
+
+let p_constraint_pat p_pat =
+  let* pat = p_pat in
+  let* typ = p_type in
+  return (PConstraint (pat, typ))
+;;
+
+let p_pat =
   skip_ws
-  *> string "and"
-  *> peek_sep1
-  *> lift3
-       (fun name args body -> Let_bind (name, args, body))
-       p_ident
-       (many p_ident)
-       (skip_ws *> string "=" *> p_expr)
+  *> fix (fun self ->
+    let atom = choice [ p_pat_const; p_parens self; p_parens (p_constraint_pat self) ] in
+    let semicolon_list = p_semicolon_list_pat (self <|> atom) <|> atom in
+    let opt = p_option semicolon_list make_option_pat <|> semicolon_list in
+    let tuple = p_tuple_pat opt <|> opt in
+    let cons = p_cons_list_pat tuple in
+    cons)
+;;
+
+let p_let_bind p_expr =
+  let* name = p_pat <|> (p_parens p_inf_oper >>| fun oper -> PVar oper) in
+  let* args = many p_pat in
+  let* body = skip_ws *> string "=" *> p_expr in
+  return (Let_bind (name, args, body))
 ;;
 
 let p_letin p_expr =
@@ -221,12 +278,10 @@ let p_letin p_expr =
   *> skip_ws_sep1
   *>
   let* rec_flag = string "rec" *> peek_sep1 *> return Rec <|> return Nonrec in
-  let* name = p_ident in
-  let* args = many p_ident in
-  let* body = skip_ws *> string "=" *> p_expr in
-  let* let_bind_list = many (p_let_bind p_expr) in
+  let* let_bind1 = p_let_bind p_expr in
+  let* let_binds = many (skip_ws *> string "and" *> peek_sep1 *> p_let_bind p_expr) in
   let* in_expr = skip_ws *> string "in" *> peek_sep1 *> p_expr in
-  return (LetIn (rec_flag, Let_bind (name, args, body), let_bind_list, in_expr))
+  return (LetIn (rec_flag, let_bind1, let_binds, in_expr))
 ;;
 
 let p_let p_expr =
@@ -235,61 +290,67 @@ let p_let p_expr =
   *> skip_ws_sep1
   *>
   let* rec_flag = string "rec" *> peek_sep1 *> return Rec <|> return Nonrec in
-  let* name = p_ident in
-  let* args = many p_ident in
-  let* body = skip_ws *> string "=" *> p_expr in
-  let* let_bind_list = many (p_let_bind p_expr) in
-  return (Let (rec_flag, Let_bind (name, args, body), let_bind_list))
+  let* let_bind1 = p_let_bind p_expr in
+  let* let_binds = many (skip_ws *> string "and" *> peek_sep1 *> p_let_bind p_expr) in
+  return (Let (rec_flag, let_bind1, let_binds))
 ;;
 
-let p_apply p_expr = chainl1 p_expr (return (fun expr1 expr2 -> Apply (expr1, expr2)))
+let p_apply p_expr =
+  chainl1 (p_expr <* peek_sep1) (return (fun expr1 expr2 -> Apply (expr1, expr2)))
+;;
 
-let p_option p make_option =
-  skip_ws *> string "None" *> peek_sep1 *> return (make_option None)
-  <|> let+ inner = skip_ws *> string "Some" *> peek_sep1 *> p in
-      make_option (Some inner)
+let p_lambda p_expr =
+  skip_ws
+  *> string "fun"
+  *> peek_sep1
+  *>
+  let* arg1 = p_pat in
+  let* args = many p_pat <* skip_ws <* string "->" in
+  let* body = p_expr in
+  return (Lambda (arg1, args, body))
 ;;
 
-let make_option_expr expr = Option expr
-let make_option_pat pat = POption pat
-let p_wild_pat = skip_ws *> string "_" *> return Wild
+let p_case p_expr =
+  let* pat = skip_ws *> string "|" *> p_pat <* skip_ws <* string "->" in
+  let* expr = p_expr in
+  return (pat, expr)
+;;
 
-let p_pat_const =
-  choice [ p_int_pat; p_bool_pat; p_unit_pat; p_string_pat; p_var_pat; p_wild_pat ]
+let p_first_case p_expr =
+  let* pat = skip_ws *> (string "|" *> p_pat <|> p_pat) <* skip_ws <* string "->" in
+  let* expr = p_expr in
+  return (pat, expr)
 ;;
 
-let p_pat =
-  skip_ws
-  *> fix (fun self ->
-    let atom = choice [ p_pat_const; p_parens self ] in
-    let tuple = p_tuple_pat (self <|> atom) <|> atom in
-    let semicolon_list = p_semicolon_list_pat (self <|> tuple) <|> tuple in
-    let opt = p_option semicolon_list make_option_pat <|> semicolon_list in
-    let cons = p_cons_list_pat opt in
-    cons)
+let p_match p_expr =
+  let* value = skip_ws *> string "match" *> p_expr <* skip_ws <* string "with" in
+  let* pat1, expr1 = p_first_case p_expr in
+  let* cases = many (p_case p_expr) in
+  return (Match (value, (pat1, expr1), cases))
 ;;
 
-let p_lambda p_expr =
+let p_function p_expr =
   skip_ws
-  *> string "fun"
-  *> peek_sep1
+  *> string "function"
   *>
-  let* pat = p_pat in
-  let* pat_list = many p_pat <* skip_ws <* string "->" in
-  let* body = p_expr in
-  return (Lambda (pat, pat_list, body))
+  let* pat1, expr1 = p_first_case p_expr in
+  let* cases = many (p_case p_expr) in
+  return (Function ((pat1, expr1), cases))
 ;;
 
-let p_match p_expr =
-  lift4
-    (fun value first_pat first_expr cases -> Match (value, first_pat, first_expr, cases))
-    (skip_ws *> string "match" *> skip_ws *> p_expr <* skip_ws <* string "with")
-    (skip_ws *> string "|" *> skip_ws *> p_pat <* skip_ws <* string "->" <* skip_ws)
-    (p_expr <* skip_ws)
-    (many
-       (let* pat = skip_ws *> string "|" *> p_pat <* skip_ws <* string "->" in
-        let* expr = p_expr in
-        return (pat, expr)))
+let p_inf_oper_expr p_expr =
+  skip_ws
+  *> chainl1
+       p_expr
+       (p_inf_oper
+        >>= fun op ->
+        return (fun expr1 expr2 -> Apply (Apply (Variable op, expr1), expr2)))
+;;
+
+let p_constraint_expr p_expr =
+  let* expr = p_expr in
+  let* typ = p_type in
+  return (EConstraint (expr, typ))
 ;;
 
 let p_expr =
@@ -304,14 +365,15 @@ let p_expr =
         ; p_bool_expr
         ; p_parens p_expr
         ; p_semicolon_list_expr p_expr
+        ; p_parens (p_constraint_expr p_expr)
         ]
     in
-    let tuple = p_tuple make_tuple_expr (p_expr <|> atom) <|> atom in
-    let if_expr = p_if (p_expr <|> tuple) <|> tuple in
+    let if_expr = p_if (p_expr <|> atom) <|> atom in
     let letin_expr = p_letin (p_expr <|> if_expr) <|> if_expr in
     let option = p_option letin_expr make_option_expr <|> letin_expr in
     let apply = p_apply option <|> option in
-    let unary = choice [ unary_chain p_not apply; unary_chain unminus apply ] in
+    let tuple = p_tuple make_tuple_expr apply <|> apply in
+    let unary = choice [ unary_chain p_not tuple; unary_chain unminus tuple ] in
     let factor = chainl1 unary (mul <|> div) in
     let term = chainl1 factor (add <|> sub) in
     let cons_op = chainr1 term cons in
@@ -323,7 +385,9 @@ let p_expr =
     let bit_or = chainl1 bit_and bitwise_or in
     let comp_and = chainl1 bit_or log_and in
     let comp_or = chainl1 comp_and log_or in
-    let ematch = p_match (p_expr <|> comp_or) <|> comp_or in
+    let inf_oper = p_inf_oper_expr comp_or <|> comp_or in
+    let p_function = p_function (p_expr <|> inf_oper) <|> inf_oper in
+    let ematch = p_match (p_expr <|> p_function) <|> p_function in
     let efun = p_lambda (p_expr <|> ematch) <|> ematch in
     efun)
 ;;
@@ -336,7 +400,5 @@ let p_construction =
 
 (* MAIN PARSE FUNCTION *)
 let parse (str : string) =
-  match parse_string ~consume:All (skip_ws *> p_construction <* skip_ws) str with
-  | Ok ast -> Some ast
-  | Error _ -> None
+  parse_string ~consume:All (skip_ws *> p_construction <* skip_ws) str
 ;;
diff --git a/FSharpActivePatterns/lib/parser.mli b/FSharpActivePatterns/lib/parser.mli
index 19a074986..6d0484176 100644
--- a/FSharpActivePatterns/lib/parser.mli
+++ b/FSharpActivePatterns/lib/parser.mli
@@ -4,4 +4,4 @@
 
 open Ast
 
-val parse : string -> construction option
+val parse : string -> (construction, string) result
diff --git a/FSharpActivePatterns/lib/prettyPrinter.ml b/FSharpActivePatterns/lib/prettyPrinter.ml
index 515606542..e4eeb1117 100644
--- a/FSharpActivePatterns/lib/prettyPrinter.ml
+++ b/FSharpActivePatterns/lib/prettyPrinter.ml
@@ -4,6 +4,7 @@
 
 open Ast
 open Format
+open TypesPp
 
 let pp_bin_op fmt = function
   | Binary_equal -> fprintf fmt "= "
@@ -50,11 +51,12 @@ let rec pp_pattern fmt = function
       (p1 :: p2 :: rest);
     fprintf fmt ")"
   | PConst literal -> fprintf fmt "%a " pp_expr (Const literal)
-  | PVar (Ident (name, _)) -> fprintf fmt "%s " name
+  | PVar (Ident name) -> fprintf fmt "%s " name
   | POption p ->
     (match p with
      | None -> fprintf fmt "None "
      | Some p -> fprintf fmt "Some (%a) " pp_pattern p)
+  | PConstraint (p, t) -> fprintf fmt "(%a : %a) " pp_pattern p pp_typ t
 
 and pp_expr fmt expr =
   match expr with
@@ -70,12 +72,29 @@ and pp_expr fmt expr =
     fprintf fmt "(";
     pp_print_list ~pp_sep:(fun fmt () -> fprintf fmt ", ") pp_expr fmt (e1 :: e2 :: rest);
     fprintf fmt ")"
-  | Match (value, pat1, expr1, cases) ->
+  | Function ((pat1, expr1), cases) ->
+    let cases =
+      List.map
+        (function
+          | a, b -> a, b)
+        cases
+    in
+    fprintf fmt "function ";
+    List.iter
+      (fun (pat, expr) -> fprintf fmt "| %a -> (%a) \n" pp_pattern pat pp_expr expr)
+      ((pat1, expr1) :: cases)
+  | Match (value, (pat1, expr1), cases) ->
+    let cases =
+      List.map
+        (function
+          | p, e -> p, e)
+        cases
+    in
     fprintf fmt "match (%a) with \n" pp_expr value;
     List.iter
       (fun (pat, expr) -> fprintf fmt "| %a -> (%a) \n" pp_pattern pat pp_expr expr)
       ((pat1, expr1) :: cases)
-  | Variable (Ident (name, _)) -> fprintf fmt "%s " name
+  | Variable (Ident name) -> fprintf fmt "%s " name
   | Unary_expr (op, expr) -> fprintf fmt "%a (%a)" pp_unary_op op pp_expr expr
   | Bin_expr (op, left, right) ->
     fprintf fmt "(%a) %a (%a)" pp_expr left pp_bin_op op pp_expr right
@@ -84,11 +103,14 @@ and pp_expr fmt expr =
     (match else_body with
      | Some body -> fprintf fmt "else %a " pp_expr body
      | None -> ())
-  | Lambda (pat1, pat_list, body) ->
+  | Lambda (arg1, args, body) ->
     fprintf fmt "fun ";
-    List.iter (fun pat -> fprintf fmt "%a " pp_pattern pat) (pat1 :: pat_list);
+    List.iter (fun pat -> fprintf fmt "(%a) " pp_pattern pat) (arg1 :: args);
     fprintf fmt "-> %a " pp_expr body
-  | Apply (func, arg) -> fprintf fmt "(%a) (%a)" pp_expr func pp_expr arg
+  | Apply (Apply (Variable (Ident op), left), right)
+    when String.for_all (fun c -> String.contains "!$%&*+-./:<=>?@^|~" c) op ->
+    fprintf fmt "(%a) %s (%a)" pp_expr left op pp_expr right
+  | Apply (func, arg) -> fprintf fmt "(%a) %a" pp_expr func pp_expr arg
   | LetIn (rec_flag, let_bind, let_bind_list, in_expr) ->
     fprintf fmt "let %a " pp_rec_flag rec_flag;
     pp_print_list
@@ -102,21 +124,19 @@ and pp_expr fmt expr =
     (match e with
      | None -> fprintf fmt "None "
      | Some e -> fprintf fmt "Some (%a)" pp_expr e)
+  | EConstraint (e, t) -> fprintf fmt "(%a : %a) " pp_expr e pp_typ t
 
 and pp_args fmt args =
   let open Format in
   pp_print_list
     ~pp_sep:pp_print_space
-    (fun fmt name -> fprintf fmt "%s" name)
+    (fun fmt arg -> fprintf fmt "%a" pp_pattern arg)
     fmt
-    (List.map
-       (function
-         | Ident (s, _) -> s)
-       args)
+    args
 
 and pp_let_bind fmt = function
-  | Let_bind (Ident (name, _), args, body) ->
-    fprintf fmt "%s %a = %a " name pp_args args pp_expr body
+  | Let_bind (name, args, body) ->
+    fprintf fmt "%a %a = %a " pp_pattern name pp_args args pp_expr body
 ;;
 
 let pp_statement fmt = function
diff --git a/FSharpActivePatterns/lib/tests/ast_printer.ml b/FSharpActivePatterns/lib/tests/ast_printer.ml
index fff43e0a9..c68ae1950 100644
--- a/FSharpActivePatterns/lib/tests/ast_printer.ml
+++ b/FSharpActivePatterns/lib/tests/ast_printer.ml
@@ -14,23 +14,22 @@ let%expect_test "print Ast factorial" =
       , If_then_else
           ( Bin_expr
               ( Logical_or
-              , Bin_expr (Binary_equal, Variable (Ident ("n", None)), Const (Int_lt 0))
-              , Bin_expr (Binary_equal, Variable (Ident ("n", None)), Const (Int_lt 1)) )
+              , Bin_expr (Binary_equal, Variable (Ident "n"), Const (Int_lt 0))
+              , Bin_expr (Binary_equal, Variable (Ident "n"), Const (Int_lt 1)) )
           , Const (Int_lt 1)
           , Some
               (Bin_expr
                  ( Binary_multiply
-                 , Variable (Ident ("n", None))
+                 , Variable (Ident "n")
                  , Apply
-                     ( Variable (Ident ("factorial", None))
-                     , Bin_expr
-                         (Binary_subtract, Variable (Ident ("n", None)), Const (Int_lt 1))
+                     ( Variable (Ident "factorial")
+                     , Bin_expr (Binary_subtract, Variable (Ident "n"), Const (Int_lt 1))
                      ) )) ) )
   in
   let program =
-    [ Statement (Let (Nonrec, Let_bind (Ident ("a", None), [], Const (Int_lt 10)), []))
+    [ Statement (Let (Nonrec, Let_bind (PVar (Ident "a"), [], Const (Int_lt 10)), []))
     ; Expr factorial
-    ; Expr (Apply (factorial, Variable (Ident ("a", None))))
+    ; Expr (Apply (factorial, Variable (Ident "a")))
     ]
   in
   List.iter (print_construction std_formatter) program;
@@ -107,7 +106,7 @@ let%expect_test "print Ast factorial" =
 ;;
 
 let%expect_test "print Ast double func" =
-  let ident = Ident ("n", None) in
+  let ident = Ident "n" in
   let pat = PConst (Int_lt 4) in
   let args = [] in
   let binary_expr = Bin_expr (Binary_multiply, Const (Int_lt 2), Variable ident) in
@@ -199,9 +198,9 @@ let%expect_test "print Ast of LetIn" =
     Expr
       (LetIn
          ( Nonrec
-         , Let_bind (Ident ("x", None), [], Const (Int_lt 5))
+         , Let_bind (PVar (Ident "x"), [], Const (Int_lt 5))
          , []
-         , Bin_expr (Binary_add, Variable (Ident ("x", None)), Const (Int_lt 5)) ))
+         , Bin_expr (Binary_add, Variable (Ident "x"), Const (Int_lt 5)) ))
   in
   print_construction std_formatter sum;
   [%expect
@@ -221,13 +220,12 @@ let%expect_test "print Ast of match_expr" =
   let patterns =
     [ PConst (Int_lt 5)
     ; PConst (String_lt " bar foo")
-    ; PList [ Wild; PVar (Ident ("xs", None)) ]
+    ; PList [ Wild; PVar (Ident "xs") ]
     ]
   in
   let pattern_values = List.map (fun p -> p, Const (Int_lt 4)) patterns in
   let match_expr =
-    Match
-      (Variable (Ident ("x", None)), PConst (Int_lt 4), Const (Int_lt 4), pattern_values)
+    Match (Variable (Ident "x"), (PConst (Int_lt 4), Const (Int_lt 4)), pattern_values)
   in
   print_construction std_formatter (Expr match_expr);
   [%expect
diff --git a/FSharpActivePatterns/lib/tests/qcheck_utils.ml b/FSharpActivePatterns/lib/tests/qcheck_utils.ml
index 10146c212..fd6cde746 100644
--- a/FSharpActivePatterns/lib/tests/qcheck_utils.ml
+++ b/FSharpActivePatterns/lib/tests/qcheck_utils.ml
@@ -29,6 +29,7 @@ let rec shrink_let_bind =
     shrink_expr e
     >|= (fun a' -> Let_bind (name, args, a'))
     <+> (QCheck.Shrink.list args >|= fun a' -> Let_bind (name, a', e))
+    <+> (shrink_pattern name >|= fun a' -> Let_bind (a', args, e))
 
 and shrink_expr =
   let open QCheck.Iter in
@@ -68,12 +69,11 @@ and shrink_expr =
     shrink_expr body
     >|= (fun body' -> Lambda (pat, pat_list, body'))
     <+> (QCheck.Shrink.list ~shrink:shrink_pattern pat_list
-         >|= fun pat_list' -> Lambda (pat, pat_list', body))
-  | Match (value, pat1, expr1, cases) ->
-    of_list [ value; expr1 ]
-    <+> (shrink_expr value >|= fun a' -> Match (a', pat1, expr1, cases))
-    <+> (shrink_pattern pat1 >|= fun a' -> Match (value, a', expr1, cases))
-    <+> (shrink_expr expr1 >|= fun a' -> Match (value, pat1, a', cases))
+         >|= fun a' -> Lambda (pat, a', body))
+  | Function ((pat1, expr1), cases) ->
+    of_list (expr1 :: List.map snd cases)
+    <+> (shrink_pattern pat1 >|= fun a' -> Function ((a', expr1), cases))
+    <+> (shrink_expr expr1 >|= fun a' -> Function ((pat1, a'), cases))
     <+> (QCheck.Shrink.list
            ~shrink:(fun (p, e) ->
              (let* p_shr = shrink_pattern p in
@@ -82,11 +82,26 @@ and shrink_expr =
              let* e_shr = shrink_expr e in
              return (p, e_shr))
            cases
-         >|= fun a' -> Match (value, pat1, expr1, a'))
+         >|= fun a' -> Function ((pat1, expr1), a'))
+  | Match (value, (pat1, expr1), cases) ->
+    of_list (value :: expr1 :: List.map snd cases)
+    <+> (shrink_expr value >|= fun a' -> Match (a', (pat1, expr1), cases))
+    <+> (shrink_pattern pat1 >|= fun a' -> Match (value, (a', expr1), cases))
+    <+> (shrink_expr expr1 >|= fun a' -> Match (value, (pat1, a'), cases))
+    <+> (QCheck.Shrink.list
+           ~shrink:(fun (p, e) ->
+             (let* p_shr = shrink_pattern p in
+              return (p_shr, e))
+             <+>
+             let* e_shr = shrink_expr e in
+             return (p, e_shr))
+           cases
+         >|= fun a' -> Match (value, (pat1, expr1), a'))
   | Option (Some e) ->
     of_list [ e; Option None ] <+> (shrink_expr e >|= fun a' -> Option (Some a'))
   | Option None -> empty
   | Variable _ -> empty
+  | EConstraint (e, _) -> return e
 
 and shrink_pattern =
   let open QCheck.Iter in
@@ -107,6 +122,7 @@ and shrink_pattern =
   | POption None -> empty
   | Wild -> empty
   | PVar _ -> empty
+  | PConstraint (p, _) -> return p
 ;;
 
 let shrink_statement =
@@ -141,6 +157,6 @@ let run n =
   QCheck_base_runner.run_tests
     [ QCheck.(
         Test.make arbitrary_construction ~count:n (fun c ->
-          Some c = parse (Format.asprintf "%a\n" pp_construction c)))
+          Ok c = parse (Format.asprintf "%a\n" pp_construction c)))
     ]
 ;;
diff --git a/FSharpActivePatterns/lib/typedTree.ml b/FSharpActivePatterns/lib/typedTree.ml
new file mode 100644
index 000000000..44aee06e8
--- /dev/null
+++ b/FSharpActivePatterns/lib/typedTree.ml
@@ -0,0 +1,41 @@
+(** Copyright 2024-2025, Ksenia Kotelnikova <xeniia.ka@gmail.com>, Gleb Nasretdinov <gleb.nasretdinov@proton.me> *)
+
+(** SPDX-License-Identifier: LGPL-3.0-or-later *)
+
+type binder = int [@@deriving show { with_path = false }, qcheck]
+
+let gen_primitive = QCheck.Gen.oneofl [ "int"; "bool"; "string"; "unit" ]
+
+type typ =
+  | Primitive of (string[@gen gen_primitive])
+  | Type_var of binder
+  | Arrow of typ * typ
+  | Type_list of typ
+  | Type_tuple of typ * typ * typ list
+  | TOption of typ
+[@@deriving show { with_path = false }, qcheck]
+
+let arrow_of_types first_types last_type =
+  let open Base in
+  List.fold_right first_types ~init:last_type ~f:(fun left right -> Arrow (left, right))
+;;
+
+module VarSet = struct
+  include Stdlib.Set.Make (Int)
+
+  let pp fmt s =
+    Format.fprintf fmt "[ ";
+    iter (Format.fprintf fmt "%d; ") s;
+    Format.fprintf fmt "]"
+  ;;
+end
+
+type binder_set = VarSet.t [@@deriving show { with_path = false }]
+
+(* binder_set here -- list of all type vars in context (?) *)
+type scheme = Scheme of binder_set * typ [@@deriving show { with_path = false }]
+
+let int_typ = Primitive "int"
+let bool_typ = Primitive "bool"
+let string_typ = Primitive "string"
+let unit_typ = Primitive "unit"
diff --git a/FSharpActivePatterns/lib/typedTree.mli b/FSharpActivePatterns/lib/typedTree.mli
new file mode 100644
index 000000000..b3e5dc4bf
--- /dev/null
+++ b/FSharpActivePatterns/lib/typedTree.mli
@@ -0,0 +1,31 @@
+(** Copyright 2024-2025, Ksenia Kotelnikova <xeniia.ka@gmail.com>, Gleb Nasretdinov <gleb.nasretdinov@proton.me> *)
+
+(** SPDX-License-Identifier: LGPL-3.0-or-later *)
+
+type binder = int
+
+type typ =
+  | Primitive of string
+  | Type_var of binder
+  | Arrow of typ * typ
+  | Type_list of typ
+  | Type_tuple of typ * typ * typ list
+  | TOption of typ
+
+val gen_typ_sized : int -> typ QCheck.Gen.t
+val pp_typ : Format.formatter -> typ -> unit
+val arrow_of_types : typ list -> typ -> typ
+
+module VarSet : sig
+  include module type of Stdlib.Set.Make (Int)
+
+  val pp : Format.formatter -> t -> unit
+end
+
+type binder_set = VarSet.t
+type scheme = Scheme of binder_set * typ [@@deriving show { with_path = false }]
+
+val int_typ : typ
+val bool_typ : typ
+val string_typ : typ
+val unit_typ : typ
diff --git a/FSharpActivePatterns/lib/typesPp.ml b/FSharpActivePatterns/lib/typesPp.ml
new file mode 100644
index 000000000..418cf6366
--- /dev/null
+++ b/FSharpActivePatterns/lib/typesPp.ml
@@ -0,0 +1,29 @@
+(** Copyright 2024-2025, Ksenia Kotelnikova <xeniia.ka@gmail.com>, Gleb Nasretdinov <gleb.nasretdinov@proton.me> *)
+
+(** SPDX-License-Identifier: LGPL-3.0-or-later *)
+
+open TypedTree
+open Format
+
+let pp_typ fmt typ =
+  let rec helper fmt = function
+    | Primitive s -> fprintf fmt "%s" s
+    | Type_var var -> fprintf fmt "'_%d" var
+    | Arrow (fst, snd) ->
+      (match fst with
+       | Arrow _ -> fprintf fmt "(%a) -> %a" helper fst helper snd
+       | _ -> fprintf fmt "%a -> %a" helper fst helper snd)
+    | Type_list typ -> fprintf fmt "%a list" helper typ
+    | Type_tuple (first, second, rest) ->
+      fprintf fmt "(";
+      Format.pp_print_list
+        ~pp_sep:(fun fmt () -> fprintf fmt ", ")
+        helper
+        fmt
+        (first :: second :: rest);
+      fprintf fmt ")"
+    | TOption t -> fprintf fmt "%a option" helper t
+  in
+  helper fmt typ;
+  fprintf fmt "\n"
+;;
diff --git a/FSharpActivePatterns/lib/typesPp.mli b/FSharpActivePatterns/lib/typesPp.mli
new file mode 100644
index 000000000..3b4a29818
--- /dev/null
+++ b/FSharpActivePatterns/lib/typesPp.mli
@@ -0,0 +1,8 @@
+(** Copyright 2024-2025, Ksenia Kotelnikova <xeniia.ka@gmail.com>, Gleb Nasretdinov <gleb.nasretdinov@proton.me> *)
+
+(** SPDX-License-Identifier: LGPL-3.0-or-later *)
+
+open TypedTree
+open Format
+
+val pp_typ : formatter -> typ -> unit
diff --git a/FSharpActivePatterns/tests/dune b/FSharpActivePatterns/tests/dune
index f2b8e0f4d..9ea42e28e 100644
--- a/FSharpActivePatterns/tests/dune
+++ b/FSharpActivePatterns/tests/dune
@@ -1,3 +1,28 @@
 (cram
  (applies_to qcheck)
  (deps ../lib/tests/run_qcheck.exe))
+
+(cram
+ (applies_to inference)
+ (deps
+  ../bin/REPL.exe
+  manytests/do_not_type/001.ml
+  manytests/do_not_type/002if.ml
+  manytests/do_not_type/003occurs.ml
+  manytests/do_not_type/004let_poly.ml
+  manytests/do_not_type/015tuples.ml
+  manytests/do_not_type/099.ml
+  manytests/typed/001fac.ml
+  manytests/typed/002fac.ml
+  manytests/typed/003fib.ml
+  manytests/typed/004manyargs.ml
+  manytests/typed/005fix.ml
+  manytests/typed/006partial.ml
+  manytests/typed/006partial2.ml
+  manytests/typed/006partial3.ml
+  manytests/typed/007order.ml
+  manytests/typed/008ascription.ml
+  manytests/typed/009let_poly.ml
+  manytests/typed/010sukharev.ml
+  manytests/typed/015tuples.ml
+  manytests/typed/016lists.ml))
diff --git a/FSharpActivePatterns/tests/inference.t b/FSharpActivePatterns/tests/inference.t
new file mode 100644
index 000000000..6c68b75a3
--- /dev/null
+++ b/FSharpActivePatterns/tests/inference.t
@@ -0,0 +1,97 @@
+  $ ../bin/REPL.exe -fromfile manytests/do_not_type/001.ml
+  Type checking failed: Undefined variable 'fac'
+  $ ../bin/REPL.exe -fromfile manytests/do_not_type/002if.ml
+  Type checking failed: unification failed on int
+   and bool
+  
+  $ ../bin/REPL.exe -fromfile manytests/do_not_type/003occurs.ml
+  Type checking failed: Occurs check failed
+  $ ../bin/REPL.exe -fromfile manytests/do_not_type/004let_poly.ml
+  Type checking failed: unification failed on bool
+   and int
+  
+  Type checking failed: unification failed on string
+   and int
+  
+  $ ../bin/REPL.exe -fromfile manytests/do_not_type/015tuples.ml
+  Type checking failed: Only variables are allowed as left-hand side of `let rec'
+  Type checking failed: unification failed on ('_0, '_1)
+   and (int, int, int)
+  
+  $ ../bin/REPL.exe -fromfile manytests/do_not_type/099.ml
+  Type checking failed: Only variables are allowed as left-hand side of `let rec'
+  Type checking failed: Undefined variable 'x'
+  Type checking failed: unification failed on '_1 option
+   and '_0 -> '_0
+  
+  Type checking failed: unification failed on unit
+   and '_2 -> '_2
+  
+  $ ../bin/REPL.exe -fromfile manytests/typed/001fac.ml
+  fac : int -> int
+  main : int
+  $ ../bin/REPL.exe -fromfile manytests/typed/002fac.ml
+  fac_cps : int -> (int -> '_7) -> '_7
+  main : int
+  $ ../bin/REPL.exe -fromfile manytests/typed/003fib.ml
+  fib_acc : int -> int -> int -> int
+  fib : int -> int
+  main : int
+  $ ../bin/REPL.exe -fromfile manytests/typed/004manyargs.ml
+  wrap : '_0 -> '_0
+  test3 : int -> int -> int -> int
+  test10 : int -> int -> int -> int -> int -> int -> int -> int -> int -> int -> int
+  main : int
+  $ ../bin/REPL.exe -fromfile manytests/typed/005fix.ml
+  fix : (('_1 -> '_5) -> '_1 -> '_5) -> '_1 -> '_5
+  fac : (int -> int) -> int -> int
+  main : int
+  $ ../bin/REPL.exe -fromfile manytests/typed/006partial.ml
+  foo : bool -> int -> int
+  foo : int -> int
+  main : int
+  $ ../bin/REPL.exe -fromfile manytests/typed/006partial2.ml
+  foo : int -> int -> int -> int
+  main : int
+  $ ../bin/REPL.exe -fromfile manytests/typed/006partial3.ml
+  foo : int -> int -> int -> unit
+  main : int
+  $ ../bin/REPL.exe -fromfile manytests/typed/007order.ml
+  _start : unit -> unit -> int -> unit -> int -> int -> unit -> int -> int -> int
+  main : unit
+  $ ../bin/REPL.exe -fromfile manytests/typed/008ascription.ml
+  addi : ('_0 -> bool -> int) -> ('_0 -> bool) -> '_0 -> int
+  main : int
+  $ ../bin/REPL.exe -fromfile manytests/typed/009let_poly.ml
+  temp : (int, bool)
+  $ ../bin/REPL.exe -fromfile manytests/typed/010sukharev.ml
+  _1 : int -> int -> (int, '_1) -> bool
+  _2 : int
+  _3 : (int, string) option
+  _4 : int -> '_14
+  _6 : '_26 option -> '_26
+  int_of_option : int option -> int
+  _42 : int -> bool
+  id1 : '_40 -> '_40
+  id2 : '_41 -> '_41
+  Type checking failed: unification failed on string
+   and int
+  
+  $ ../bin/REPL.exe -fromfile manytests/typed/015tuples.ml
+  fix : (('_1 -> '_5) -> '_1 -> '_5) -> '_1 -> '_5
+  map : ('_9 -> '_11) -> ('_9, '_9) -> ('_11, '_11)
+  fixpoly : (('_21 -> '_25, '_21 -> '_25) -> '_21 -> '_25, ('_21 -> '_25, '_21 -> '_25) -> '_21 -> '_25) -> ('_21 -> '_25, '_21 -> '_25)
+  feven : ('_33, int -> int) -> int -> int
+  fodd : (int -> int, '_41) -> int -> int
+  tie : (int -> int, int -> int)
+  Type checking failed: Undefined variable 'modd'
+  : string
+  $ ../bin/REPL.exe -fromfile manytests/typed/016lists.ml
+  length : '_3 list -> int
+  length_tail : '_18 list -> int
+  map : ('_25 -> '_56) -> '_25 list -> '_56 list
+  append : '_67 list -> '_67 list -> '_67 list
+  concat : '_81 list list -> '_81 list
+  iter : ('_87 -> unit) -> '_87 list -> unit
+  cartesian : '_98 list -> '_105 list -> ('_98, '_105) list
+  main : int
diff --git a/FSharpActivePatterns/tests/manytests b/FSharpActivePatterns/tests/manytests
new file mode 120000
index 000000000..0bd48791d
--- /dev/null
+++ b/FSharpActivePatterns/tests/manytests
@@ -0,0 +1 @@
+../../manytests
\ No newline at end of file
diff --git a/Haskell/bin/REPL.ml b/Haskell/bin/REPL.ml
index 1642096e3..186e80f4a 100644
--- a/Haskell/bin/REPL.ml
+++ b/Haskell/bin/REPL.ml
@@ -2,8 +2,6 @@
 
 (** SPDX-License-Identifier: MIT *)
 
-open Haskell_lib.Parser
-
 type opts =
   { mutable dump_parsetree : bool
   ; mutable read_from_file : string
@@ -23,14 +21,30 @@ let () =
           Stdlib.exit 1))
       "Parse and print ast"
   in
-  let text =
+  let is_stdin =
     match opts.read_from_file with
-    | "" -> In_channel.(input_all stdin) |> String.trim
-    | _ -> In_channel.with_open_text opts.read_from_file In_channel.input_all
+    | "" -> true
+    | _ -> false
   in
-  if opts.dump_parsetree
-  then parse_and_print_line text
+  if not is_stdin
+  then
+    Haskell_lib.Pai.parse_and_infer
+      (String.split_on_char
+         '\n'
+         (In_channel.with_open_text opts.read_from_file In_channel.input_all))
+      opts.dump_parsetree
+      Haskell_lib.Inferencer.typeenv_print_int
   else (
-    let _ = parse_line text in
-    ())
+    let rec helper (env, st) =
+      (* TODO(Kakadu): Why curry? *)
+      let line =
+        try input_line stdin with
+        | End_of_file -> ":quit"
+      in
+      match line with
+      | ":quit" -> ()
+      | "" -> helper (env, st)
+      | _ -> helper (Haskell_lib.Pai.parse_and_infer_line line env st)
+    in
+    helper (Haskell_lib.Inferencer.typeenv_print_int, 0))
 ;;
diff --git a/Haskell/lib/ast.ml b/Haskell/lib/ast.ml
index 7fdff0fab..f74a6c847 100644
--- a/Haskell/lib/ast.ml
+++ b/Haskell/lib/ast.ml
@@ -18,6 +18,7 @@ type tp =
   | TUnit (** () *)
   | TInt (** Int *)
   | TBool (** Bool *)
+  | MaybeParam of tp (** e.g. [Maybe Int]*)
   | TreeParam of tp (** e.g. [{Int}] *)
   | ListParam of tp (** e.g. [[Int]] *)
   | TupleParams of tp * tp * tp_list (** e.g. [(Int, Bool)] *)
@@ -28,7 +29,7 @@ and functype = FuncT of tp * tp * tp_list (** e.g. [Int-> Bool -> (Int,Bool)] *)
 
 and tp_list =
   (tp list
-  [@gen QCheck.Gen.(list_size (return (Int.min 2 (n / 7))) (gen_tp_sized (n / 7)))])
+  [@gen QCheck.Gen.(list_size (return (Int.min 2 (n / 10))) (gen_tp_sized (n / 10)))])
 [@@deriving qcheck, show { with_path = false }]
 
 type binop =
diff --git a/Haskell/lib/dune b/Haskell/lib/dune
index 6adae5ce9..a8a88e981 100644
--- a/Haskell/lib/dune
+++ b/Haskell/lib/dune
@@ -3,7 +3,7 @@
  (public_name Haskell.Lib)
  (libraries angstrom qcheck-core.runner)
  (inline_tests)
- (modules Parser Ast Pprintast Qcheck)
+ (modules Parser Ast Pprintast Qcheck Typedtree Inferencer Pprint Pai)
  (preprocess
   (pps ppx_deriving.show ppx_inline_test ppx_expect ppx_deriving_qcheck))
  (instrumentation
diff --git a/Haskell/lib/inferencer.ml b/Haskell/lib/inferencer.ml
new file mode 100644
index 000000000..23c22e597
--- /dev/null
+++ b/Haskell/lib/inferencer.ml
@@ -0,0 +1,697 @@
+(** Copyright 2024, Kostya Oreshin and Nikita Shchutskii *)
+
+(** SPDX-License-Identifier: MIT *)
+
+open Typedtree
+open Ast
+
+module R : sig
+  type 'a t
+
+  val return : 'a -> 'a t
+  val fail : error -> 'a t
+
+  include Base.Monad.Infix with type 'a t := 'a t
+
+  module Syntax : sig
+    val ( let* ) : 'a t -> ('a -> 'b t) -> 'b t
+  end
+
+  module RList : sig
+    val fold_left : 'a list -> init:'b t -> f:('b -> 'a -> 'b t) -> 'b t
+  end
+
+  val fresh : int t
+
+  (** Running a transformer: getting the inner result value *)
+  val run : 'a t -> int -> int * ('a, error) Result.t
+end = struct
+  (* A compositon: State monad after Result monad *)
+  type 'a t = int -> int * ('a, error) Result.t
+
+  let ( >>= ) : 'a 'b. 'a t -> ('a -> 'b t) -> 'b t =
+    fun m f st ->
+    let lbindings, r = m st in
+    match r with
+    | Result.Error x -> lbindings, Error x
+    | Ok a -> f a lbindings
+  ;;
+
+  let fail e st = st, Base.Result.fail e
+  let return x lbindings = lbindings, Base.Result.return x
+  let bind x ~f = x >>= f
+
+  let ( >>| ) : 'a 'b. 'a t -> ('a -> 'b) -> 'b t =
+    fun x f st ->
+    match x st with
+    | st, Ok x -> st, Ok (f x)
+    | st, Result.Error e -> st, Result.Error e
+  ;;
+
+  module Syntax = struct
+    let ( let* ) x f = bind x ~f
+  end
+
+  module RList = struct
+    let fold_left xs ~init ~f =
+      Base.List.fold_left xs ~init ~f:(fun acc x ->
+        let open Syntax in
+        let* acc = acc in
+        f acc x)
+    ;;
+  end
+
+  let fresh : int t = fun lbindings -> lbindings + 1, Result.Ok lbindings
+  let run m = m
+end
+
+type fresh = int
+
+module Type = struct
+  type t = ty
+
+  let rec occurs_in v = function
+    | Ty_var b | Ty_ord b | Ty_enum b -> b = v
+    | Ty_arrow (l, r) -> occurs_in v l || occurs_in v r
+    | Ty_prim _ -> false
+    | Ty_list ty | Ty_tree ty | Ty_maybe ty -> occurs_in v ty
+    | Ty_tuple (ty1, ty2, ty_list) ->
+      List.exists (fun ty -> occurs_in v ty) (ty1 :: ty2 :: ty_list)
+  ;;
+
+  let free_vars =
+    let rec helper acc = function
+      | Ty_var b | Ty_ord b | Ty_enum b -> VarSet.add b acc
+      | Ty_arrow (l, r) -> helper (helper acc l) r
+      | Ty_prim _ -> acc
+      | Ty_list ty | Ty_tree ty | Ty_maybe ty -> helper acc ty
+      | Ty_tuple (ty1, ty2, ty_list) -> List.fold_left helper acc (ty1 :: ty2 :: ty_list)
+    in
+    helper VarSet.empty
+  ;;
+end
+
+module Subst : sig
+  type t
+
+  val empty : t
+  val singleton : fresh -> ty -> t R.t
+  val apply : t -> ty -> ty
+  val unify : ty -> ty -> t R.t
+
+  (** Compositon of substitutions *)
+  val compose : t -> t -> t R.t
+
+  val compose_all : t list -> t R.t
+  val remove : t -> fresh -> t
+end = struct
+  open R
+  open R.Syntax
+  open Base
+
+  (* an association list. In real world replace it by a finite map *)
+  type t = (fresh * ty) list
+
+  let empty = []
+  let mapping k v = if Type.occurs_in k v then fail `Occurs_check else return (k, v)
+
+  let singleton k v =
+    let* mapping = mapping k v in
+    return [ mapping ]
+  ;;
+
+  let find_exn k xs = List.Assoc.find_exn xs k ~equal:Int.equal
+  let remove xs k = List.Assoc.remove xs k ~equal:Int.equal
+
+  let apply s =
+    let rec helper = function
+      | Ty_var b as ty ->
+        (match find_exn b s with
+         | exception Not_found_s _ -> ty
+         | x -> x)
+      | Ty_arrow (l, r) -> Ty_arrow (helper l, helper r)
+      | Ty_list ty -> Ty_list (helper ty)
+      | Ty_tuple (ty1, ty2, ty_list) ->
+        Ty_tuple (helper ty1, helper ty2, List.map ty_list ~f:helper)
+      | Ty_tree ty -> Ty_tree (helper ty)
+      | Ty_maybe ty -> Ty_maybe (helper ty)
+      | Ty_ord ty ->
+        (match helper (Ty_var ty) with
+         | Ty_var ty' -> Ty_ord ty'
+         | t' -> t')
+      | Ty_enum ty ->
+        (match helper (Ty_var ty) with
+         | Ty_var ty' -> Ty_enum ty'
+         | t' -> t')
+      | other -> other
+    in
+    helper
+  ;;
+
+  let rec unify l r =
+    match l, r with
+    | Ty_prim l, Ty_prim r when String.equal l r -> return empty
+    | Ty_var a, Ty_var b when Int.equal a b -> return empty
+    | Ty_var b, t | t, Ty_var b -> singleton b t
+    | Ty_ord _, Ty_arrow _ | Ty_arrow _, Ty_ord _ -> fail (`Unification_failed (l, r))
+    | Ty_enum b, (Ty_prim _ as t) | (Ty_prim _ as t), Ty_enum b -> singleton b t
+    | Ty_ord b, ((Ty_list t | Ty_maybe t | Ty_tree t) as ty)
+    | ((Ty_list t | Ty_maybe t | Ty_tree t) as ty), Ty_ord b ->
+      let* s = fresh >>= fun f -> unify (Ty_ord f) t in
+      let ty2 = apply s ty in
+      singleton b ty2 >>= fun s2 -> compose s2 s
+    | Ty_ord b, (Ty_tuple (t1, t2, tt) as ty) | (Ty_tuple (t1, t2, tt) as ty), Ty_ord b ->
+      let* s =
+        RList.fold_left (t1 :: t2 :: tt) ~init:(return empty) ~f:(fun s t ->
+          let* s2 = fresh >>= fun f -> unify (Ty_ord f) t in
+          compose s2 s)
+      in
+      let ty2 = apply s ty in
+      singleton b ty2 >>= fun s2 -> compose s2 s
+    | Ty_ord b, t | t, Ty_ord b -> singleton b t
+    | Ty_arrow (l1, r1), Ty_arrow (l2, r2) ->
+      let* subs1 = unify l1 l2 in
+      let* subs2 = unify (apply subs1 r1) (apply subs1 r2) in
+      compose subs2 subs1
+    | Ty_list ty1, Ty_list ty2 -> unify ty1 ty2
+    | Ty_tuple (t1, t2, tt), Ty_tuple (t1', t2', tt')
+      when List.length tt = List.length tt' ->
+      RList.fold_left
+        (List.zip_exn (t1 :: t2 :: tt) (t1' :: t2' :: tt'))
+        ~init:(return empty)
+        ~f:(fun acc (t1, t2) ->
+          let* subs = unify (apply acc t1) (apply acc t2) in
+          compose subs acc)
+    | Ty_tree ty1, Ty_tree ty2 -> unify ty1 ty2
+    | Ty_maybe ty1, Ty_maybe ty2 -> unify ty1 ty2
+    | _ ->
+      (* TODO(Kakadu): You already have case like this above. Why split? *)
+      fail (`Unification_failed (l, r))
+
+  and extend s (k, v) =
+    let bind v f =
+      match v with
+      | Ty_var k' when k = k' -> return s
+      | _ -> f v
+    in
+    let ( let** ) = bind in
+    let** v = v in
+    match List.Assoc.find s ~equal:Int.equal k with
+    | None ->
+      let** v = apply s v in
+      let* s2 = singleton k v in
+      RList.fold_left s ~init:(return s2) ~f:(fun acc (k, v) ->
+        let** v = apply s2 v in
+        let* mapping = mapping k v in
+        return (mapping :: acc))
+    | Some v2 ->
+      let* s2 = unify v v2 in
+      compose s2 s
+
+  and compose s2 s1 = RList.fold_left s2 ~init:(return s1) ~f:extend
+
+  let compose_all ss = RList.fold_left ss ~init:(return empty) ~f:compose
+end
+
+module VarSet = struct
+  include VarSet
+
+  let fold_left_m f acc set =
+    fold
+      (fun x acc ->
+        let open R.Syntax in
+        let* acc = acc in
+        f acc x)
+      acc
+      set
+  ;;
+end
+
+module Scheme = struct
+  type t = scheme
+
+  let free_vars = function
+    | S (bs, t) -> VarSet.diff (Type.free_vars t) bs
+  ;;
+
+  let apply sub (S (names, ty)) =
+    let s2 = VarSet.fold (fun k s -> Subst.remove s k) names sub in
+    S (names, Subst.apply s2 ty)
+  ;;
+end
+
+module SMap = Map.Make (String)
+
+module TypeEnv = struct
+  open Base
+
+  type t = scheme SMap.t
+
+  let extend : t -> string * scheme -> t = fun e (name, scheme) -> SMap.add name scheme e
+  let empty = SMap.empty
+
+  let pp_some ppf names =
+    let open Stdlib.Format in
+    fprintf ppf "[ \n%a ]" (fun ppf env ->
+      SMap.iter
+        (fun name (S (bb, t)) ->
+          match List.find names ~f:(String.equal name) with
+          | Some _ -> fprintf ppf "%s: %a %a\n" name VarSet.pp bb Pprint.pp_ty t
+          | None -> ())
+        env)
+  ;;
+
+  let free_vars : t -> VarSet.t =
+    fun env ->
+    SMap.fold (fun _ s acc -> VarSet.union acc (Scheme.free_vars s)) env VarSet.empty
+  ;;
+
+  let apply s = SMap.map (Scheme.apply s)
+  let find_exn = SMap.find
+end
+
+type typeenv = TypeEnv.t
+
+let typeenv_print_int =
+  TypeEnv.extend
+    TypeEnv.empty
+    ("print_int", S (VarSet.empty, Ty_arrow (Ty_prim "Int", Ty_prim "()")))
+;;
+
+let typeenv_empty = TypeEnv.empty
+let pp_some_typeenv ppf (n, e) = TypeEnv.pp_some ppf n e
+
+open R
+open R.Syntax
+
+let unify = Subst.unify
+let fresh_var = fresh >>| fun n -> Ty_var n
+
+let instantiate : scheme -> ty R.t =
+  fun (S (bs, t)) ->
+  VarSet.fold_left_m
+    (fun typ name ->
+      let* f1 = fresh_var in
+      let* s = Subst.singleton name f1 in
+      return (Subst.apply s typ))
+    bs
+    (return t)
+;;
+
+let generalize : TypeEnv.t -> Type.t -> Scheme.t =
+  fun env ty ->
+  let free = VarSet.diff (Type.free_vars ty) (TypeEnv.free_vars env) in
+  S (free, ty)
+;;
+
+let lookup_env e xs =
+  match TypeEnv.find_exn e xs with
+  | exception Not_found -> fail (`No_variable e)
+  | scheme ->
+    let* ans = instantiate scheme in
+    return ans
+;;
+
+let built_in_sign op =
+  (function
+    | And | Or -> return (Ty_prim "Bool", Ty_prim "Bool", Ty_prim "Bool")
+    | Cons ->
+      let* t = fresh_var in
+      return (t, Ty_list t, Ty_list t)
+    | Plus | Minus | Divide | Mod | Multiply | Pow ->
+      return (Ty_prim "Int", Ty_prim "Int", Ty_prim "Int")
+    | _ -> fresh >>| fun t -> Ty_ord t, Ty_ord t, Ty_prim "Bool")
+    op
+  (* TODO(Kakadu): overly complicated. Maybe introduce helper function
+     `arrow3` and get rid of >>|? *)
+  >>| fun (t1, t2, t3) -> Ty_arrow (t1, Ty_arrow (t2, t3))
+;;
+
+let rec tp_to_ty = function
+  | TUnit -> Ty_prim "()"
+  | TBool -> Ty_prim "Bool"
+  | TInt -> Ty_prim "Int"
+  | MaybeParam tp -> Ty_maybe (tp_to_ty tp)
+  | TreeParam tp -> Ty_tree (tp_to_ty tp)
+  | ListParam tp -> Ty_list (tp_to_ty tp)
+  | TupleParams (t1, t2, tt) -> Ty_tuple (tp_to_ty t1, tp_to_ty t2, List.map tp_to_ty tt)
+  | FunctionType (FuncT (t1, t2, [])) -> Ty_arrow (tp_to_ty t1, tp_to_ty t2)
+  | FunctionType (FuncT (t1, t2, hd :: tl)) ->
+    Ty_arrow (tp_to_ty t1, tp_to_ty (FunctionType (FuncT (t2, hd, tl))))
+;;
+
+let rec bindings bb env =
+  let f (subst, env) = function
+    | FunDef (_, p, pp, bd, bb), tv0 ->
+      let* tt, inner_env = helper_pp (p :: pp) env in
+      let* s1, inner_env, _ = bindings bb inner_env in
+      let* s2, t1 =
+        (match bd with
+         | Guards (ep, eps) -> helper_guards (ep :: eps) inner_env
+         | OrdBody e -> infer e inner_env)
+        >>| fun (s, ty) -> s, ty_arr (List.map (Subst.apply s) (List.rev tt)) ty
+      in
+      let* s = Subst.compose_all [ s2; s1; subst ] in
+      let* s3 = unify (Subst.apply s tv0) t1 in
+      let* s = Subst.compose s3 s in
+      Subst.compose s subst >>| fun s -> s, env
+    | VarsDef (_, bd, bb), tv0 ->
+      let* s1, inner_env, _ = bindings bb env in
+      let* s2, t1 =
+        match bd with
+        | Guards (ep, eps) -> helper_guards (ep :: eps) env
+        | OrdBody e -> infer e inner_env
+      in
+      let* s = Subst.compose_all [ s2; s1; subst ] in
+      let* s_p = Subst.compose s subst in
+      let* s3 = unify (Subst.apply s_p tv0) t1 in
+      let* s = Subst.compose s3 s in
+      Subst.compose s subst >>| fun fs -> fs, env
+    | _ ->
+      (* TODO(Kakadu): All new constructors will go here, and type system will not help you *)
+      return (subst, env)
+  in
+  let* prep_bb, decls, delta_env, env, names = prep [] [] TypeEnv.empty env [] bb in
+  let init =
+    RList.fold_left
+      decls
+      ~init:(return (Subst.empty, env))
+      ~f:(fun (s, env) (name, t1) ->
+        let* _ = lookup_env name delta_env in
+        let* t2 = lookup_env name env in
+        let* s1 = unify t1 t2 in
+        Subst.compose s1 s >>| fun fs -> fs, TypeEnv.apply s1 env)
+  in
+  let* init_env = init >>| snd in
+  let* s, env = RList.fold_left prep_bb ~init ~f in
+  let* fenv =
+    RList.fold_left
+      names
+      ~init:(return (TypeEnv.apply s env))
+      ~f:(fun env' name ->
+        lookup_env name env' >>| fun t -> TypeEnv.extend env' (name, generalize init_env t))
+  in
+  return (s, fenv, names)
+
+and helper_guards eps env =
+  let* fresh = fresh_var in
+  RList.fold_left
+    eps
+    ~init:(return (Subst.empty, fresh))
+    ~f:(fun (s, t) (cond, e) ->
+      let* s2, t1 = infer cond env in
+      let* s3, t2 = infer e env in
+      let* s4 = unify t1 (Ty_prim "Bool") in
+      let* s5 = unify t t2 in
+      Subst.compose_all [ s5; s4; s3; s2; s ] >>| fun fs -> fs, Subst.apply s5 t)
+
+and prep prep_bb decls env1 env2 names = function
+  | [] -> return (prep_bb, decls, env1, env2, names)
+  | Decl (Ident name, t) :: tl ->
+    prep prep_bb ((name, tp_to_ty t) :: decls) env1 env2 names tl
+  | (FunDef (Ident name, _, _, _, _) as b) :: tl ->
+    let* tv = fresh_var in
+    let ext env = TypeEnv.extend env (name, S (VarSet.empty, tv)) in
+    prep ((b, tv) :: prep_bb) decls (ext env1) (ext env2) (name :: names) tl
+  | (VarsDef (p, _, _) as b) :: tl ->
+    let* _, env1, _ = helper_p p env1 [] in
+    let* t, env2, new_names = helper_p p env2 [] in
+    prep
+      ((b, t) :: prep_bb)
+      decls
+      env1
+      env2
+      (List.fold_left (fun nn n -> n :: nn) names new_names)
+      tl
+
+and helper_p (al, pat, type_annots) env names =
+  (match pat with
+   | PWildcard ->
+     let* fresh = fresh_var in
+     let* _, t = type_annots_hndl type_annots fresh in
+     return (t, env, names)
+   | PConst (NegativePInt _) ->
+     let* _, t = type_annots_hndl type_annots (Ty_prim "Int") in
+     return (t, env, names)
+   | PConst (OrdinaryPConst c) ->
+     let* _, t =
+       type_annots_hndl
+         type_annots
+         (Ty_prim
+            (match c with
+             | Int _ -> "Int"
+             | Bool _ -> "Bool"
+             | Unit -> "()"))
+     in
+     return (t, env, names)
+   | PIdentificator (Ident name) ->
+     let* fresh = fresh_var in
+     let* _, t = type_annots_hndl type_annots fresh in
+     return (t, TypeEnv.extend env (name, S (VarSet.empty, t)), name :: names)
+   | PMaybe Nothing ->
+     let* fresh = fresh_var in
+     let* _, t = type_annots_hndl type_annots (Ty_maybe fresh) in
+     return (t, env, names)
+   | PMaybe (Just pt) ->
+     let* t, env, names = helper_p pt env names in
+     let* s, t = type_annots_hndl type_annots (Ty_maybe t) in
+     return (t, TypeEnv.apply s env, names)
+   | PList (PCons (x, xs)) ->
+     let* t1, env1, names1 = helper_p x env names in
+     let* t2, env2, names2 = helper_p xs env1 names1 in
+     let* s = unify t2 (Ty_list t1) in
+     let t = Subst.apply s t2 in
+     let* s2, t' = type_annots_hndl type_annots t in
+     let* fs = Subst.compose s2 s in
+     return (t', TypeEnv.apply fs env2, names2)
+   | PTuple (p1, p2, pp) ->
+     let* t1, env1, names1 = helper_p p1 env names in
+     let* t2, env2, names2 = helper_p p2 env1 names1 in
+     let* tt, env, names =
+       RList.fold_left
+         pp
+         ~init:(return ([], env2, names2))
+         ~f:(fun (tt, env, names) p ->
+           let* t, env', names = helper_p p env names in
+           return (t :: tt, env', names))
+     in
+     let* s, t = type_annots_hndl type_annots (Ty_tuple (t1, t2, tt)) in
+     return (t, TypeEnv.apply s env, names)
+   | PList (PEnum pp) ->
+     let* fresh = fresh_var in
+     let* env, el_t, names =
+       RList.fold_left
+         pp
+         ~init:(return (env, fresh, names))
+         ~f:(fun (env, t, names) p ->
+           let* t', env', names = helper_p p env names in
+           let* s = unify t t' in
+           return (TypeEnv.apply s env', Subst.apply s t, names))
+     in
+     let* s, t = type_annots_hndl type_annots (Ty_list el_t) in
+     return (t, TypeEnv.apply s env, names)
+   | PTree PNul ->
+     let* fresh = fresh_var in
+     let* _, t = type_annots_hndl type_annots (Ty_tree fresh) in
+     return (t, env, names)
+   | PTree (PNode (d, l, r)) ->
+     let* t, env', names' = helper_p d env names >>| fun (t, e, n) -> Ty_tree t, e, n in
+     let* tl, env'', names'' = helper_p l env' names' in
+     let* tr, env''', names''' = helper_p r env'' names'' in
+     let* s1 = unify t tl in
+     let* s2 = unify (Subst.apply s1 t) tr in
+     let* s = Subst.compose s2 s1 in
+     let* _, t = type_annots_hndl type_annots (Subst.apply s t) in
+     return (t, TypeEnv.apply s env''', names'''))
+  >>| fun (t, env, names) ->
+  let env', names =
+    List.fold_left
+      (fun (env, names) (Ident name) ->
+        TypeEnv.extend env (name, S (VarSet.empty, t)), name :: names)
+      (env, names)
+      al
+  in
+  t, env', names
+
+and helper_pp pp env =
+  RList.fold_left
+    pp
+    ~init:(return ([], env))
+    ~f:(fun (tt, env) p ->
+      let* t, env', _ = helper_p p env [] in
+      return (t :: tt, env'))
+
+and infer (e, type_annots) env =
+  let helper_list ee t =
+    RList.fold_left
+      ee
+      ~init:(return (Subst.empty, t))
+      ~f:(fun (s, t) e ->
+        let* s2, t2 = infer e env in
+        let* s3 = unify t t2 in
+        Subst.compose_all [ s3; s2; s ] >>| fun s -> s, Subst.apply s3 t2)
+    >>| fun (s, t) -> s, Ty_list t
+  in
+  let ty_enum = fresh >>| fun b -> Ty_enum b in
+  let helper_e expr env =
+    match expr with
+    | Const const ->
+      (match const with
+       | Int _ -> return (Subst.empty, Ty_prim "Int")
+       | Bool _ -> return (Subst.empty, Ty_prim "Bool")
+       | Unit -> return (Subst.empty, Ty_prim "()"))
+    | Identificator (Ident i) -> lookup_env i env >>| fun t -> Subst.empty, t
+    | ENothing ->
+      let* fresh = fresh_var in
+      return (Subst.empty, Ty_maybe fresh)
+    | EJust ->
+      let* fresh = fresh_var in
+      return (Subst.empty, Ty_arrow (fresh, Ty_maybe fresh))
+    | BinTreeBld Nul ->
+      let* fresh = fresh_var in
+      return (Subst.empty, Ty_tree fresh)
+    | BinTreeBld (Node (d, l, r)) ->
+      let* s1, t = infer d env >>| fun (s, t) -> s, Ty_tree t in
+      let* s2, t2 = infer l env in
+      let* s3, t3 = infer r env in
+      let* s4 = unify t t2 in
+      let* s = Subst.compose_all [ s4; s3; s2; s1 ] in
+      let* s5 = unify (Subst.apply s t) t3 in
+      Subst.compose s5 s >>| fun fs -> fs, Subst.apply s5 t
+    | ListBld (OrdList (IncomprehensionlList ee)) -> fresh_var >>= helper_list ee
+    | ListBld (LazyList (e1, Some e2, Some e3)) -> ty_enum >>= helper_list [ e1; e2; e3 ]
+    | ListBld (LazyList (e1, Some e2, None) | LazyList (e1, None, Some e2)) ->
+      ty_enum >>= helper_list [ e1; e2 ]
+    | ListBld (LazyList (e1, None, None)) -> ty_enum >>= helper_list [ e1 ]
+    | FunctionApply (f, a, aa) ->
+      (match aa with
+       | [] ->
+         let* s1, t1 = infer f env in
+         let* s2, t2 = infer a (TypeEnv.apply s1 env) in
+         let* tv = fresh_var in
+         let* s3 = unify (Subst.apply s2 t1) (Ty_arrow (t2, tv)) in
+         let trez = Subst.apply s3 tv in
+         let* final_subst = Subst.compose_all [ s3; s2; s1 ] in
+         return (final_subst, trez)
+       | hd :: tl ->
+         infer (FunctionApply ((FunctionApply (f, a, []), []), hd, tl), []) env)
+    | IfThenEsle (c, th, el) ->
+      let* s1, t1 = infer c env in
+      let* s2, t2 = infer th env in
+      let* s3, t3 = infer el env in
+      let* s4 = unify t1 (Ty_prim "Bool") in
+      let* s5 = unify t2 t3 in
+      let* final_subst = Subst.compose_all [ s5; s4; s3; s2; s1 ] in
+      return (final_subst, Subst.apply s5 t2)
+    | Neg e ->
+      let* s, t = infer e env in
+      let* s1 = unify t (Ty_prim "Int") in
+      let* s2 = Subst.compose s1 s in
+      return (s2, Subst.apply s1 t)
+    | TupleBld (e1, e2, ee) ->
+      let* s1, t1 = infer e1 env in
+      let* s2, t2 = infer e2 env in
+      let* ss, tt =
+        RList.fold_left
+          ee
+          ~init:(return ([], []))
+          ~f:(fun (ss, tt) e -> infer e env >>| fun (s, t) -> s :: ss, t :: tt)
+      in
+      let* final_subst = Subst.compose_all (s1 :: s2 :: ss) in
+      return (final_subst, Ty_tuple (t1, t2, tt))
+    | Binop (e1, op, e2) ->
+      let* sign = built_in_sign op in
+      let* s1, t1 = infer e1 env in
+      let* s2, t2 = infer e2 env in
+      let* tv = fresh_var in
+      let* s3 = unify (Ty_arrow (t1, Ty_arrow (t2, tv))) sign in
+      let* final_subst = Subst.compose_all [ s1; s2; s3 ] in
+      return (final_subst, Subst.apply s3 tv)
+    | Lambda (p, pp, e) ->
+      let* tt, env' = helper_pp (p :: pp) env in
+      let* s, ty = infer e env' in
+      let trez = ty_arr (List.map (Subst.apply s) (List.rev tt)) (Subst.apply s ty) in
+      return (s, trez)
+    | InnerBindings (b, bb, e) ->
+      let* s, env, _ = bindings (b :: bb) env in
+      let* s2, t2 = infer e env in
+      Subst.compose s2 s >>| fun fs -> fs, t2
+    | Case (e, pb, pbs) ->
+      let* fresh = fresh_var in
+      let* s1, t1 =
+        RList.fold_left
+          (pb :: pbs)
+          ~init:(return (Subst.empty, fresh))
+          ~f:(fun (s, t) (p, b) ->
+            let* s1, t1 =
+              match b with
+              | OrdBody e -> infer (Lambda (p, [], e), []) env
+              | Guards (ep, eps) ->
+                let* t, env', _ = helper_p p env [] in
+                let* s, ty = helper_guards (ep :: eps) env' in
+                let trez = Ty_arrow (Subst.apply s t, ty) in
+                return (s, trez)
+            in
+            let* s2 = unify t1 t in
+            Subst.compose_all [ s2; s1; s ] >>| fun fs -> fs, Subst.apply s2 t)
+      in
+      let* s2, t2 = infer e (TypeEnv.apply s1 env) in
+      let* tv = fresh_var in
+      let* s3 = unify (Subst.apply s2 t1) (Ty_arrow (t2, tv)) in
+      let trez = Subst.apply s3 tv in
+      let* final_subst = Subst.compose_all [ s3; s2; s1 ] in
+      return (final_subst, trez)
+    | ListBld (OrdList (ComprehensionList (e, c, cc))) ->
+      let* s1, env' =
+        RList.fold_left
+          (c :: cc)
+          ~init:(return (Subst.empty, env))
+          ~f:(fun (s, env) cmp ->
+            let* s1, env =
+              match cmp with
+              | Condition x ->
+                let* s1, t1 = infer x env in
+                let* s2 = unify t1 (Ty_prim "Bool") in
+                let* final_subst = Subst.compose s2 s1 in
+                return (final_subst, env)
+              | Generator (p, e) ->
+                let* s2, t2 = infer e env in
+                let* t3, env', _ = helper_p p env [] in
+                let* s3 = unify t2 (Ty_list t3) in
+                let* s = Subst.compose s3 s2 in
+                return (s, env')
+            in
+            Subst.compose s1 s >>| fun fs -> fs, env)
+      in
+      let* s2, t2 = infer e (TypeEnv.apply s1 env') in
+      let* final_subst = Subst.compose s2 s1 in
+      return (final_subst, Ty_list t2)
+  in
+  match type_annots with
+  | [] -> helper_e e env
+  | type_annots ->
+    let* fresh = fresh_var in
+    let* _, t0 = type_annots_hndl type_annots fresh in
+    helper_e e env
+    >>= fun (s, t) ->
+    let* s' = unify t t0 in
+    Subst.compose s' s >>| fun fs -> fs, Subst.apply s' t
+
+and type_annots_hndl type_annots init =
+  RList.fold_left
+    type_annots
+    ~init:(return (Subst.empty, init))
+    ~f:(fun (s, t) tp ->
+      unify t (tp_to_ty tp)
+      >>= fun s' -> Subst.compose s' s >>| fun fs -> fs, Subst.apply s' t)
+
+and ty_arr tt t =
+  match tt with
+  | [] -> t
+  | hd :: tl -> Ty_arrow (hd, ty_arr tl t)
+;;
+
+let w p env st =
+  let st, res = run (bindings p env) st in
+  st, Result.map (fun (_, env, names) -> env, names) res
+;;
diff --git a/Haskell/lib/inferencer.mli b/Haskell/lib/inferencer.mli
new file mode 100644
index 000000000..532a6de57
--- /dev/null
+++ b/Haskell/lib/inferencer.mli
@@ -0,0 +1,18 @@
+(** Copyright 2024, Kostya Oreshin and Nikita Shchutskii *)
+
+(** SPDX-License-Identifier: MIT *)
+
+open Ast
+open Typedtree
+
+type typeenv
+
+val typeenv_print_int : typeenv
+val typeenv_empty : typeenv
+val pp_some_typeenv : Format.formatter -> string list * typeenv -> unit
+
+val w
+  :  binding_list
+  -> typeenv
+  -> binder
+  -> binder * (typeenv * string list, error) Result.t
diff --git a/Haskell/lib/pai.ml b/Haskell/lib/pai.ml
new file mode 100644
index 000000000..dadaf7dd5
--- /dev/null
+++ b/Haskell/lib/pai.ml
@@ -0,0 +1,40 @@
+(** Copyright 2024, Kostya Oreshin and Nikita Shchutskii *)
+
+(** SPDX-License-Identifier: MIT *)
+
+let parse_and_infer =
+  let rec helper st names text print env =
+    match text with
+    | [] ->
+      if env != Inferencer.typeenv_empty && env != Inferencer.typeenv_print_int
+      then Format.printf "%a\n%!" Inferencer.pp_some_typeenv (names, env)
+    | "" :: rest -> helper st names rest print env
+    | line :: rest ->
+      if print then Parser.parse_and_print_line line;
+      (match Parser.parse_line line with
+       | Result.Ok list ->
+         (match Inferencer.w list env st with
+          | st, Result.Ok (env, nn) ->
+            helper st (List.fold_left (fun nn n -> n :: nn) names nn) rest print env
+          | st, Result.Error err ->
+            Format.printf "%a\n%!" Pprint.pp_error err;
+            helper st names rest print env)
+       | Result.Error error -> Format.printf "%s\n%!" error)
+  in
+  helper 0 []
+;;
+
+let parse_and_infer_line line env st =
+  match Parser.parse_line line with
+  | Result.Ok list ->
+    (match Inferencer.w list env st with
+     | st, Result.Ok (env, names) ->
+       Format.printf "%a\n%!" Inferencer.pp_some_typeenv (names, env);
+       env, st
+     | st, Result.Error err ->
+       Format.printf "%a\n%!" Pprint.pp_error err;
+       env, st)
+  | Result.Error error ->
+    Format.printf "%s\n%!" error;
+    env, st
+;;
diff --git a/Haskell/lib/pai.mli b/Haskell/lib/pai.mli
new file mode 100644
index 000000000..68e0f5788
--- /dev/null
+++ b/Haskell/lib/pai.mli
@@ -0,0 +1,6 @@
+(** Copyright 2024, Kostya Oreshin and Nikita Shchutskii *)
+
+(** SPDX-License-Identifier: MIT *)
+
+val parse_and_infer : string list -> bool -> Inferencer.typeenv -> unit
+val parse_and_infer_line : string -> Inferencer.typeenv -> int -> Inferencer.typeenv * int
diff --git a/Haskell/lib/parser.ml b/Haskell/lib/parser.ml
index bab0a6c19..995a0a1d6 100644
--- a/Haskell/lib/parser.ml
+++ b/Haskell/lib/parser.ml
@@ -169,14 +169,20 @@ let func_tp_tail hd ord_tp =
 
 let ord_tp tp =
   let w = word ~point_allowed:Allow_point in
-  choice
-    [ string "()" *> return TUnit
-    ; w "Int" *> return TInt
-    ; w "Bool" *> return TBool
-    ; (sq_brackets tp >>| fun x -> ListParam x)
-    ; (braces tp >>| fun x -> TreeParam x)
-    ; tuple_or_parensed_item tp (fun fs sn tl -> return (TupleParams (fs, sn, tl))) return
-    ]
+  let ord_tp =
+    choice
+      [ string "()" *> return TUnit
+      ; w "Int" *> return TInt
+      ; w "Bool" *> return TBool
+      ; (sq_brackets tp >>| fun x -> ListParam x)
+      ; (braces tp >>| fun x -> TreeParam x)
+      ; tuple_or_parensed_item
+          tp
+          (fun fs sn tl -> return (TupleParams (fs, sn, tl)))
+          return
+      ]
+  in
+  ord_tp <|> (w "Maybe" *> ws *> ord_tp >>| fun t -> MaybeParam t)
 ;;
 
 let tp =
@@ -189,6 +195,11 @@ let%expect_test "tp_list_of_func" =
   [%expect {| (ListParam (FunctionType (FuncT (TInt, TInt, [])))) |}]
 ;;
 
+let%expect_test "tp_maybe" =
+  prs_and_prnt_ln tp show_tp "Maybe Int ";
+  [%expect {| (MaybeParam TInt) |}]
+;;
+
 let%expect_test "tp_tree_of_func" =
   prs_and_prnt_ln tp show_tp "{Bool -> ()} ";
   [%expect {| (TreeParam (FunctionType (FuncT (TBool, TUnit, [])))) |}]
@@ -706,10 +717,43 @@ let tuple_or_parensed_item_e e =
     return
 ;;
 
+let infix_binop =
+  let binop_lambda op =
+    return
+      (Lambda
+         ( ([], PIdentificator (Ident "x"), [])
+         , [ [], PIdentificator (Ident "y"), [] ]
+         , ( Binop ((Identificator (Ident "x"), []), op, (Identificator (Ident "y"), []))
+           , [] ) ))
+  in
+  choice
+    [ parens
+        (choice
+           [ oper "||" *> binop_lambda Or
+           ; oper "&&" *> binop_lambda And
+           ; oper "==" *> binop_lambda Equality
+           ; oper "/=" *> binop_lambda Inequality
+           ; oper ">=" *> binop_lambda EqualityOrGreater
+           ; oper "<=" *> binop_lambda EqualityOrLess
+           ; oper ">" *> binop_lambda Greater
+           ; oper "<" *> binop_lambda Less
+           ; oper ":" *> binop_lambda Cons
+           ; oper "-" *> binop_lambda Minus
+           ; oper "+" *> binop_lambda Plus
+           ; oper "*" *> binop_lambda Multiply
+           ; oper "^" *> binop_lambda Multiply
+           ])
+    ; word "div" *> binop_lambda Divide
+    ; word "mod" *> binop_lambda Mod
+    ]
+  >>| fun e -> e, []
+;;
+
 let other_expr e fa =
   let e' = e >>= ex_tp in
   choice
     [ const_e
+    ; infix_binop
     ; ident_e
     ; nothing (return (ENothing, []))
     ; just (return (EJust, []))
@@ -733,6 +777,7 @@ let function_application ex e =
       (ws
        *> choice
             [ const_e
+            ; infix_binop
             ; ident_e
             ; just (return (EJust, []))
             ; nothing (return (ENothing, []))
@@ -757,10 +802,17 @@ let expr = function
   | Allow_t -> fix e >>= ex_tp
 ;;
 
-let%expect_test "expr_const" =
-  prs_and_prnt_ln (expr Allow_t) show_expr "123456789012345678901234567890";
-  [%expect {|
-      error: : no more choices |}]
+let%expect_test "infix_binop" =
+  prs_and_prnt_ln (expr Allow_t) show_expr "(*)";
+  [%expect
+    {|
+      ((Lambda (([], (PIdentificator (Ident "x")), []),
+          [([], (PIdentificator (Ident "y")), [])],
+          ((Binop (((Identificator (Ident "x")), []), Multiply,
+              ((Identificator (Ident "y")), []))),
+           [])
+          )),
+       []) |}]
 ;;
 
 let%expect_test "expr_prio" =
diff --git a/Haskell/lib/pprint.ml b/Haskell/lib/pprint.ml
new file mode 100644
index 000000000..dbe14443f
--- /dev/null
+++ b/Haskell/lib/pprint.ml
@@ -0,0 +1,40 @@
+(** Copyright 2024, Kostya Oreshin and Nikita Shchutskii *)
+
+(** SPDX-License-Identifier: MIT *)
+
+open Format
+open Typedtree
+
+let pp_ty =
+  let rec helper fmt = function
+    | Ty_maybe ty -> fprintf fmt "Maybe %a" helper ty
+    | Ty_prim s -> pp_print_string fmt s
+    | Ty_var b -> fprintf fmt "t%d" b
+    | Ty_arrow (ty1, ty2) ->
+      (match ty1 with
+       | Ty_arrow (_, _) -> fprintf fmt "(%a) -> %a" helper ty1 helper ty2
+       | _ -> fprintf fmt "%a -> %a" helper ty1 helper ty2)
+    | Ty_list ty -> fprintf fmt "[%a]" helper ty
+    | Ty_tuple (ty1, ty2, ty_list) ->
+      fprintf
+        fmt
+        "(%a, %a%a)"
+        helper
+        ty1
+        helper
+        ty2
+        (pp_print_list (fun fmt ty -> fprintf fmt ", %a" helper ty))
+        ty_list
+    | Ty_tree ty -> fprintf fmt "{%a}" helper ty
+    | Ty_ord ty -> fprintf fmt "Ord t%d" ty
+    | Ty_enum ty -> fprintf fmt "Enum t%d" ty
+  in
+  helper
+;;
+
+let pp_error ppf : error -> _ = function
+  | `Occurs_check -> Format.fprintf ppf "Occurs check failed"
+  | `No_variable s -> Format.fprintf ppf "Undefined variable '%s'" s
+  | `Unification_failed (l, r) ->
+    Format.fprintf ppf "unification failed on %a and %a" pp_ty l pp_ty r
+;;
diff --git a/Haskell/lib/pprint.mli b/Haskell/lib/pprint.mli
new file mode 100644
index 000000000..b67c25ec1
--- /dev/null
+++ b/Haskell/lib/pprint.mli
@@ -0,0 +1,8 @@
+(** Copyright 2024, Kostya Oreshin and Nikita Shchutskii *)
+
+(** SPDX-License-Identifier: MIT *)
+
+open Typedtree
+
+val pp_ty : Format.formatter -> ty -> unit
+val pp_error : Format.formatter -> error -> unit
diff --git a/Haskell/lib/pprintast.ml b/Haskell/lib/pprintast.ml
index b56874092..9223394bb 100644
--- a/Haskell/lib/pprintast.ml
+++ b/Haskell/lib/pprintast.ml
@@ -37,6 +37,14 @@ and pp_tp fmt = function
   | TUnit -> fprintf fmt "()"
   | TInt -> fprintf fmt "Int"
   | TBool -> fprintf fmt "Bool"
+  | MaybeParam tp ->
+    fprintf
+      fmt
+      (match tp with
+       | MaybeParam _ | FunctionType _ -> "Maybe (%a)"
+       | _ -> "Maybe %a")
+      pp_tp
+      tp
   | TreeParam tp -> fprintf fmt "{%a}" pp_tp tp
   | ListParam tp -> fprintf fmt "[%a]" pp_tp tp
   | TupleParams (first, second, list) ->
diff --git a/Haskell/lib/qcheck.ml b/Haskell/lib/qcheck.ml
index 2ed40b10e..7083cdecc 100644
--- a/Haskell/lib/qcheck.ml
+++ b/Haskell/lib/qcheck.ml
@@ -12,6 +12,7 @@ let rec shrink_tp =
   | TUnit | TInt | TBool -> empty
   | TreeParam tp -> shrink_tp tp >|= fun a' -> TreeParam a'
   | ListParam tp -> shrink_tp tp >|= fun a' -> ListParam a'
+  | MaybeParam tp -> shrink_tp tp >|= fun a' -> MaybeParam a'
   | TupleParams (first, second, rest) ->
     of_list [ first; second ]
     <+> (shrink_tp first >|= fun a' -> TupleParams (a', second, rest))
diff --git a/Haskell/lib/typedtree.ml b/Haskell/lib/typedtree.ml
new file mode 100644
index 000000000..60b53d5d5
--- /dev/null
+++ b/Haskell/lib/typedtree.ml
@@ -0,0 +1,34 @@
+(** Copyright 2024, Kostya Oreshin and Nikita Shchutskii *)
+
+(** SPDX-License-Identifier: MIT *)
+
+type binder = int [@@deriving show { with_path = false }]
+
+module VarSet = struct
+  include Stdlib.Set.Make (Int)
+
+  let pp ppf s = iter (Format.fprintf ppf "t%d. ") s
+end
+
+type binder_set = VarSet.t [@@deriving show { with_path = false }]
+
+type ty =
+  | Ty_prim of string
+  | Ty_maybe of ty
+  | Ty_var of binder
+  | Ty_arrow of ty * ty
+  | Ty_list of ty
+  | Ty_tuple of ty * ty * ty list
+  | Ty_tree of ty
+  | Ty_ord of binder
+  | Ty_enum of binder
+[@@deriving show { with_path = false }]
+
+type scheme = S of binder_set * ty [@@deriving show { with_path = false }]
+
+type error =
+  [ `Occurs_check
+  | `No_variable of string
+  | (* TODO(Kakadu): Unbound variable *)
+    `Unification_failed of ty * ty
+  ]
diff --git a/Haskell/lib/typedtree.mli b/Haskell/lib/typedtree.mli
new file mode 100644
index 000000000..e5538ade0
--- /dev/null
+++ b/Haskell/lib/typedtree.mli
@@ -0,0 +1,39 @@
+(** Copyright 2024, Kostya Oreshin and Nikita Shchutskii *)
+
+(** SPDX-License-Identifier: MIT *)
+
+type binder = int [@@deriving show { with_path = false }]
+
+module VarSet : sig
+  type t
+
+  val add : int -> t -> t
+  val empty : t
+  val fold : (int -> 'a -> 'a) -> t -> 'a -> 'a
+  val diff : t -> t -> t
+  val union : t -> t -> t
+  val pp : Format.formatter -> t -> unit
+end
+
+type binder_set = VarSet.t [@@deriving show { with_path = false }]
+
+(** hierarchy: https://www.haskell.org/onlinereport/haskell2010/haskellch6.html#x13-1270011 *)
+type ty =
+  | Ty_prim of string
+  | Ty_maybe of ty
+  | Ty_var of binder
+  | Ty_arrow of ty * ty
+  | Ty_list of ty
+  | Ty_tuple of ty * ty * ty list
+  | Ty_tree of ty
+  | Ty_ord of binder (** i.e. [Ord a]; e.g. [(>) :: Ord a -> Ord a -> Bool] *)
+  | Ty_enum of binder (** i.e. [Enum a]; e.g. [ (\x -> [x..]) :: Enum a -> [Enum a]] *)
+[@@deriving show { with_path = false }]
+
+type scheme = S of binder_set * ty [@@deriving show { with_path = false }]
+
+type error =
+  [ `Occurs_check
+  | `No_variable of string
+  | `Unification_failed of ty * ty
+  ]
diff --git a/Haskell/tests/dune b/Haskell/tests/dune
index 60393c879..a4fcf042b 100644
--- a/Haskell/tests/dune
+++ b/Haskell/tests/dune
@@ -1,3 +1,25 @@
 (cram
- (applies_to qcheck)
- (deps ../lib/run_binding.exe))
+ (applies_to repl)
+ (deps
+  ../lib/run_binding.exe
+  ../bin/REPL.exe
+  manytests/do_not_type/001.hs
+  manytests/do_not_type/002if.hs
+  manytests/do_not_type/003occurs.hs
+  manytests/do_not_type/004_let_poly.hs
+  manytests/do_not_type/099.hs
+  manytests/typed/001fac.hs
+  manytests/typed/001fac.hs
+  manytests/typed/002fac.hs
+  manytests/typed/003fib.hs
+  manytests/typed/004manyargs.hs
+  manytests/typed/005fix.hs
+  manytests/typed/006partial.hs
+  manytests/typed/006partial2.hs
+  manytests/typed/006partial3.hs
+  manytests/typed/007order.hs
+  manytests/typed/008ascription.hs
+  manytests/typed/009let_poly.hs
+  manytests/typed/010sukharev.hs
+  manytests/typed/015tuples.hs
+  manytests/typed/016lists.hs))
diff --git a/Haskell/tests/manytests/do_not_type/001.hs b/Haskell/tests/manytests/do_not_type/001.hs
new file mode 100644
index 000000000..081362e28
--- /dev/null
+++ b/Haskell/tests/manytests/do_not_type/001.hs
@@ -0,0 +1 @@
+recfac n = if n<=1 then 1 else n * fac (n-1)
diff --git a/Haskell/tests/manytests/do_not_type/002if.hs b/Haskell/tests/manytests/do_not_type/002if.hs
new file mode 100644
index 000000000..8bde7f52b
--- /dev/null
+++ b/Haskell/tests/manytests/do_not_type/002if.hs
@@ -0,0 +1 @@
+main = if True then 1 else False
\ No newline at end of file
diff --git a/Haskell/tests/manytests/do_not_type/003occurs.hs b/Haskell/tests/manytests/do_not_type/003occurs.hs
new file mode 100644
index 000000000..080bf93c1
--- /dev/null
+++ b/Haskell/tests/manytests/do_not_type/003occurs.hs
@@ -0,0 +1 @@
+fix f = (\x -> f (\f -> x x f))  (\x -> f (\f -> x x f))
diff --git a/Haskell/tests/manytests/do_not_type/004_let_poly.hs b/Haskell/tests/manytests/do_not_type/004_let_poly.hs
new file mode 100644
index 000000000..ad1602238
--- /dev/null
+++ b/Haskell/tests/manytests/do_not_type/004_let_poly.hs
@@ -0,0 +1 @@
+temp = (\f -> (f 1, f True)) (\x -> x)
\ No newline at end of file
diff --git a/Haskell/tests/manytests/do_not_type/099.hs b/Haskell/tests/manytests/do_not_type/099.hs
new file mode 100644
index 000000000..3aa086217
--- /dev/null
+++ b/Haskell/tests/manytests/do_not_type/099.hs
@@ -0,0 +1,3 @@
+Just x = Just 1
+Just a = (<)
+() = (\x -> x)
\ No newline at end of file
diff --git a/Haskell/tests/manytests/typed/001fac.hs b/Haskell/tests/manytests/typed/001fac.hs
new file mode 100644
index 000000000..ddf2d9a5f
--- /dev/null
+++ b/Haskell/tests/manytests/typed/001fac.hs
@@ -0,0 +1,3 @@
+fac n = if n<=1 then 1 else n * fac (n-1)
+
+main = let () = print_int (fac 4) in 0
\ No newline at end of file
diff --git a/Haskell/tests/manytests/typed/002fac.hs b/Haskell/tests/manytests/typed/002fac.hs
new file mode 100644
index 000000000..332562db2
--- /dev/null
+++ b/Haskell/tests/manytests/typed/002fac.hs
@@ -0,0 +1,3 @@
+fac_cps n k = if n==1 then k 1 else fac_cps (n-1) (\p -> k (p*n))
+
+main = let () = print_int (fac_cps 4 (\ print_int -> print_int)) in 0
\ No newline at end of file
diff --git a/Haskell/tests/manytests/typed/003fib.hs b/Haskell/tests/manytests/typed/003fib.hs
new file mode 100644
index 000000000..e86d90390
--- /dev/null
+++ b/Haskell/tests/manytests/typed/003fib.hs
@@ -0,0 +1,5 @@
+fib_acc a b n = if n==1 then b else let n1 = n-1 in let ab = a+b in fib_acc b ab n1
+
+fib n = if n<2 then n else fib (n - 1) + fib (n - 2) 
+
+main = let () = print_int (fib_acc 0 1 4) in let () = print_int (fib 4) in 0
\ No newline at end of file
diff --git a/Haskell/tests/manytests/typed/004manyargs.hs b/Haskell/tests/manytests/typed/004manyargs.hs
new file mode 100644
index 000000000..e9010816f
--- /dev/null
+++ b/Haskell/tests/manytests/typed/004manyargs.hs
@@ -0,0 +1,7 @@
+wrap f = if 1 == 1 then f else f
+
+test3 a b c = let x = print_int a in let y = print_int b in let z = print_int c in 0
+
+test10 a b c d e f g h i j = a + b + c + d + e + f + g + h + i + j
+
+main = let rez = (wrap test10 1 10 100 1000 10000 100000 1000000 10000000 100000000 1000000000) in let () = print_int rez in let temp2 = wrap test3 1 10 100 in 0
\ No newline at end of file
diff --git a/Haskell/tests/manytests/typed/005fix.hs b/Haskell/tests/manytests/typed/005fix.hs
new file mode 100644
index 000000000..5ff4718ba
--- /dev/null
+++ b/Haskell/tests/manytests/typed/005fix.hs
@@ -0,0 +1,5 @@
+fix f x = f (fix f) x
+
+fac self n = if n<=1 then 1 else n * self (n-1)
+
+main = let () = print_int (fix fac 6) in 0
diff --git a/Haskell/tests/manytests/typed/006partial.hs b/Haskell/tests/manytests/typed/006partial.hs
new file mode 100644
index 000000000..1e6db7b5d
--- /dev/null
+++ b/Haskell/tests/manytests/typed/006partial.hs
@@ -0,0 +1,5 @@
+foo b = if b then (\foo -> foo+2) else (\foo -> foo*10)
+
+foo2 x = foo True (foo False (foo True (foo False x)))
+
+main = let () = print_int (foo2 11) in 0
diff --git a/Haskell/tests/manytests/typed/006partial2.hs b/Haskell/tests/manytests/typed/006partial2.hs
new file mode 100644
index 000000000..bc88d26ec
--- /dev/null
+++ b/Haskell/tests/manytests/typed/006partial2.hs
@@ -0,0 +1,3 @@
+foo a b c = let () = print_int a in let () = print_int b in let () = print_int c in a + b * c
+
+main = let foo2 = foo 1 in let foo = foo2 2 in let foo2 = foo 3 in let () = print_int foo2 in 0
diff --git a/Haskell/tests/manytests/typed/006partial3.hs b/Haskell/tests/manytests/typed/006partial3.hs
new file mode 100644
index 000000000..7960c0566
--- /dev/null
+++ b/Haskell/tests/manytests/typed/006partial3.hs
@@ -0,0 +1,3 @@
+foo a = let () = print_int a in \b -> let () = print_int b in \c -> print_int c
+
+main = let () = foo 4 8 9 in 0
diff --git a/Haskell/tests/manytests/typed/007order.hs b/Haskell/tests/manytests/typed/007order.hs
new file mode 100644
index 000000000..cda0e572d
--- /dev/null
+++ b/Haskell/tests/manytests/typed/007order.hs
@@ -0,0 +1,4 @@
+_start () () a () b _c () d __ = let () = print_int (a+b) in let () = print_int __ in a*b `div` _c + d
+
+
+main = print_int (_start (print_int 1) (print_int 2) 3 (print_int 4) 100 1000 (print_int (-1)) 10000 (-555555))
diff --git a/Haskell/tests/manytests/typed/008ascription.hs b/Haskell/tests/manytests/typed/008ascription.hs
new file mode 100644
index 000000000..926902b4f
--- /dev/null
+++ b/Haskell/tests/manytests/typed/008ascription.hs
@@ -0,0 +1,3 @@
+addi = \f g x -> (f x (g x:: Bool) :: Int)
+
+main = let () = print_int (addi (\x b -> if b then x+1 else x*2) (\ _start -> _start `div` 2 == 0) 4) in 0
diff --git a/Haskell/tests/manytests/typed/009let_poly.hs b/Haskell/tests/manytests/typed/009let_poly.hs
new file mode 100644
index 000000000..df0bbd4e9
--- /dev/null
+++ b/Haskell/tests/manytests/typed/009let_poly.hs
@@ -0,0 +1 @@
+temp = let f = \x -> x in (f 1, f True)
diff --git a/Haskell/tests/manytests/typed/010sukharev.hs b/Haskell/tests/manytests/typed/010sukharev.hs
new file mode 100644
index 000000000..c8736a6e0
--- /dev/null
+++ b/Haskell/tests/manytests/typed/010sukharev.hs
@@ -0,0 +1,14 @@
+_1 = \x y (a, _) -> (x + y - a) == 1
+_2 = let (x, Just f) = (1, Just ( ( + ) 4 )) in f x
+
+_3 = Just (1, True)
+
+_4 = let (a, _, _) = (1, 2, 3) in a
+
+int_of_option (Just x) = x 
+int_of_option Nothing = 0
+
+_5 = let f x = f 5 in f
+
+_42  42 = True
+_42 _  = False
diff --git a/Haskell/tests/manytests/typed/015tuples.hs b/Haskell/tests/manytests/typed/015tuples.hs
new file mode 100644
index 000000000..8acb46e9c
--- /dev/null
+++ b/Haskell/tests/manytests/typed/015tuples.hs
@@ -0,0 +1,8 @@
+fix f x = f (fix f) x
+map f p = let (a,b) = p in (f a, f b)
+fixpoly l = fix (\self l -> map (\li x -> li (self l) x) l) l
+feven p n = let (e, o) = p in if n == 0 then 1 else o (n - 1)
+fodd p n = let (e, o) = p in if n == 0 then 0 else e (n - 1)
+tie = fixpoly (feven, fodd)
+meven n = if n == 0 then 1 else modd (n - 1); modd n = if n == 0 then 1 else meven (n - 1)
+main = let () = print_int (modd 1) in let () = print_int (meven 2) in let (even,odd) = tie in let () = print_int (odd 3) in let () = print_int (even 4) in 0
diff --git a/Haskell/tests/manytests/typed/016lists.hs b/Haskell/tests/manytests/typed/016lists.hs
new file mode 100644
index 000000000..e346538ba
--- /dev/null
+++ b/Haskell/tests/manytests/typed/016lists.hs
@@ -0,0 +1,15 @@
+length xs = case xs of [] -> 0; h:tl -> 1 + length tl
+
+length_tail = let helper acc xs = case xs of [] -> acc; h:tl -> helper (acc + 1) tl in helper 0
+
+map f xs = case xs of [] -> []; a:[] -> [f a]; a:b:[] -> [f a, f b]; a:b:c:[] -> [f a, f b, f c]; a:b:c:d:tl -> f a : f b : f c : f d : map f tl
+
+append xs ys = case xs of [] -> ys; x:xs -> x:(append xs ys)
+
+concat = let helper xs = case xs of [] -> []; h:tl -> append h (helper tl) in helper
+
+iter f xs = case xs of [] -> (); h:tl -> let () = f h in iter f tl
+
+cartesian xs ys = case xs of [] -> []; h:tl -> append (map (\a -> (h,a)) ys) (cartesian tl ys)
+
+main = let () = iter print_int [1,2,3] in let () = print_int (length (cartesian [1,2] [1,2,3,4])) in 0
diff --git a/Haskell/tests/qcheck.t b/Haskell/tests/qcheck.t
deleted file mode 100644
index 36cbac32e..000000000
--- a/Haskell/tests/qcheck.t
+++ /dev/null
@@ -1,6 +0,0 @@
-Copyright 2024, Kostya Oreshin and Nikita Shchutskii
-SPDX-License-Identifier: MIT
-  $ ../lib/run_binding.exe -seed 67 -gen 1 -stop
-  random seed: 67
-  ================================================================================
-  success (ran 1 tests)
diff --git a/Haskell/tests/repl.t b/Haskell/tests/repl.t
new file mode 100644
index 000000000..03db34eb8
--- /dev/null
+++ b/Haskell/tests/repl.t
@@ -0,0 +1,181 @@
+Copyright 2024, Kostya Oreshin and Nikita Shchutskii
+SPDX-License-Identifier: MIT
+  $ ../lib/run_binding.exe -seed 67 -gen 1 -stop
+  random seed: 67
+  ================================================================================
+  success (ran 1 tests)
+
+  $ ../bin/REPL.exe manytests/do_not_type/001.hs
+  Undefined variable 'fac'
+
+  $ ../bin/REPL.exe manytests/do_not_type/002if.hs
+  unification failed on Int and Bool
+
+  $ ../bin/REPL.exe manytests/do_not_type/003occurs.hs
+  Occurs check failed
+
+  $ ../bin/REPL.exe manytests/do_not_type/004_let_poly.hs
+  unification failed on Int and Bool
+
+  $ ../bin/REPL.exe manytests/do_not_type/099.hs
+  unification failed on Maybe t5 and Ord t8 -> Ord t8 -> Bool
+  unification failed on () and t10 -> t10
+  [ 
+  x:  Int
+   ]
+
+  $ ../bin/REPL.exe manytests/typed/001fac.hs
+  [ 
+  fac:  Int -> Int
+  main:  Int
+   ]
+
+  $ ../bin/REPL.exe manytests/typed/002fac.hs
+  [ 
+  fac_cps: t11.  Int -> (Int -> t11) -> t11
+  main:  Int
+   ]
+
+  $ ../bin/REPL.exe manytests/typed/003fib.hs
+  [ 
+  fib:  Int -> Int
+  fib_acc:  Int -> Int -> Int -> Int
+  main:  Int
+   ]
+
+  $ ../bin/REPL.exe manytests/typed/004manyargs.hs
+  [ 
+  main:  Int
+  test10:  Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int
+  test3:  Int -> Int -> Int -> Int
+  wrap: t1.  t1 -> t1
+   ]
+
+  $ ../bin/REPL.exe manytests/typed/005fix.hs
+  [ 
+  fac:  (Int -> Int) -> Int -> Int
+  fix: t2. t5.  ((t2 -> t5) -> t2 -> t5) -> t2 -> t5
+  main:  Int
+   ]
+
+  $ ../bin/REPL.exe manytests/typed/006partial.hs
+  [ 
+  foo:  Bool -> Int -> Int
+  foo2:  Int -> Int
+  main:  Int
+   ]
+
+  $ ../bin/REPL.exe manytests/typed/006partial2.hs
+  [ 
+  foo:  Int -> Int -> Int -> Int
+  main:  Int
+   ]
+
+  $ ../bin/REPL.exe manytests/typed/006partial3.hs
+  [ 
+  foo:  Int -> Int -> Int -> ()
+  main:  Int
+   ]
+
+  $ ../bin/REPL.exe manytests/typed/007order.hs
+  [ 
+  _start:  () -> () -> Int -> () -> Int -> Int -> () -> Int -> Int -> Int
+  main:  ()
+   ]
+
+  $ ../bin/REPL.exe manytests/typed/008ascription.hs
+  [ 
+  addi: t4.  (t4 -> Bool -> Int) -> (t4 -> Bool) -> t4 -> Int
+  main:  Int
+   ]
+
+  $ ../bin/REPL.exe manytests/typed/009let_poly.hs
+  [ 
+  temp:  (Int, Bool)
+   ]
+
+
+  $ ../bin/REPL.exe manytests/typed/010sukharev.hs
+  [ 
+  _1: t5.  Int -> Int -> (Int, t5) -> Bool
+  _2:  Int
+  _3:  Maybe (Int, Bool)
+  _4:  Int
+  _42: t47.  t47 -> Bool
+  _5: t44.  Int -> t44
+  int_of_option: t38.  Maybe t38 -> Int
+   ]
+  $ ../bin/REPL.exe manytests/typed/015tuples.hs
+  [ 
+  feven: t37.  (t37, Int -> Int) -> Int -> Int
+  fix: t2. t5.  ((t2 -> t5) -> t2 -> t5) -> t2 -> t5
+  fixpoly: t24. t27.  ((t24 -> t27, t24 -> t27) -> t24 -> t27, (t24 -> t27, t24 -> t27) -> t24 -> t27) -> (t24 -> t27, t24 -> t27)
+  fodd: t49.  (Int -> Int, t49) -> Int -> Int
+  main:  Int
+  map: t12. t14.  (t12 -> t14) -> (t12, t12) -> (t14, t14)
+  meven:  Int -> Int
+  modd:  Int -> Int
+  tie:  (Int -> Int, Int -> Int)
+   ]
+
+  $ ../bin/REPL.exe manytests/typed/016lists.hs
+  [ 
+  append: t72.  [t72] -> [t72] -> [t72]
+  cartesian: t110. t117.  [t110] -> [t117] -> [(t110, t117)]
+  concat: t94.  [[t94]] -> [t94]
+  iter: t99.  (t99 -> ()) -> [t99] -> ()
+  length: t3.  [t3] -> Int
+  length_tail: t22.  [t22] -> Int
+  main:  Int
+  map: t28. t29.  (t28 -> t29) -> [t28] -> [t29]
+   ]
+
+  $ ../bin/REPL.exe <<-EOF
+  >  fac0 self n = if n<2 then n else n* self (n-1) 
+  >  fix f = f (fix f)
+  >  fac = fix fac0
+  >  main = print_int (fac 3)
+  > EOF
+  [ 
+  fac0:  (Int -> Int) -> Int -> Int
+   ]
+  [ 
+  fix: t11.  (t11 -> t11) -> t11
+   ]
+  [ 
+  fac:  Int -> Int
+   ]
+  [ 
+  main:  ()
+   ]
+
+# fibonacci
+  $ ../bin/REPL.exe <<-EOF
+  > iter f xs = case xs of [] -> (); h:tl -> let () = f h in iter f tl
+  > take n xs = case xs of [] -> []; h:tl -> if n>0 then h : (take (n-1) tl) else []
+  > tail xs = case xs of h:tl -> tl
+  > zip_with f xs ys = case (xs,ys) of ([],[]) -> []; (h:tl, h2:tl2) -> (f h h2) : zip_with f tl tl2
+  > fib = 0:1:(zip_with (+) fib (tail fib))
+  > main = let () = iter print_int (take 10 fib) in 0
+  > EOF
+  [ 
+  iter: t4.  (t4 -> ()) -> [t4] -> ()
+   ]
+  [ 
+  take: t16.  Int -> [t16] -> [t16]
+   ]
+  [ 
+  tail: t31.  [t31] -> [t31]
+   ]
+  [ 
+  zip_with: t39. t40. t41.  (t39 -> t40 -> t41) -> [t39] -> [t40] -> [t41]
+   ]
+  [ 
+  fib:  [Int]
+   ]
+  [ 
+  main:  Int
+   ]
+
+
+# TODO(Kakadu): It would be great to call read GHCi somewhere in the tests
diff --git a/Haskell/lib/tests/dune b/Haskell/tests/tests/dune
similarity index 78%
rename from Haskell/lib/tests/dune
rename to Haskell/tests/tests/dune
index 34f79c31e..08eea4f79 100644
--- a/Haskell/lib/tests/dune
+++ b/Haskell/tests/tests/dune
@@ -3,6 +3,6 @@
  (public_name Haskell.Lib.Test)
  (libraries haskell_lib)
  (inline_tests)
- (modules Pprintast_test)
+ (modules Pprintast_test Inferencer_test)
  (preprocess
   (pps ppx_inline_test ppx_expect)))
diff --git a/Haskell/tests/tests/inferencer_test.ml b/Haskell/tests/tests/inferencer_test.ml
new file mode 100644
index 000000000..88e08d38f
--- /dev/null
+++ b/Haskell/tests/tests/inferencer_test.ml
@@ -0,0 +1,1409 @@
+(** Copyright 2024, Kostya Oreshin and Nikita Shchutskii *)
+
+(** SPDX-License-Identifier: MIT *)
+
+let%expect_test "int type" =
+  Haskell_lib.Pai.parse_and_infer [ "a = 42" ] false Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    [
+    a:  Int
+     ] |}]
+;;
+
+let%expect_test "bool type" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = True" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    [
+    a:  Bool
+     ] |}]
+;;
+
+let%expect_test "unit type" =
+  Haskell_lib.Pai.parse_and_infer [ "a = ()" ] false Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    [
+    a:  ()
+     ] |}]
+;;
+
+let%expect_test "const with explicit correct single type" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = 42 :: Int" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    [
+    a:  Int
+     ] |}]
+;;
+
+let%expect_test "const with explicit correct multiple type" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = (42 :: Int) :: Int" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    [
+    a:  Int
+     ] |}]
+;;
+
+let%expect_test "const with explicit wrong single type" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = 42 :: Bool" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {| unification failed on Int and Bool |}]
+;;
+
+let%expect_test "const with explicit wrong multiple type" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = (42 :: Int) :: Bool" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {| unification failed on Bool and Int |}]
+;;
+
+let%expect_test "tuple" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = (42, True)" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    [
+    a:  (Int, Bool)
+     ] |}]
+;;
+
+let%expect_test "tuple with extra types" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = (42, True, ())" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    [
+    a:  (Int, Bool, ())
+     ] |}]
+;;
+
+let%expect_test "tuple with explicit correct single type" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = (42, True, ()) :: (Int, Bool, ())" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    [
+    a:  (Int, Bool, ())
+     ] |}]
+;;
+
+let%expect_test "tuple with explicit correct multiple type" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = ((42, True, ()) :: (Int, Bool, ())) :: (Int, Bool, ())" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    [
+    a:  (Int, Bool, ())
+     ] |}]
+;;
+
+let%expect_test "tuple with explicit wrong single type" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "x = (42, True, ()) :: (Bool, Bool, ())" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {| unification failed on Int and Bool |}]
+;;
+
+let%expect_test "tuple with explicit wrong multiple type" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "x = ((42, True, ()) :: (Int, Bool, ())) :: (Bool, Bool, ())" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {| unification failed on Bool and Int |}]
+;;
+
+let%expect_test "maybe type just" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = \\x -> Just x" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    [
+    a: t2.  t2 -> Maybe t2
+     ] |}]
+;;
+
+let%expect_test "maybe type just int" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = \\x -> Just (x + 1)" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    [
+    a:  Int -> Maybe Int
+     ] |}]
+;;
+
+let%expect_test "maybe type just list" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = \\x y -> Just (y : x)" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    [
+    a: t5.  [t5] -> t5 -> Maybe [t5]
+     ] |}]
+;;
+
+let%expect_test "maybe type nothing" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = Nothing" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    [
+    a: t2.  Maybe t2
+     ] |}]
+;;
+
+let%expect_test "correct ariphmetic operation" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = 5 + 3" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    [
+    a:  Int
+     ] |}]
+;;
+
+let%expect_test "incorrect ariphmetic operation" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = 5 + ()" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {| unification failed on () and Int |}]
+;;
+
+let%expect_test "ariphmetic operation with explicit correct single type" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = (5 + 3) :: Int" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    [
+    a:  Int
+     ] |}]
+;;
+
+let%expect_test "ariphmetic operation with explicit correct multiple type" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = ((5 + 3) :: Int) :: Int" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    [
+    a:  Int
+     ] |}]
+;;
+
+let%expect_test "ariphmetic operation with explicit wrong single type" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = (5 + 3) :: Bool" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {| unification failed on Int and Bool |}]
+;;
+
+let%expect_test "ariphmetic operation with explicit wrong multiple type" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = ((5 + 3) :: Int) :: Bool" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {| unification failed on Bool and Int |}]
+;;
+
+let%expect_test "correct logical operation" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = True && False" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    [
+    a:  Bool
+     ] |}]
+;;
+
+let%expect_test "incorrect logical operation" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = True && 1" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {| unification failed on Int and Bool |}]
+;;
+
+let%expect_test "logical operation with correct explicit single type" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = True && False :: Bool" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    [
+    a:  Bool
+     ] |}]
+;;
+
+let%expect_test "logical operation with correct explicit multiple type" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = (True && False :: Bool) :: Bool" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    [
+    a:  Bool
+     ] |}]
+;;
+
+let%expect_test "logical operation with incorrect explicit single type" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = True && False :: Int" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {| unification failed on Bool and Int |}]
+;;
+
+let%expect_test "logical operation with incorrect explicit multiple type" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = (True && False :: Bool) :: Int" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {| unification failed on Int and Bool |}]
+;;
+
+let%expect_test "correct comparison operation with int" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = 1 <= 2" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    [
+    a:  Bool
+     ] |}]
+;;
+
+let%expect_test "correct comparison operation with bool" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = False <= True" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    [
+    a:  Bool
+     ] |}]
+;;
+
+let%expect_test "incorrect comparison operation with () and int" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = 1 <= ()" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {| unification failed on () and Int |}]
+;;
+
+let%expect_test "incorrect comparison operation with bool and int" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = 1 <= True" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {| unification failed on Bool and Int |}]
+;;
+
+let%expect_test "comparison operation with explicit correct single type" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = (1 <= 2) :: Bool" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    [
+    a:  Bool
+     ] |}]
+;;
+
+let%expect_test "comparison operation with explicit correct multiple type" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = ((1 <= 2) :: Bool) :: Bool" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    [
+    a:  Bool
+     ] |}]
+;;
+
+let%expect_test "comparison operation with explicit wrong single type" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = (1 <= 2) :: Int" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {| unification failed on Bool and Int |}]
+;;
+
+let%expect_test "comparison operation with explicit wrong multiple type" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = ((1 <= 2) :: Int) :: Bool" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {| unification failed on Bool and Int |}]
+;;
+
+let%expect_test "cons correct with int" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = 1 : []" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    [
+    a:  [Int]
+     ] |}]
+;;
+
+let%expect_test "cons correct with bool" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = True : []" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    [
+    a:  [Bool]
+     ] |}]
+;;
+
+let%expect_test "cons incorrect with int" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = 1 : 2" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {| unification failed on Int and [Int] |}]
+;;
+
+let%expect_test "cons incorrect with bool" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = True : False" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {| unification failed on Bool and [Bool] |}]
+;;
+
+let%expect_test "cons incorrect with int and bool" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = 1 : [True]" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {| unification failed on Bool and Int |}]
+;;
+
+let%expect_test "neg type correct" =
+  Haskell_lib.Pai.parse_and_infer [ "a = -42" ] false Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    [
+    a:  Int
+     ] |}]
+;;
+
+let%expect_test "neg type incorrect" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = -True" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {| unification failed on Bool and Int |}]
+;;
+
+let%expect_test "neg type with explicit correct single type" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = -42 :: Int" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    [
+    a:  Int
+     ] |}]
+;;
+
+let%expect_test "neg type with explicit correct multiple type" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = (-42 :: Int) :: Int" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    [
+    a:  Int
+     ] |}]
+;;
+
+let%expect_test "neg type with explicit wrong single type" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = -42 :: Bool" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {| unification failed on Int and Bool |}]
+;;
+
+let%expect_test "neg type with explicit wrong multiple type" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = (-42 :: Int) :: Bool" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {| unification failed on Bool and Int |}]
+;;
+
+let%expect_test "ord polymor" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = (\\f -> let g = (f True) in (f 3)) (\\x -> x)" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {| unification failed on Bool and Int |}]
+;;
+
+let%expect_test "if correct with int return type" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = if True then 1 else -1" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    [
+    a:  Int
+     ] |}]
+;;
+
+let%expect_test "if correct with tuple return type" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = if True then (True, 2) else (False, -1)" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    [
+    a:  (Bool, Int)
+     ] |}]
+;;
+
+let%expect_test "if incorrect with int condition" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = if (1 + 2) then (True, 2) else (False, -1)" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {| unification failed on Int and Bool |}]
+;;
+
+let%expect_test "if incorrect with tuple condition" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = if (True, ()) then (True, 2) else (False, -1)" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {| unification failed on (Bool, ()) and Bool |}]
+;;
+
+let%expect_test "if incorrect with int and bool return types" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = if True then 1 else False" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {| unification failed on Int and Bool |}]
+;;
+
+let%expect_test "if incorrect with int and tuple return types" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = if True then 1 else (1, False)" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {| unification failed on Int and (Int, Bool) |}]
+;;
+
+let%expect_test "if incorrect with bool and list return types" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = if True then True else [1, 4]" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {| unification failed on Bool and [Int] |}]
+;;
+
+let%expect_test "lambda ident" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = \\x -> x" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    [
+    a: t2.  t2 -> t2
+     ] |}]
+;;
+
+let%expect_test "lambda int return type" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = \\x -> 1" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    [
+    a: t2.  t2 -> Int
+     ] |}]
+;;
+
+let%expect_test "lambda narrowing to int type" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = \\x -> x + 1" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    [
+    a:  Int -> Int
+     ] |}]
+;;
+
+let%expect_test "lambda tuple return type" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = \\x -> (x, ())" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    [
+    a: t2.  t2 -> (t2, ())
+     ] |}]
+;;
+
+let%expect_test "lambda multiple arguments" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = \\x y z -> x + y + z" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    [
+    a:  Int -> Int -> Int -> Int
+     ] |}]
+;;
+
+let%expect_test "lambda narrowing to list type" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = \\x -> 1 : x" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    [
+    a:  [Int] -> [Int]
+     ] |}]
+;;
+
+let%expect_test "lambda narrowing to arrow type" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = \\f -> \\y -> f y" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    [
+    a: t3. t4.  (t3 -> t4) -> t3 -> t4
+     ] |}]
+;;
+
+let%expect_test "lambda occurs check" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = \\x -> x x" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {| Occurs check failed |}]
+;;
+
+let%expect_test "lambda tuple return type" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = \\x -> x `mod` 2 == 0 && x > 5" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    [
+    a:  Int -> Bool
+     ] |}]
+;;
+
+let%expect_test "lambda correct with explicit single type" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = (\\x -> 1) :: (Int -> Int)" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    [
+    a:  Int -> Int
+     ] |}]
+;;
+
+let%expect_test "lambda correct with explicit multiple type" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = ((\\x -> 1) :: (Bool -> Int)) :: (Bool -> Int)" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    [
+    a:  Bool -> Int
+     ] |}]
+;;
+
+let%expect_test "lambda wrong with explicit single type" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = (\\x -> ()) :: (() -> Bool)" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {| unification failed on () and Bool |}]
+;;
+
+let%expect_test "lambda wrong with explicit multiple type" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = ((\\x -> ()) :: (() -> ())) :: (() -> [Int])" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {| unification failed on [Int] and () |}]
+;;
+
+let%expect_test "let id" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = let x = x in x" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    [
+    a: t3.  t3
+     ] |}]
+;;
+
+let%expect_test "let narrowing to int" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = let x = x; y = 1 in x + y" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    [
+    a:  Int
+     ] |}]
+;;
+
+let%expect_test "let narrowing to [int]" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = let x = x; y = 1 in y : x" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    [
+    a:  [Int]
+     ] |}]
+;;
+
+let%expect_test "let narrowing to bool" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = let x = x; y = True in y && x" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    [
+    a:  Bool
+     ] |}]
+;;
+
+let%expect_test "let function" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = let compose f g x = f (g x) in compose" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    [
+    a: t8. t9. t10.  (t9 -> t10) -> (t8 -> t9) -> t8 -> t10
+     ] |}]
+;;
+
+let%expect_test "let recursive fib" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = let fib n = if (n == 0) then 0 else if (n==1) then 1 else ((fib (n-1)) + (fib \
+       (n-2))) in fib"
+    ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    [
+    a:  Int -> Int
+     ] |}]
+;;
+
+let%expect_test "let recursive fac" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = let factorial = \\n -> if n == 0 then 1 else n * factorial (n - 1) in \
+       factorial"
+    ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    [
+    a:  Int -> Int
+     ] |}]
+;;
+
+let%expect_test "let with explicit correct single type" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = let (x :: Int) = x in x" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    [
+    a:  Int
+     ] |}]
+;;
+
+let%expect_test "let with explicit correct mutliple type" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = let ((x :: Int) :: Int) = x in x" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    [
+    a:  Int
+     ] |}]
+;;
+
+let%expect_test "let with explicit wrong single type" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = let (x :: Bool) = 1 in x" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {| unification failed on Bool and Int |}]
+;;
+
+let%expect_test "let with explicit wrong mutliple type" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = let ((x :: Int) :: Bool) = x in x" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {| unification failed on Bool and Int |}]
+;;
+
+let%expect_test "let wrong unification" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = let x = if x <= True then 1 else 0 in x + 1" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {| unification failed on Bool and Int |}]
+;;
+
+let%expect_test "let wrong unification" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = let x = if x <= True then True else False in x" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    [
+    a:  Bool
+     ] |}]
+;;
+
+let%expect_test "let wrong unification" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = let x = if x <= True then True else False in x" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    [
+    a:  Bool
+     ] |}]
+;;
+
+let%expect_test "case correct with int type" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = \\x -> case x of 1 -> True; 2 -> False" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    [
+    a:  Int -> Bool
+     ] |}]
+;;
+
+let%expect_test "case correct with lists" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = \\x -> case x of (x:xs) -> x; [] -> []" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    [
+    a: t7.  [[t7]] -> [t7]
+     ] |}]
+;;
+
+let%expect_test "case correct with int lists and explicit similar types" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = \\x -> case x of ((x :: [Int]):(xs :: [[Int]])) -> x; [] -> []" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    [
+    a:  [[Int]] -> [Int]
+     ] |}]
+;;
+
+let%expect_test "case incorrect with int lists and explicit different types" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = \\x -> case x of ((x :: [Int]):(xs :: [[Bool]])) -> x; [] -> []" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {| unification failed on Bool and Int |}]
+;;
+
+let%expect_test "function apply incorrect" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = (\\x -> x + 1) True" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {| unification failed on Int and Bool |}]
+;;
+
+let%expect_test "function apply list return type" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = (\\x -> x : []) True" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    [
+    a:  [Bool]
+     ] |}]
+;;
+
+let%expect_test "function apply with correct single type" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = (\\(x :: Int) -> x <= 2) 1" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    [
+    a:  Bool
+     ] |}]
+;;
+
+let%expect_test "function apply return correct multiple type" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = (\\((x :: Int) :: Int) -> x <= 2) 1" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    [
+    a:  Bool
+     ] |}]
+;;
+
+let%expect_test "function apply return wrong single type" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = (\\(x :: Bool) -> x <= 2) 1" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {| unification failed on Int and Bool |}]
+;;
+
+let%expect_test "function apply return wrong multiple type" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = (\\((x :: Int) :: Bool) -> x <= 2) 1" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {| unification failed on Bool and Int |}]
+;;
+
+let%expect_test "function apply return correct single type" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = (\\(x :: Int) -> x : []) 1" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    [
+    a:  [Int]
+     ] |}]
+;;
+
+let%expect_test "list int" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = [1, 2]" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    [
+    a:  [Int]
+     ] |}]
+;;
+
+let%expect_test "lazy list int" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = [1..]" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    [
+    a:  [Int]
+     ] |}]
+;;
+
+let%expect_test "lazy list wrong type" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = [(True, 1)..]" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {| unification failed on Enum t2 and (Bool, Int) |}]
+;;
+
+let%expect_test "list of list" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = [[True]]" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    [
+    a:  [[Bool]]
+     ] |}]
+;;
+
+let%expect_test "wrong list of different types" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = [True, (), 3]" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {| unification failed on Bool and () |}]
+;;
+
+let%expect_test "comprehension list with generator" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = [x * y | x <- [1..10], y <- [1]]" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    [
+    a:  [Int]
+     ] |}]
+;;
+
+let%expect_test "comprehension list with simple condition" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = [1 * 2 | True]" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    [
+    a:  [Int]
+     ] |}]
+;;
+
+let%expect_test "comprehension list with condition" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = \\x -> [ x | x < 10 ]" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    [
+    a:  Int -> [Int]
+     ] |}]
+;;
+
+let%expect_test "comprehension list with condition and generator" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = \\y -> [ x * y | x <- [1..10], y <= 10  ]" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    [
+    a:  Int -> [Int]
+     ] |}]
+;;
+
+let%expect_test "wrong comprehension list with generator condition" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = \\x y -> [ x * y | x < 10, y <- [True, False]]" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {| unification failed on Bool and Int |}]
+;;
+
+let%expect_test "several functions" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "f x = g x; g y = y" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+[
+f: t2.  t2 -> t2
+g: t2.  t2 -> t2
+ ] |}]
+;;
+
+let%expect_test "several bindings non_poly" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "f x = x; g = f True" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+[
+f:  Bool -> Bool
+g:  Bool
+ ] |}]
+;;
+
+let%expect_test "mutually recursive functions" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "f x = g x; g y = f y" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+  [
+  f: t2. t3.  t2 -> t3
+  g: t2. t3.  t2 -> t3
+   ] |}]
+;;
+
+let%expect_test "mutually recursive functions with guards" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "isEven n | n == 0 = True | n > 0 = isOdd (n - 1) | True = isOdd (-n); isOdd n | n \
+       == 0 = False | n > 0 = isEven (n - 1) | True = isEven (-n)"
+    ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+  [
+  isEven:  Int -> Bool
+  isOdd:  Int -> Bool
+   ] |}]
+;;
+
+let%expect_test "guards" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "f x | x > 0 = x | True = -1" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    [
+    f:  Int -> Int
+     ] |}]
+;;
+
+let%expect_test "where single statement" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "f x = x + y where y = 1" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {| 
+    [
+    f:  Int -> Int
+     ] |}]
+;;
+
+let%expect_test "where single statement with explicit incorrect type" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "f x = x + y where (y :: Bool) = 1" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {| unification failed on Bool and Int |}]
+;;
+
+let%expect_test "where multiple statements" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "f x = x && y || z where y = False; z = True" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {| 
+    [
+    f:  Bool -> Bool
+     ] |}]
+;;
+
+let%expect_test "where single statement incorrect" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "f x = x + y where y = True" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {| unification failed on Bool and Int |}]
+;;
+
+let%expect_test "where single statement with param shadowing incorrect" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "f x y = x + y where y = True" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {| unification failed on Bool and Int |}]
+;;
+
+let%expect_test "where multiple statements incorrect" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "f x  = x && y || z where y = False; z = 3" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {| unification failed on Int and Bool |}]
+;;
+
+let%expect_test "where polymorphic argument" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "f x = y where y = False" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    [
+    f: t1.  t1 -> Bool
+     ] |}]
+;;
+
+let%expect_test "where list argument" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "f (x:xs) = y : xs where y = 2" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    [
+    f:  [Int] -> [Int]
+     ] |}]
+;;
+
+let%expect_test "function with tuple argument" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "f (x, y) = (x + 1, y && True)" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    [
+    f:  (Int, Bool) -> (Int, Bool)
+     ] |}]
+;;
+
+let%expect_test "several functions with incorrect type" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "f x = x + 1; g = f y where y = False" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {| unification failed on Bool and Int |}]
+;;
+
+let%expect_test "correct arrow declaration" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "f :: Int -> Int; f x = x" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    [
+    f:  Int -> Int
+     ] |}]
+;;
+
+let%expect_test "incorrect arrow declaration" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "f :: Int; f x = x" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {| unification failed on Int and t1 -> t1 |}]
+;;
+
+let%expect_test "incorrect arrow declaration with different types" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "f :: Int -> Bool; f x = x" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    unification failed on Bool and Int |}]
+;;
+
+let%expect_test "incorrect list declaration with different types" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a :: [Int]; a = [False, True]" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    unification failed on Int and Bool |}]
+;;
+
+let%expect_test "correct declaration with explicit type" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a :: [Int]; (a :: [Int]) = [1, 2]" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    [
+    a:  [Int]
+     ] |}]
+;;
+
+let%expect_test "incorrect declaration with explicit type" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "f :: Bool -> Bool; f (x :: Int) = x" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    unification failed on Bool and Int |}]
+;;
+
+let%expect_test "correct tuple declaration" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a :: (Int, Bool, ()); a = (1, True, ())" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    [
+    a:  (Int, Bool, ())
+     ] |}]
+;;
+
+let%expect_test "incorrect tuple declaration" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a :: (Int, Bool, ()); a = (False, True, ())" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    unification failed on Int and Bool |}]
+;;
+
+let%expect_test "failed unification" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = let f = (\\id -> (id 1, id True)) (\\x -> x) in f" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {| unification failed on Int and Bool |}]
+;;
+
+let%expect_test "generalization" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = let f = \\x -> let const = \\y -> x in const x in f" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    [
+    a: t10.  t10 -> t10
+     ] |}]
+;;
+
+let%expect_test "compatible restrictions" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = let double f z = f (f z) in (double (\\x -> x+1) 1, double (\\x -> x && x) \
+       False)"
+    ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    [
+    a:  (Int, Bool)
+     ] |}]
+;;
+
+let%expect_test "y-combinator" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = let fix f = f (fix f) in fix" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    [
+    a: t6.  (t6 -> t6) -> t6
+     ] |}]
+;;
+
+let%expect_test "z-combinator without recursion" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = let fix f eta = f (fix f) eta in fix" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    [
+    a: t8. t9.  ((t8 -> t9) -> t8 -> t9) -> t8 -> t9
+     ] |}]
+;;
+
+let%expect_test "occurs check" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = let f x = f in f" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {| Occurs check failed |}]
+;;
+
+let%expect_test "let poly" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = let f = (\\x -> x) in let g = (f True) in f 3" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    [
+    a:  Int
+     ] |}]
+;;
+
+let%expect_test "fail unification" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "a = (\\f -> let g = (f True) in (f 3)) (\\x -> x)" ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {| unification failed on Bool and Int |}]
+;;
+
+let%expect_test "unif with ord, succ" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "f x = x > (1,2); g y = y < Just True " ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    [
+    f:  (Int, Int) -> Bool
+    g:  Maybe Bool -> Bool
+     ] |}]
+;;
+
+let%expect_test "unif with ord, fail (tuple)" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "f x = x > (1, \\ x -> x) " ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    unification failed on Ord t6 and t3 -> t3 |}]
+;;
+
+let%expect_test "unif with ord, fail" =
+  Haskell_lib.Pai.parse_and_infer
+    [ "f x = x > [\\ x -> x] " ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    unification failed on Ord t6 and t4 -> t4 |}]
+;;
+
+let%expect_test "tree param valid" =
+  Haskell_lib.Pai.parse_and_infer
+    [ " f (x; (1; $;$); $) = x " ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    [
+    f:  {Int} -> Int
+     ] |}]
+;;
+
+let%expect_test "tree param invalid" =
+  Haskell_lib.Pai.parse_and_infer
+    [ " f (x; (True; $;$); $) = x - x " ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    unification failed on Bool and Int |}]
+;;
+
+let%expect_test "tree expr valid" =
+  Haskell_lib.Pai.parse_and_infer
+    [ " f x  = (x; (1; $;$); $) " ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    [
+    f:  Int -> {Int}
+     ] |}]
+;;
+
+let%expect_test "tree param invalid" =
+  Haskell_lib.Pai.parse_and_infer
+    [ " f x = ((x; (True; $;$); $), x - x) " ]
+    false
+    Haskell_lib.Inferencer.typeenv_empty;
+  [%expect {|
+    unification failed on Bool and Int |}]
+;;
diff --git a/Haskell/lib/tests/pprintast_test.mli b/Haskell/tests/tests/inferencer_test.mli
similarity index 100%
rename from Haskell/lib/tests/pprintast_test.mli
rename to Haskell/tests/tests/inferencer_test.mli
diff --git a/Haskell/lib/tests/pprintast_test.ml b/Haskell/tests/tests/pprintast_test.ml
similarity index 100%
rename from Haskell/lib/tests/pprintast_test.ml
rename to Haskell/tests/tests/pprintast_test.ml
diff --git a/Haskell/tests/tests/pprintast_test.mli b/Haskell/tests/tests/pprintast_test.mli
new file mode 100644
index 000000000..e06ef3aab
--- /dev/null
+++ b/Haskell/tests/tests/pprintast_test.mli
@@ -0,0 +1,3 @@
+(** Copyright 2024, Kostya Oreshin and Nikita Shchutskii *)
+
+(** SPDX-License-Identifier: MIT *)
diff --git a/manytests/do_not_type/001.ml b/manytests/do_not_type/001.ml
new file mode 100644
index 000000000..8618315ae
--- /dev/null
+++ b/manytests/do_not_type/001.ml
@@ -0,0 +1 @@
+let recfac n = if n<=1 then 1 else n * fac (n-1)
\ No newline at end of file
diff --git a/manytests/do_not_type/002if.ml b/manytests/do_not_type/002if.ml
new file mode 100644
index 000000000..515dbc989
--- /dev/null
+++ b/manytests/do_not_type/002if.ml
@@ -0,0 +1 @@
+let main = if true then 1 else false
\ No newline at end of file
diff --git a/manytests/do_not_type/003occurs.ml b/manytests/do_not_type/003occurs.ml
new file mode 100644
index 000000000..9b6c9c6d6
--- /dev/null
+++ b/manytests/do_not_type/003occurs.ml
@@ -0,0 +1 @@
+let fix f = (fun x -> f (fun f -> x x f))  (fun x -> f (fun f -> x x f))
diff --git a/manytests/do_not_type/004let_poly.ml b/manytests/do_not_type/004let_poly.ml
new file mode 100644
index 000000000..e2f1ba493
--- /dev/null
+++ b/manytests/do_not_type/004let_poly.ml
@@ -0,0 +1,6 @@
+let _1 =
+  (fun f -> (f 1, f true)) (fun x -> x)
+
+let _2 = function
+  | Some f -> let _ = f "42" in f 42
+  | None -> 1
\ No newline at end of file
diff --git a/manytests/do_not_type/015tuples.ml b/manytests/do_not_type/015tuples.ml
new file mode 100644
index 000000000..cf97262c6
--- /dev/null
+++ b/manytests/do_not_type/015tuples.ml
@@ -0,0 +1,3 @@
+let rec (a,b) = (a,b)
+
+let a, _ = 1, 2, 3
diff --git a/manytests/do_not_type/099.ml b/manytests/do_not_type/099.ml
new file mode 100644
index 000000000..1a6e359d3
--- /dev/null
+++ b/manytests/do_not_type/099.ml
@@ -0,0 +1,7 @@
+let rec Some x = Some 1
+
+let rec x = x + 1
+
+let Some a = (fun x -> x)
+
+let () = (fun x -> x)
\ No newline at end of file
diff --git a/manytests/typed/001fac.ml b/manytests/typed/001fac.ml
new file mode 100644
index 000000000..2c335f125
--- /dev/null
+++ b/manytests/typed/001fac.ml
@@ -0,0 +1,6 @@
+let rec fac n = if n<=1 then 1 else n * fac (n-1)
+
+let main =
+  let () = print_int (fac 4) in
+  0
+
diff --git a/manytests/typed/002fac.ml b/manytests/typed/002fac.ml
new file mode 100644
index 000000000..f40bcc7fa
--- /dev/null
+++ b/manytests/typed/002fac.ml
@@ -0,0 +1,8 @@
+let rec fac_cps n k =
+  if n=1 then k 1 else
+  fac_cps (n-1) (fun p -> k (p*n))
+
+let main =
+  let () = print_int (fac_cps 4 (fun print_int -> print_int)) in
+  0
+
diff --git a/manytests/typed/003fib.ml b/manytests/typed/003fib.ml
new file mode 100644
index 000000000..270f3df38
--- /dev/null
+++ b/manytests/typed/003fib.ml
@@ -0,0 +1,17 @@
+let rec fib_acc a b n =
+  if n=1 then b
+  else
+    let n1 = n-1 in
+    let ab = a+b in
+    fib_acc b ab n1
+
+let rec fib n =
+  if n<2
+  then n
+  else fib (n - 1) + fib (n - 2) 
+
+let main =
+  let () = print_int (fib_acc 0 1 4) in
+  let () = print_int (fib 4) in
+  0
+
diff --git a/manytests/typed/004manyargs.ml b/manytests/typed/004manyargs.ml
new file mode 100644
index 000000000..aef00092c
--- /dev/null
+++ b/manytests/typed/004manyargs.ml
@@ -0,0 +1,19 @@
+let wrap f = if 1 = 1 then f else f
+
+let test3 a b c =
+  let a = print_int a in
+  let b = print_int b in
+  let c = print_int c in
+  0
+
+let test10 a b c d e f g h i j = a + b + c + d + e + f + g + h + i + j
+
+let main =
+  let rez =
+      (wrap test10 1 10 100 1000 10000 100000 1000000 10000000 100000000
+         1000000000)
+  in
+  let () = print_int rez in
+  let temp2 = wrap test3 1 10 100 in
+  0
+
diff --git a/manytests/typed/005fix.ml b/manytests/typed/005fix.ml
new file mode 100644
index 000000000..5b62f5fa2
--- /dev/null
+++ b/manytests/typed/005fix.ml
@@ -0,0 +1,8 @@
+let rec fix f x = f (fix f) x
+
+let fac self n = if n<=1 then 1 else n * self (n-1)
+
+let main =
+  let () = print_int (fix fac 6) in
+  0
+
diff --git a/manytests/typed/006partial.ml b/manytests/typed/006partial.ml
new file mode 100644
index 000000000..5b568d8e5
--- /dev/null
+++ b/manytests/typed/006partial.ml
@@ -0,0 +1,6 @@
+let foo b = if b then (fun foo -> foo+2) else (fun foo -> foo*10)
+
+let foo x = foo true (foo false (foo true (foo false x)))
+let main =
+  let () = print_int (foo 11) in
+  0
\ No newline at end of file
diff --git a/manytests/typed/006partial2.ml b/manytests/typed/006partial2.ml
new file mode 100644
index 000000000..d5eafc748
--- /dev/null
+++ b/manytests/typed/006partial2.ml
@@ -0,0 +1,12 @@
+let foo a b c =
+  let () = print_int a in
+  let () = print_int b in
+  let () = print_int c in
+  a + b * c
+
+let main =
+  let foo = foo 1 in
+  let foo = foo 2 in
+  let foo = foo 3 in
+  let () = print_int foo in
+  0
\ No newline at end of file
diff --git a/manytests/typed/006partial3.ml b/manytests/typed/006partial3.ml
new file mode 100644
index 000000000..1801a6ff1
--- /dev/null
+++ b/manytests/typed/006partial3.ml
@@ -0,0 +1,8 @@
+let foo a =
+  let () = print_int a in fun b ->
+  let () = print_int b in fun c ->
+  print_int c
+
+let main =
+  let () = foo 4 8 9 in
+  0
\ No newline at end of file
diff --git a/manytests/typed/007order.ml b/manytests/typed/007order.ml
new file mode 100644
index 000000000..a2f45813a
--- /dev/null
+++ b/manytests/typed/007order.ml
@@ -0,0 +1,8 @@
+let _start () () a () b _c () d __ =
+  let () = print_int (a+b) in
+  let () = print_int __ in
+  a*b / _c + d
+
+
+let main =
+  print_int (_start (print_int 1) (print_int 2) 3 (print_int 4) 100 1000 (print_int (-1)) 10000 (-555555))
\ No newline at end of file
diff --git a/manytests/typed/008ascription.ml b/manytests/typed/008ascription.ml
new file mode 100644
index 000000000..c3d985578
--- /dev/null
+++ b/manytests/typed/008ascription.ml
@@ -0,0 +1,5 @@
+let addi = fun f g x -> (f x (g x: bool) : int)
+
+let main =
+  let () = print_int (addi (fun x b -> if b then x+1 else x*2) (fun _start -> _start/2 = 0) 4) in
+  0
\ No newline at end of file
diff --git a/manytests/typed/009let_poly.ml b/manytests/typed/009let_poly.ml
new file mode 100644
index 000000000..a679b67ce
--- /dev/null
+++ b/manytests/typed/009let_poly.ml
@@ -0,0 +1,3 @@
+let temp =
+  let f = fun x -> x in
+  (f 1, f true)
\ No newline at end of file
diff --git a/manytests/typed/010sukharev.ml b/manytests/typed/010sukharev.ml
new file mode 100644
index 000000000..b5ed3335c
--- /dev/null
+++ b/manytests/typed/010sukharev.ml
@@ -0,0 +1,23 @@
+let _1 = fun x y (a, _) -> (x + y - a) = 1
+
+let _2 =
+    let x, Some f = 1, Some ( "p1onerka was here" )
+    in x
+
+let _3 =  Some (1, "hi")
+
+let _4 = let rec f x = f 5 in f
+
+let _5 =
+    let id x = x in
+    match Some id with
+      | Some f -> let _ = f "42" in f 42
+      | None -> 0
+
+let _6 = fun arg -> match arg with Some x -> let y = x in y
+
+let int_of_option = function Some x -> x | None -> 0
+
+let _42 = function 42 -> true | _ -> false
+
+let id1, id2 = let id x = x in (id, id)
\ No newline at end of file
diff --git a/manytests/typed/015tuples.ml b/manytests/typed/015tuples.ml
new file mode 100644
index 000000000..e19762aaa
--- /dev/null
+++ b/manytests/typed/015tuples.ml
@@ -0,0 +1,22 @@
+let rec fix f x = f (fix f) x
+let map f p = let (a,b) = p in (f a, f b)
+let fixpoly l =
+  fix (fun self l -> map (fun li x -> li (self l) x) l) l
+let feven p n =
+  let (e, o) = p in
+  if n = 0 then 1 else o (n - 1)
+let fodd p n =
+  let (e, o) = p in
+  if n = 0 then 0 else e (n - 1)
+let tie = fixpoly (feven, fodd)
+
+let rec meven n = if n = 0 then 1 else modd (n - 1)
+and modd n = if n = 0 then 1 else meven (n - 1)
+let main =
+  let () = print_int (modd 1) in
+  let () = print_int (meven 2) in
+  let (even,odd) = tie in
+  let () = print_int (odd 3) in
+  let () = print_int (even 4) in
+  0
+
diff --git a/manytests/typed/016lists.ml b/manytests/typed/016lists.ml
new file mode 100644
index 000000000..b1312d900
--- /dev/null
+++ b/manytests/typed/016lists.ml
@@ -0,0 +1,41 @@
+let rec length xs =
+  match xs with
+  | [] -> 0
+  | h::tl -> 1 + length tl
+
+let length_tail =
+  let rec helper acc xs =
+  match xs with
+  | [] -> acc
+  | h::tl -> helper (acc + 1) tl
+  in
+  helper 0
+
+let rec map f xs =
+  match xs with
+  | [] -> []
+  | a::[] -> [f a]
+  | a::b::[] -> [f a; f b]
+  | a::b::c::[] -> [f a; f b; f c]
+  | a::b::c::d::tl -> f a :: f b :: f c :: f d :: map f tl
+
+let rec append xs ys = match xs with [] -> ys | x::xs -> x::(append xs ys)
+
+let concat =
+  let rec helper xs =
+    match xs with
+    | [] -> []
+    | h::tl -> append h (helper tl)
+  in helper
+
+let rec iter f xs = match xs with [] -> () | h::tl -> let () = f h in iter f tl
+
+let rec cartesian xs ys =
+  match xs with
+  | [] -> []
+  | h::tl -> append (map (fun a -> (h,a)) ys) (cartesian tl ys)
+
+let main =
+  let () = iter print_int [1;2;3] in
+  let () = print_int (length (cartesian [1;2] [1;2;3;4])) in
+  0