From 872fc115127e74fdd701aaa1c7e8e953e10cf03d Mon Sep 17 00:00:00 2001
From: Gleb Nasretdinov <gleb.nasretdinov@proton.me>
Date: Sat, 14 Dec 2024 16:57:39 +0300
Subject: [PATCH 01/15] ref: eta reduction

Signed-off-by: Gleb Nasretdinov <gleb.nasretdinov@proton.me>
---
 FSharpActivePatterns/lib/inferencer.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/FSharpActivePatterns/lib/inferencer.ml b/FSharpActivePatterns/lib/inferencer.ml
index 3cfe55884..ef7a1aef5 100644
--- a/FSharpActivePatterns/lib/inferencer.ml
+++ b/FSharpActivePatterns/lib/inferencer.ml
@@ -190,8 +190,8 @@ end = struct
   ;;
 
   (* aliases for Map actions *)
-  let find map key = Map.find map key
-  let remove map key = Map.remove map key
+  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.

From 3e51aa135eef2fea14499a475571430d4d63a384 Mon Sep 17 00:00:00 2001
From: Gleb Nasretdinov <gleb.nasretdinov@proton.me>
Date: Sun, 15 Dec 2024 15:56:49 +0300
Subject: [PATCH 02/15] feat: implement LetIn inference

Signed-off-by: Gleb Nasretdinov <gleb.nasretdinov@proton.me>
---
 FSharpActivePatterns/lib/inferencer.ml | 225 +++++++++++++++----------
 FSharpActivePatterns/lib/typedTree.ml  |   6 +-
 FSharpActivePatterns/lib/typedTree.mli |   2 +-
 FSharpActivePatterns/lib/typesPp.ml    |   5 +-
 4 files changed, 143 insertions(+), 95 deletions(-)

diff --git a/FSharpActivePatterns/lib/inferencer.ml b/FSharpActivePatterns/lib/inferencer.ml
index ef7a1aef5..d5c24714c 100644
--- a/FSharpActivePatterns/lib/inferencer.ml
+++ b/FSharpActivePatterns/lib/inferencer.ml
@@ -122,7 +122,7 @@ module Type : sig
   type t = typ
 
   val occurs_in : fresh -> t -> bool
-  (* val free_vars : t -> binder_set *)
+  val free_vars : t -> binder_set
 end = struct
   type t = typ
 
@@ -139,17 +139,17 @@ end = struct
   ;;
 
   (* 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
-     ;; *)
+  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 *)
@@ -217,7 +217,6 @@ end = struct
   let rec unify fst snd =
     match fst, snd with
     | Primitive fst, Primitive snd when String.equal fst snd -> return empty
-    | Primitive _, Primitive _ -> fail (`Unification_failed (fst, snd))
     | 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) ->
@@ -267,7 +266,7 @@ module Scheme : sig
 
   (* val occurs_in : fresh -> t -> bool *)
   val apply : Substitution.t -> t -> t
-  (* val free_vars : t -> binder_set *)
+  val free_vars : t -> binder_set
 end = struct
   type t = scheme
 
@@ -277,30 +276,33 @@ end = struct
      ;; *)
 
   (* take all vars that are not bound in typ *)
-  (* let free_vars = function
-     | S (vars, t) -> VarSet.diff (Type.free_vars t) vars
-     ;; *)
+  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 (S (vars, t)) =
+  let apply subst (Scheme (vars, t)) =
     let subst2 = VarSet.fold (fun key s -> Substitution.remove s key) vars subst in
-    S (vars, Substitution.apply subst2 t)
+    Scheme (vars, Substitution.apply subst2 t)
   ;;
 
   (* let pp = pp_scheme *)
 end
 
 module TypeEnvironment : sig
-  val extend : ('a, 'b, 'c) Base.Map.t -> 'a -> 'b -> ('a, 'b, 'c) Base.Map.t
-  val apply : Substitution.t -> ('a, scheme, 'b) Base.Map.t -> ('a, scheme, 'b) Base.Map.t
-  val empty : (string, 'a, Base.String.comparator_witness) Base.Map.t
-  val find : 'a -> ('a, 'b, 'c) Base.Map.t -> 'b option
+  type t
+
+  val free_vars : t -> VarSet.t
+  val extend : t -> string -> scheme -> t
+  val apply : Substitution.t -> t -> t
+  val empty : t
+  val find : string -> t -> scheme option
 end = struct
   open Base
 
   (* environment (context?) -- pairs of names and their types list *)
-  (* type t = (ident, scheme, String.comparator_witness) Map.t *)
+  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 *)
@@ -314,10 +316,10 @@ end = struct
   let find key env = Map.find env key
 
   (* 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))
-     ;; *)
+  let free_vars : t -> VarSet.t =
+    Map.fold ~init:VarSet.empty ~f:(fun ~key:_ ~data:s acc ->
+      VarSet.union acc (Scheme.free_vars s))
+  ;;
 
   (* TODO: custom pp_scheme? not from deriving *)
   (* let pp fmt map =
@@ -336,7 +338,7 @@ let make_fresh_var = fresh >>| fun n -> Type_var n
 
 (* replace all type vars with fresh ones *)
 let instantiate : scheme -> typ R.t =
-  fun (S (vars, t)) ->
+  fun (Scheme (vars, t)) ->
   VarSet.fold
     (fun name ty ->
       let* ty = ty in
@@ -349,11 +351,11 @@ let instantiate : scheme -> typ R.t =
 
 (* take free vars of type t and environment, put difference between them
    in S constructor so all vars are context independent *)
-(* let generalize : TypeEnvironment.t -> Type.t -> Scheme.t =
-   fun env t ->
-   let free = VarSet.diff (Type.free_vars t) (TypeEnvironment.free_vars env) in
-   S (free, t)
-   ;; *)
+let generalize : TypeEnvironment.t -> Type.t -> Scheme.t =
+  fun env t ->
+  let free = VarSet.diff (Type.free_vars t) (TypeEnvironment.free_vars env) in
+  Scheme (free, t)
+;;
 
 let infer_lt = function
   | Int_lt _ -> return (Substitution.empty, int_typ)
@@ -364,24 +366,24 @@ let infer_lt = function
 
 let rec infer_pattern env = function
   | Wild ->
-    let* fresh_type = make_fresh_var in
-    return (fresh_type, env)
+    let* fresh_var = make_fresh_var in
+    return (fresh_var, env)
   | PConst lt ->
     let* _, t = infer_lt lt in
     return (t, env)
   | PVar (Ident (name, _)) ->
     (* подумать что делать с типом в Ident*)
     let* fresh = make_fresh_var in
-    let scheme = S (VarSet.empty, fresh) in
+    let scheme = Scheme (VarSet.empty, fresh) in
     let env = TypeEnvironment.extend env name scheme in
     return (fresh, env)
   | POption None ->
-    let* fresh_type = make_fresh_var in
-    return (fresh_type, env)
+    let* fresh_var = make_fresh_var in
+    return (fresh_var, env)
   | POption (Some p) -> infer_pattern env p
   | PList [] ->
-    let* fresh_type = make_fresh_var in
-    return (Type_list fresh_type, env)
+    let* fresh_var = make_fresh_var in
+    return (Type_list fresh_var, env)
   | PList (hd :: tl) ->
     let* typ1, env = infer_pattern env hd in
     let* subst_unify, typ_unified =
@@ -453,11 +455,11 @@ let rec infer_expr env = function
       | 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_type = make_fresh_var in
-        return (fresh_type, fresh_type, bool_typ)
+        let* fresh_var = make_fresh_var in
+        return (fresh_var, fresh_var, bool_typ)
       | Binary_cons ->
-        let* fresh_type = make_fresh_var in
-        return (fresh_type, Type_list fresh_type, Type_list fresh_type)
+        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
     (*Format.printf "Checking types: res_typ1 = %a\n" pp_typ (Substitution.apply subst2 typ1);
@@ -492,8 +494,8 @@ let rec infer_expr env = function
     in
     return (subst_result, Type_tuple (typ1, typ2, typs_rest))
   | List [] ->
-    let* fresh_type = make_fresh_var in
-    return (Substitution.empty, Type_list fresh_type)
+    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
@@ -529,10 +531,10 @@ let rec infer_expr env = function
   | Apply (f, arg) ->
     let* subst1, typ1 = infer_expr env f in
     let* subst2, typ2 = infer_expr (TypeEnvironment.apply subst1 env) arg in
-    let* fresh_type = make_fresh_var in
-    let* subst3 = unify (Substitution.apply subst2 typ1) (Arrow (typ2, fresh_type)) in
+    let* fresh_var = make_fresh_var in
+    let* subst3 = unify (Substitution.apply subst2 typ1) (Arrow (typ2, fresh_var)) in
     let* subst_result = Substitution.compose_all [ subst1; subst2; subst3 ] in
-    return (subst_result, Substitution.apply subst_result fresh_type)
+    return (subst_result, Substitution.apply subst_result fresh_var)
   | Lambda (arg, args, e) ->
     let* env, arg_types =
       RList.fold_right
@@ -544,48 +546,91 @@ let rec infer_expr env = function
     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 bind_names =
-     List.map (let_bind :: let_binds) ~f:(fun let_bind ->
-     match let_bind with
-     | Let_bind (Ident (name, _), _, _) -> name)
-     in
-     let* env =
-     List.fold
-     ~init:(return env)
-     ~f:(fun acc name ->
-     let* fresh_type = make_fresh_var in
-     let* acc = acc in
-     return (TypeEnvironment.extend acc name (S (VarSet.empty, fresh_type))))
-     bind_names
-     in
-     x *)
+  | LetIn (Rec, let_bind, let_binds, e) ->
+    let bind_names =
+      List.map (let_bind :: let_binds) ~f:(function Let_bind (Ident (name, _), _, _) ->
+        name)
+    in
+    let fresh_vars =
+      List.init (List.length (let_bind :: let_binds)) ~f:(fun _ -> make_fresh_var)
+    in
+    let* env =
+      List.fold2_exn
+        ~init:(return env)
+        ~f:(fun acc bind_name fresh_var ->
+          let* fresh_var = fresh_var in
+          let* acc = acc in
+          return (TypeEnvironment.extend acc bind_name (Scheme (VarSet.empty, fresh_var))))
+        bind_names
+        fresh_vars
+    in
+    let* env, subst1 =
+      List.fold
+        (let_bind :: let_binds)
+        ~init:(return (env, Substitution.empty))
+        ~f:(fun acc let_bind ->
+          let* env, subst_acc = acc in
+          let* subst, bind_varname, scheme = infer_let_bind env let_bind in
+          let env = TypeEnvironment.extend env bind_varname scheme in
+          let env = TypeEnvironment.apply subst env in
+          let* subst_acc = Substitution.compose subst_acc subst in
+          return (env, subst_acc))
+    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 =
+      List.fold
+        (let_bind :: let_binds)
+        ~init:(return (env, Substitution.empty))
+        ~f:(fun acc let_bind ->
+          let* env, subst_acc = acc in
+          let* subst, bind_varname, scheme = infer_let_bind env let_bind in
+          let env = TypeEnvironment.extend env bind_varname scheme in
+          let env = TypeEnvironment.apply subst env in
+          let* subst_acc = Substitution.compose subst_acc subst in
+          return (env, subst_acc))
+    in
+    let* subst2, typ = infer_expr env e in
+    let* subst_final = Substitution.compose subst1 subst2 in
+    return (subst_final, typ)
   | _ -> fail (`WIP "Expr inference WIP")
-;;
 
-(* and infer_let_bind env fresh_type = function
-   | Let_bind (_, args, e) ->
-   let arg_names =
-   List.map args ~f:(fun arg ->
-   match arg with
-   | Ident (name, _) -> name)
-   in
-   let* env =
-   List.fold
-   ~init:(return env)
-   ~f:(fun acc arg ->
-   let* fresh_type = make_fresh_var in
-   let* acc = acc in
-   return (TypeEnvironment.extend acc arg (S (VarSet.empty, fresh_type))))
-   arg_names
-   in
-   let* subst1, typ1 = infer_expr env e in
-   let* subst2 = unify (Substitution.apply subst1 fresh_type) typ1 in
-   let* subst = Substitution.compose subst1 subst2 in
-   let env = TypeEnvironment.apply subst env in
-   let typ2 = generalize env (Substitution.apply subst fresh_type) in
-   return (subst, typ2)
-   ;; *)
+and infer_let_bind env = function
+  | Let_bind (Ident (bind_varname, _), args, e) ->
+    let fresh_vars = List.init (List.length args) ~f:(fun _ -> make_fresh_var) in
+    let arg_names =
+      List.map args ~f:(fun arg ->
+        match arg with
+        | Ident (name, _) -> name)
+    in
+    let* env =
+      List.fold2_exn
+        ~init:(return env)
+        ~f:(fun acc arg fresh_var ->
+          let* acc = acc in
+          let* fresh_var = fresh_var in
+          return (TypeEnvironment.extend acc arg (Scheme (VarSet.empty, fresh_var))))
+        arg_names
+        fresh_vars
+    in
+    let* subst1, typ1 = infer_expr env e in
+    (* If let_bind is recursive, then bind_varname was already in environment *)
+    let* bind_typevar =
+      match TypeEnvironment.find bind_varname env with
+      | Some (Scheme (_, bind_typevar)) -> return bind_typevar
+      | None -> make_fresh_var
+    in
+    let env =
+      TypeEnvironment.extend env bind_varname (Scheme (VarSet.empty, bind_typevar))
+    in
+    let* subst2 = unify (Substitution.apply subst1 bind_typevar) typ1 in
+    let* subst = Substitution.compose subst1 subst2 in
+    let env = TypeEnvironment.apply subst env in
+    let bind_var_scheme = generalize env (Substitution.apply subst bind_typevar) in
+    return (subst, bind_varname, bind_var_scheme)
+;;
 
 let infer_construction env = function
   | Expr exp ->
diff --git a/FSharpActivePatterns/lib/typedTree.ml b/FSharpActivePatterns/lib/typedTree.ml
index 54ff2528f..26ab398a2 100644
--- a/FSharpActivePatterns/lib/typedTree.ml
+++ b/FSharpActivePatterns/lib/typedTree.ml
@@ -13,9 +13,9 @@ type typ =
   | TOption of typ
 [@@deriving show { with_path = false }]
 
-let arrow_of_types first_types last =
+let arrow_of_types first_types last_type =
   let open Base in
-  List.fold_right first_types ~init:last ~f:(fun left right -> Arrow (left, right))
+  List.fold_right first_types ~init:last_type ~f:(fun left right -> Arrow (left, right))
 ;;
 
 module VarSet = struct
@@ -31,7 +31,7 @@ end
 type binder_set = VarSet.t [@@deriving show { with_path = false }]
 
 (* binder_set here -- list of all type vars in context (?) *)
-type scheme = S of binder_set * typ [@@deriving show { with_path = false }]
+type scheme = Scheme of binder_set * typ [@@deriving show { with_path = false }]
 
 let int_typ = Primitive "int"
 let bool_typ = Primitive "bool"
diff --git a/FSharpActivePatterns/lib/typedTree.mli b/FSharpActivePatterns/lib/typedTree.mli
index 09c2ff54a..d8f8667a1 100644
--- a/FSharpActivePatterns/lib/typedTree.mli
+++ b/FSharpActivePatterns/lib/typedTree.mli
@@ -21,7 +21,7 @@ module VarSet : sig
 end
 
 type binder_set = VarSet.t
-type scheme = S of binder_set * typ [@@deriving show { with_path = false }]
+type scheme = Scheme of binder_set * typ [@@deriving show { with_path = false }]
 
 val int_typ : typ
 val bool_typ : typ
diff --git a/FSharpActivePatterns/lib/typesPp.ml b/FSharpActivePatterns/lib/typesPp.ml
index 8e18b1ef4..59207a761 100644
--- a/FSharpActivePatterns/lib/typesPp.ml
+++ b/FSharpActivePatterns/lib/typesPp.ml
@@ -9,7 +9,10 @@ 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) -> fprintf fmt "(%a) -> %a" helper fst helper snd
+    | 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 "(";

From ffdcdd96f5df8b759aa3dd501eaee837bec9e7ca Mon Sep 17 00:00:00 2001
From: Gleb Nasretdinov <gleb.nasretdinov@proton.me>
Date: Sun, 15 Dec 2024 16:09:13 +0300
Subject: [PATCH 03/15] ref: move duplicated code to functions

Signed-off-by: Gleb Nasretdinov <gleb.nasretdinov@proton.me>
---
 FSharpActivePatterns/lib/inferencer.ml | 70 +++++++++++---------------
 1 file changed, 29 insertions(+), 41 deletions(-)

diff --git a/FSharpActivePatterns/lib/inferencer.ml b/FSharpActivePatterns/lib/inferencer.ml
index d5c24714c..b2ef31783 100644
--- a/FSharpActivePatterns/lib/inferencer.ml
+++ b/FSharpActivePatterns/lib/inferencer.ml
@@ -547,56 +547,44 @@ let rec infer_expr env = function
     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 bind_names =
-      List.map (let_bind :: let_binds) ~f:(function Let_bind (Ident (name, _), _, _) ->
-        name)
-    in
-    let fresh_vars =
-      List.init (List.length (let_bind :: let_binds)) ~f:(fun _ -> make_fresh_var)
-    in
-    let* env =
-      List.fold2_exn
-        ~init:(return env)
-        ~f:(fun acc bind_name fresh_var ->
-          let* fresh_var = fresh_var in
-          let* acc = acc in
-          return (TypeEnvironment.extend acc bind_name (Scheme (VarSet.empty, fresh_var))))
-        bind_names
-        fresh_vars
-    in
-    let* env, subst1 =
-      List.fold
-        (let_bind :: let_binds)
-        ~init:(return (env, Substitution.empty))
-        ~f:(fun acc let_bind ->
-          let* env, subst_acc = acc in
-          let* subst, bind_varname, scheme = infer_let_bind env let_bind in
-          let env = TypeEnvironment.extend env bind_varname scheme in
-          let env = TypeEnvironment.apply subst env in
-          let* subst_acc = Substitution.compose subst_acc subst in
-          return (env, subst_acc))
-    in
+    let* env = extend_env_with_bind_names env (let_bind :: let_binds) in
+    let* env, subst1 = extend_env_with_let_binds env (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)
   | LetIn (Nonrec, let_bind, let_binds, e) ->
-    let* env, subst1 =
-      List.fold
-        (let_bind :: let_binds)
-        ~init:(return (env, Substitution.empty))
-        ~f:(fun acc let_bind ->
-          let* env, subst_acc = acc in
-          let* subst, bind_varname, scheme = infer_let_bind env let_bind in
-          let env = TypeEnvironment.extend env bind_varname scheme in
-          let env = TypeEnvironment.apply subst env in
-          let* subst_acc = Substitution.compose subst_acc subst in
-          return (env, subst_acc))
-    in
+    let* env, subst1 = extend_env_with_let_binds env (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)
   | _ -> fail (`WIP "Expr inference WIP")
 
+and extend_env_with_let_binds env let_binds =
+  List.fold
+    let_binds
+    ~init:(return (env, Substitution.empty))
+    ~f:(fun acc let_bind ->
+      let* env, subst_acc = acc in
+      let* subst, bind_varname, scheme = infer_let_bind env let_bind in
+      let env = TypeEnvironment.extend env bind_varname scheme in
+      let env = TypeEnvironment.apply subst env in
+      let* subst_acc = Substitution.compose subst_acc subst in
+      return (env, subst_acc))
+
+and extend_env_with_bind_names env let_binds =
+  let bind_names =
+    List.map let_binds ~f:(function Let_bind (Ident (name, _), _, _) -> name)
+  in
+  let fresh_vars = List.init (List.length let_binds) ~f:(fun _ -> make_fresh_var) in
+  List.fold2_exn
+    ~init:(return env)
+    ~f:(fun acc bind_name fresh_var ->
+      let* fresh_var = fresh_var in
+      let* acc = acc in
+      return (TypeEnvironment.extend acc bind_name (Scheme (VarSet.empty, fresh_var))))
+    bind_names
+    fresh_vars
+
 and infer_let_bind env = function
   | Let_bind (Ident (bind_varname, _), args, e) ->
     let fresh_vars = List.init (List.length args) ~f:(fun _ -> make_fresh_var) in

From 950aaacbacd68ae72758bed43d9d8282a06398dd Mon Sep 17 00:00:00 2001
From: Gleb Nasretdinov <gleb.nasretdinov@proton.me>
Date: Sun, 15 Dec 2024 17:42:51 +0300
Subject: [PATCH 04/15] ref: move function from mutual recursion definition

Signed-off-by: Gleb Nasretdinov <gleb.nasretdinov@proton.me>
---
 FSharpActivePatterns/lib/inferencer.ml | 29 +++++++++++++-------------
 1 file changed, 15 insertions(+), 14 deletions(-)

diff --git a/FSharpActivePatterns/lib/inferencer.ml b/FSharpActivePatterns/lib/inferencer.ml
index b2ef31783..68898efef 100644
--- a/FSharpActivePatterns/lib/inferencer.ml
+++ b/FSharpActivePatterns/lib/inferencer.ml
@@ -420,6 +420,21 @@ let rec infer_pattern env = function
     return (Type_tuple (typ1, typ2, typs_rest), env)
 ;;
 
+let extend_env_with_bind_names env let_binds =
+  let bind_names =
+    List.map let_binds ~f:(function Let_bind (Ident (name, _), _, _) -> name)
+  in
+  let fresh_vars = List.init (List.length let_binds) ~f:(fun _ -> make_fresh_var) in
+  List.fold2_exn
+    ~init:(return env)
+    ~f:(fun acc bind_name fresh_var ->
+      let* fresh_var = fresh_var in
+      let* acc = acc in
+      return (TypeEnvironment.extend acc bind_name (Scheme (VarSet.empty, fresh_var))))
+    bind_names
+    fresh_vars
+;;
+
 let rec infer_expr env = function
   | Const lt -> infer_lt lt
   | Variable (Ident (varname, _)) ->
@@ -571,20 +586,6 @@ and extend_env_with_let_binds env let_binds =
       let* subst_acc = Substitution.compose subst_acc subst in
       return (env, subst_acc))
 
-and extend_env_with_bind_names env let_binds =
-  let bind_names =
-    List.map let_binds ~f:(function Let_bind (Ident (name, _), _, _) -> name)
-  in
-  let fresh_vars = List.init (List.length let_binds) ~f:(fun _ -> make_fresh_var) in
-  List.fold2_exn
-    ~init:(return env)
-    ~f:(fun acc bind_name fresh_var ->
-      let* fresh_var = fresh_var in
-      let* acc = acc in
-      return (TypeEnvironment.extend acc bind_name (Scheme (VarSet.empty, fresh_var))))
-    bind_names
-    fresh_vars
-
 and infer_let_bind env = function
   | Let_bind (Ident (bind_varname, _), args, e) ->
     let fresh_vars = List.init (List.length args) ~f:(fun _ -> make_fresh_var) in

From 606266073d7736bb3f77831cf09ad3202d1e46ca Mon Sep 17 00:00:00 2001
From: Gleb Nasretdinov <gleb.nasretdinov@proton.me>
Date: Sun, 15 Dec 2024 18:04:03 +0300
Subject: [PATCH 05/15] fix: Let bind inference with arguments

Signed-off-by: Gleb Nasretdinov <gleb.nasretdinov@proton.me>
---
 FSharpActivePatterns/lib/inferencer.ml | 14 ++++++++++----
 1 file changed, 10 insertions(+), 4 deletions(-)

diff --git a/FSharpActivePatterns/lib/inferencer.ml b/FSharpActivePatterns/lib/inferencer.ml
index 68898efef..9382b314e 100644
--- a/FSharpActivePatterns/lib/inferencer.ml
+++ b/FSharpActivePatterns/lib/inferencer.ml
@@ -588,7 +588,13 @@ and extend_env_with_let_binds env let_binds =
 
 and infer_let_bind env = function
   | Let_bind (Ident (bind_varname, _), args, e) ->
-    let fresh_vars = List.init (List.length args) ~f:(fun _ -> make_fresh_var) in
+    let* fresh_vars =
+      (* Hack for get typ list, not typ t list*)
+      List.fold args ~init:(return []) ~f:(fun acc _ ->
+        let* fresh_var = make_fresh_var in
+        let* acc = acc in
+        return (fresh_var :: acc))
+    in
     let arg_names =
       List.map args ~f:(fun arg ->
         match arg with
@@ -599,7 +605,6 @@ and infer_let_bind env = function
         ~init:(return env)
         ~f:(fun acc arg fresh_var ->
           let* acc = acc in
-          let* fresh_var = fresh_var in
           return (TypeEnvironment.extend acc arg (Scheme (VarSet.empty, fresh_var))))
         arg_names
         fresh_vars
@@ -611,13 +616,14 @@ and infer_let_bind env = function
       | Some (Scheme (_, bind_typevar)) -> return bind_typevar
       | None -> make_fresh_var
     in
+    let bind_type = arrow_of_types fresh_vars bind_typevar in
     let env =
-      TypeEnvironment.extend env bind_varname (Scheme (VarSet.empty, bind_typevar))
+      TypeEnvironment.extend env bind_varname (Scheme (VarSet.empty, bind_type))
     in
     let* subst2 = unify (Substitution.apply subst1 bind_typevar) typ1 in
     let* subst = Substitution.compose subst1 subst2 in
     let env = TypeEnvironment.apply subst env in
-    let bind_var_scheme = generalize env (Substitution.apply subst bind_typevar) in
+    let bind_var_scheme = generalize env (Substitution.apply subst bind_type) in
     return (subst, bind_varname, bind_var_scheme)
 ;;
 

From 6f24d1be800d570d5c095e3493957deb6d1a2f1b Mon Sep 17 00:00:00 2001
From: Gleb Nasretdinov <gleb.nasretdinov@proton.me>
Date: Sun, 15 Dec 2024 18:44:20 +0300
Subject: [PATCH 06/15] feat: implement Let statements inference, REPL with
 TypeEnvironment

Signed-off-by: Gleb Nasretdinov <gleb.nasretdinov@proton.me>
---
 FSharpActivePatterns/bin/REPL.ml        | 24 +++++++-----
 FSharpActivePatterns/lib/inferencer.ml  | 49 ++++++++++++++++++++-----
 FSharpActivePatterns/lib/inferencer.mli | 12 +++++-
 3 files changed, 64 insertions(+), 21 deletions(-)

diff --git a/FSharpActivePatterns/bin/REPL.ml b/FSharpActivePatterns/bin/REPL.ml
index 89e6e8c23..1be28108d 100644
--- a/FSharpActivePatterns/bin/REPL.ml
+++ b/FSharpActivePatterns/bin/REPL.ml
@@ -61,31 +61,35 @@ let run_repl dump_parsetree input_file =
     | None -> stdin
     | Some n -> open_in n
   in
-  let rec run_repl_helper run =
+  let rec run_repl_helper run env =
     let open Format in
     match run ic with
     | Fail -> fprintf err_formatter "Error occured\n"
     | Empty ->
       fprintf std_formatter "\n";
       print_flush ();
-      run_repl_helper run
+      run_repl_helper run env
     | End -> ()
     | Result ast ->
-      let result = infer ast in
+      let result = infer ast env in
       (match result with
        | Error err ->
          fprintf err_formatter "Type checking failed: %a\n" pp_error err;
-         print_flush ()
-       | Ok t ->
+         print_flush ();
+         run_repl_helper run env
+       | Ok (env, types) ->
          (match dump_parsetree with
           | true -> print_construction std_formatter ast
           | false ->
-            fprintf std_formatter "- : ";
-            pp_typ std_formatter t);
-         print_flush ());
-      run_repl_helper run
+            List.iter
+              (fun t ->
+                fprintf std_formatter "- : ";
+                pp_typ std_formatter t)
+              types;
+            print_flush ());
+         run_repl_helper run env)
   in
-  run_repl_helper run_single
+  run_repl_helper run_single TypeEnvironment.empty
 ;;
 
 type opts =
diff --git a/FSharpActivePatterns/lib/inferencer.ml b/FSharpActivePatterns/lib/inferencer.ml
index 9382b314e..3e5fab246 100644
--- a/FSharpActivePatterns/lib/inferencer.ml
+++ b/FSharpActivePatterns/lib/inferencer.ml
@@ -297,7 +297,8 @@ module TypeEnvironment : sig
   val extend : t -> string -> scheme -> t
   val apply : Substitution.t -> t -> t
   val empty : t
-  val find : string -> t -> scheme option
+  val find : t -> string -> scheme option
+  val find_exn : t -> string -> scheme
 end = struct
   open Base
 
@@ -313,7 +314,8 @@ end = struct
 
   (* apply given substitution to all elements of environment *)
   let apply subst env = Map.map env ~f:(Scheme.apply subst)
-  let find key env = Map.find env key
+  let find = Map.find
+  let find_exn = Map.find_exn
 
   (* collect all free vars from environment *)
   let free_vars : t -> VarSet.t =
@@ -420,10 +422,12 @@ let rec infer_pattern env = function
     return (Type_tuple (typ1, typ2, typs_rest), env)
 ;;
 
+let extract_names_from_let_binds let_binds =
+  List.map let_binds ~f:(function Let_bind (Ident (name, _), _, _) -> name)
+;;
+
 let extend_env_with_bind_names env let_binds =
-  let bind_names =
-    List.map let_binds ~f:(function Let_bind (Ident (name, _), _, _) -> name)
-  in
+  let bind_names = extract_names_from_let_binds let_binds in
   let fresh_vars = List.init (List.length let_binds) ~f:(fun _ -> make_fresh_var) in
   List.fold2_exn
     ~init:(return env)
@@ -439,7 +443,7 @@ let rec infer_expr env = function
   | Const lt -> infer_lt lt
   | Variable (Ident (varname, _)) ->
     (* подумать что делать с типом Ident*)
-    (match TypeEnvironment.find varname env with
+    (match TypeEnvironment.find env varname with
      | Some s ->
        let* t = instantiate s in
        return (Substitution.empty, t)
@@ -612,7 +616,7 @@ and infer_let_bind env = function
     let* subst1, typ1 = infer_expr env e in
     (* If let_bind is recursive, then bind_varname was already in environment *)
     let* bind_typevar =
-      match TypeEnvironment.find bind_varname env with
+      match TypeEnvironment.find env bind_varname with
       | Some (Scheme (_, bind_typevar)) -> return bind_typevar
       | None -> make_fresh_var
     in
@@ -627,11 +631,36 @@ and infer_let_bind env = function
     return (subst, bind_varname, bind_var_scheme)
 ;;
 
+let infer_statement env = function
+  | Let (Rec, let_bind, let_binds) ->
+    let* env = extend_env_with_bind_names env (let_bind :: let_binds) in
+    let* env, _ = extend_env_with_let_binds env (let_bind :: let_binds) in
+    let bind_names = extract_names_from_let_binds let_binds in
+    let bind_types =
+      List.map bind_names ~f:(fun name ->
+        match TypeEnvironment.find_exn env name with
+        | Scheme (_, typ) -> typ)
+    in
+    return (env, bind_types)
+  | Let (Nonrec, let_bind, let_binds) ->
+    let let_binds = let_bind :: let_binds in
+    let* env, _ = extend_env_with_let_binds env let_binds in
+    let bind_names = extract_names_from_let_binds let_binds in
+    let bind_types =
+      List.map bind_names ~f:(fun name ->
+        match TypeEnvironment.find_exn env name with
+        | Scheme (_, typ) -> typ)
+    in
+    return (env, bind_types)
+;;
+
 let infer_construction env = function
   | Expr exp ->
     let* _, typ = infer_expr env exp in
-    return typ
-  | _ -> fail (`WIP "Statement inference WIP")
+    return (env, [ typ ])
+  | Statement s ->
+    let* env, types = infer_statement env s in
+    return (env, types)
 ;;
 
-let infer c = run (infer_construction TypeEnvironment.empty c)
+let infer c env = run (infer_construction env c)
diff --git a/FSharpActivePatterns/lib/inferencer.mli b/FSharpActivePatterns/lib/inferencer.mli
index 04854645b..3c7b36f36 100644
--- a/FSharpActivePatterns/lib/inferencer.mli
+++ b/FSharpActivePatterns/lib/inferencer.mli
@@ -6,6 +6,12 @@ open Ast
 open TypedTree
 open Format
 
+module TypeEnvironment : sig
+  type t
+
+  val empty : t
+end
+
 type error =
   [ `Occurs_check
   | `Undef_var of string
@@ -14,4 +20,8 @@ type error =
   ]
 
 val pp_error : formatter -> error -> unit
-val infer : construction -> (typ, error) result
+
+val infer
+  :  construction
+  -> TypeEnvironment.t
+  -> (TypeEnvironment.t * typ list, error) result

From af0fb22fc8b742f1b8b92c61dd2753d27fbb4621 Mon Sep 17 00:00:00 2001
From: Gleb Nasretdinov <gleb.nasretdinov@proton.me>
Date: Sun, 15 Dec 2024 18:47:42 +0300
Subject: [PATCH 07/15] ref: remove old comments

Signed-off-by: Gleb Nasretdinov <gleb.nasretdinov@proton.me>
---
 FSharpActivePatterns/lib/inferencer.ml | 2 --
 1 file changed, 2 deletions(-)

diff --git a/FSharpActivePatterns/lib/inferencer.ml b/FSharpActivePatterns/lib/inferencer.ml
index 3e5fab246..c21cb51f1 100644
--- a/FSharpActivePatterns/lib/inferencer.ml
+++ b/FSharpActivePatterns/lib/inferencer.ml
@@ -481,8 +481,6 @@ let rec infer_expr env = function
         return (fresh_var, Type_list fresh_var, Type_list fresh_var)
     in
     let* subst3 = Substitution.unify (Substitution.apply subst2 typ1) e1typ in
-    (*Format.printf "Checking types: res_typ1 = %a\n" pp_typ (Substitution.apply subst2 typ1);
-      Format.printf "Checking types: res_typ2 = %a\n" pp_typ (Substitution.apply subst3 typ2);*)
     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)

From a20330d73be2da1db883352522d857a869242540 Mon Sep 17 00:00:00 2001
From: Gleb Nasretdinov <gleb.nasretdinov@proton.me>
Date: Sun, 15 Dec 2024 19:39:20 +0300
Subject: [PATCH 08/15] fix: inference of Let with shadowing

Signed-off-by: Gleb Nasretdinov <gleb.nasretdinov@proton.me>
---
 FSharpActivePatterns/lib/inferencer.ml | 28 ++++++++++++++++----------
 1 file changed, 17 insertions(+), 11 deletions(-)

diff --git a/FSharpActivePatterns/lib/inferencer.ml b/FSharpActivePatterns/lib/inferencer.ml
index c21cb51f1..cf4b0c9a7 100644
--- a/FSharpActivePatterns/lib/inferencer.ml
+++ b/FSharpActivePatterns/lib/inferencer.ml
@@ -299,6 +299,7 @@ module TypeEnvironment : sig
   val empty : t
   val find : t -> string -> scheme option
   val find_exn : t -> string -> scheme
+  val find_typ_exn : t -> string -> typ
 end = struct
   open Base
 
@@ -317,6 +318,11 @@ end = struct
   let find = Map.find
   let find_exn = Map.find_exn
 
+  let find_typ_exn env key =
+    match find_exn env key with
+    | Scheme (_, 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 ->
@@ -565,30 +571,30 @@ let rec infer_expr env = function
     return (subst, Substitution.apply subst (arrow_of_types arg_types e_type))
   | LetIn (Rec, let_bind, let_binds, e) ->
     let* env = extend_env_with_bind_names env (let_bind :: let_binds) in
-    let* env, subst1 = extend_env_with_let_binds env (let_bind :: let_binds) in
+    let* env, subst1 = extend_env_with_let_binds env Rec (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)
   | LetIn (Nonrec, let_bind, let_binds, e) ->
-    let* env, subst1 = extend_env_with_let_binds env (let_bind :: let_binds) in
+    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)
   | _ -> fail (`WIP "Expr inference WIP")
 
-and extend_env_with_let_binds env let_binds =
+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, bind_varname, scheme = infer_let_bind env let_bind in
+      let* subst, bind_varname, scheme = infer_let_bind env is_rec let_bind in
       let env = TypeEnvironment.extend env bind_varname scheme 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 = function
+and infer_let_bind env is_rec = function
   | Let_bind (Ident (bind_varname, _), args, e) ->
     let* fresh_vars =
       (* Hack for get typ list, not typ t list*)
@@ -612,11 +618,11 @@ and infer_let_bind env = function
         fresh_vars
     in
     let* subst1, typ1 = infer_expr env e in
-    (* If let_bind is recursive, then bind_varname was already in environment *)
+    (* If let_bind is recursive, then bind_varname is already in environment *)
     let* bind_typevar =
-      match TypeEnvironment.find env bind_varname with
-      | Some (Scheme (_, bind_typevar)) -> return bind_typevar
-      | None -> make_fresh_var
+      match is_rec with
+      | Rec -> return (TypeEnvironment.find_typ_exn env bind_varname)
+      | Nonrec -> make_fresh_var
     in
     let bind_type = arrow_of_types fresh_vars bind_typevar in
     let env =
@@ -632,7 +638,7 @@ and infer_let_bind env = function
 let infer_statement env = function
   | Let (Rec, let_bind, let_binds) ->
     let* env = extend_env_with_bind_names env (let_bind :: let_binds) in
-    let* env, _ = extend_env_with_let_binds env (let_bind :: let_binds) in
+    let* env, _ = extend_env_with_let_binds env Rec (let_bind :: let_binds) in
     let bind_names = extract_names_from_let_binds let_binds in
     let bind_types =
       List.map bind_names ~f:(fun name ->
@@ -642,7 +648,7 @@ let infer_statement env = function
     return (env, bind_types)
   | Let (Nonrec, let_bind, let_binds) ->
     let let_binds = let_bind :: let_binds in
-    let* env, _ = extend_env_with_let_binds env let_binds in
+    let* env, _ = extend_env_with_let_binds env Nonrec let_binds in
     let bind_names = extract_names_from_let_binds let_binds in
     let bind_types =
       List.map bind_names ~f:(fun name ->

From 763d9bdc22add3bc6cc77125045e030a65edb849 Mon Sep 17 00:00:00 2001
From: Gleb Nasretdinov <gleb.nasretdinov@proton.me>
Date: Mon, 16 Dec 2024 12:43:20 +0300
Subject: [PATCH 09/15] fix: recursive generalize

Signed-off-by: Gleb Nasretdinov <gleb.nasretdinov@proton.me>
---
 FSharpActivePatterns/lib/inferencer.ml | 59 +++++++++++++++-----------
 1 file changed, 34 insertions(+), 25 deletions(-)

diff --git a/FSharpActivePatterns/lib/inferencer.ml b/FSharpActivePatterns/lib/inferencer.ml
index cf4b0c9a7..ba8a27f83 100644
--- a/FSharpActivePatterns/lib/inferencer.ml
+++ b/FSharpActivePatterns/lib/inferencer.ml
@@ -300,6 +300,7 @@ module TypeEnvironment : sig
   val find : t -> string -> scheme option
   val find_exn : t -> string -> scheme
   val find_typ_exn : t -> string -> typ
+  val remove : t -> string -> t
 end = struct
   open Base
 
@@ -309,8 +310,7 @@ end = struct
   (* 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 remove env key = Map.remove env key *)
+  let remove env key = Map.remove env key
   let empty = Map.empty (module String)
 
   (* apply given substitution to all elements of environment *)
@@ -348,21 +348,26 @@ let make_fresh_var = fresh >>| fun n -> Type_var n
 let instantiate : scheme -> typ R.t =
   fun (Scheme (vars, t)) ->
   VarSet.fold
-    (fun name ty ->
-      let* ty = ty in
+    (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 ty))
+      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 : TypeEnvironment.t -> Type.t -> Scheme.t =
-  fun env t ->
-  let free = VarSet.diff (Type.free_vars t) (TypeEnvironment.free_vars env) in
-  Scheme (free, t)
+let generalize env typ =
+  let free = VarSet.diff (Type.free_vars typ) (TypeEnvironment.free_vars env) in
+  Scheme (free, typ)
+;;
+
+let generalize_rec env typ rec_name =
+  let env = TypeEnvironment.remove env rec_name in
+  let free = VarSet.diff (Type.free_vars typ) (TypeEnvironment.free_vars env) in
+  Scheme (free, typ)
 ;;
 
 let infer_lt = function
@@ -510,11 +515,6 @@ let rec infer_expr env = function
         ~init:(return (Substitution.empty, []))
     in
     let* subst_result = Substitution.compose_all [ subst1; subst2; subst_rest ] in
-    let typ1 = Substitution.apply subst_result typ1 in
-    let typ2 = Substitution.apply subst_result typ2 in
-    let typs_rest =
-      List.map typs_rest ~f:(fun typ -> Substitution.apply subst_result typ)
-    in
     return (subst_result, Type_tuple (typ1, typ2, typs_rest))
   | List [] ->
     let* fresh_var = make_fresh_var in
@@ -555,9 +555,10 @@ let rec infer_expr env = function
     let* subst1, typ1 = infer_expr env f in
     let* subst2, typ2 = infer_expr (TypeEnvironment.apply subst1 env) arg in
     let* fresh_var = make_fresh_var in
-    let* subst3 = unify (Substitution.apply subst2 typ1) (Arrow (typ2, fresh_var)) in
+    let typ1 = Substitution.apply subst2 typ1 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 subst_result fresh_var)
+    return (subst_result, Substitution.apply subst3 fresh_var)
   | Lambda (arg, args, e) ->
     let* env, arg_types =
       RList.fold_right
@@ -570,8 +571,9 @@ let rec infer_expr env = function
     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* env = extend_env_with_bind_names env (let_bind :: let_binds) in
-    let* env, subst1 = extend_env_with_let_binds env Rec (let_bind :: let_binds) in
+    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)
@@ -608,7 +610,7 @@ and infer_let_bind env is_rec = function
         match arg with
         | Ident (name, _) -> name)
     in
-    let* env =
+    let* env_with_args =
       List.fold2_exn
         ~init:(return env)
         ~f:(fun acc arg fresh_var ->
@@ -617,21 +619,28 @@ and infer_let_bind env is_rec = function
         arg_names
         fresh_vars
     in
-    let* subst1, typ1 = infer_expr env e in
-    (* If let_bind is recursive, then bind_varname is already in environment *)
+    let* subst1, typ1 = infer_expr env_with_args e in
+    let bind_type = arrow_of_types fresh_vars typ1 in
+    (* If let_bind is recursive, then bind_varname was already in environment *)
     let* bind_typevar =
       match is_rec with
       | Rec -> return (TypeEnvironment.find_typ_exn env bind_varname)
       | Nonrec -> make_fresh_var
     in
-    let bind_type = arrow_of_types fresh_vars bind_typevar in
     let env =
-      TypeEnvironment.extend env bind_varname (Scheme (VarSet.empty, bind_type))
+      match is_rec with
+      | Rec -> TypeEnvironment.extend env bind_varname (Scheme (VarSet.empty, bind_type))
+      | Nonrec -> env
     in
-    let* subst2 = unify (Substitution.apply subst1 bind_typevar) typ1 in
+    let* subst2 = unify (Substitution.apply subst1 bind_typevar) bind_type in
     let* subst = Substitution.compose subst1 subst2 in
     let env = TypeEnvironment.apply subst env in
-    let bind_var_scheme = generalize env (Substitution.apply subst bind_type) in
+    let bind_type = Substitution.apply subst bind_type in
+    let bind_var_scheme =
+      match is_rec with
+      | Rec -> generalize_rec env bind_type bind_varname
+      | Nonrec -> generalize env bind_type
+    in
     return (subst, bind_varname, bind_var_scheme)
 ;;
 

From 971619246fd58d218f368ad5ca15fd5d729a3c76 Mon Sep 17 00:00:00 2001
From: Gleb Nasretdinov <gleb.nasretdinov@proton.me>
Date: Mon, 16 Dec 2024 13:43:15 +0300
Subject: [PATCH 10/15] fix: REPL now runs with new state

Signed-off-by: Gleb Nasretdinov <gleb.nasretdinov@proton.me>
---
 FSharpActivePatterns/bin/REPL.ml        | 16 ++++++++--------
 FSharpActivePatterns/lib/inferencer.ml  |  6 +++---
 FSharpActivePatterns/lib/inferencer.mli |  3 ++-
 3 files changed, 13 insertions(+), 12 deletions(-)

diff --git a/FSharpActivePatterns/bin/REPL.ml b/FSharpActivePatterns/bin/REPL.ml
index 1be28108d..f8ebe5386 100644
--- a/FSharpActivePatterns/bin/REPL.ml
+++ b/FSharpActivePatterns/bin/REPL.ml
@@ -61,23 +61,23 @@ let run_repl dump_parsetree input_file =
     | None -> stdin
     | Some n -> open_in n
   in
-  let rec run_repl_helper run env =
+  let rec run_repl_helper run env state =
     let open Format in
     match run ic with
     | Fail -> fprintf err_formatter "Error occured\n"
     | Empty ->
       fprintf std_formatter "\n";
       print_flush ();
-      run_repl_helper run env
+      run_repl_helper run env state
     | End -> ()
     | Result ast ->
-      let result = infer ast env in
+      let result = infer ast env state in
       (match result with
-       | Error err ->
+       | new_state, Error err ->
          fprintf err_formatter "Type checking failed: %a\n" pp_error err;
          print_flush ();
-         run_repl_helper run env
-       | Ok (env, types) ->
+         run_repl_helper run env new_state
+       | new_state, Ok (env, types) ->
          (match dump_parsetree with
           | true -> print_construction std_formatter ast
           | false ->
@@ -87,9 +87,9 @@ let run_repl dump_parsetree input_file =
                 pp_typ std_formatter t)
               types;
             print_flush ());
-         run_repl_helper run env)
+         run_repl_helper run env new_state)
   in
-  run_repl_helper run_single TypeEnvironment.empty
+  run_repl_helper run_single TypeEnvironment.empty 0
 ;;
 
 type opts =
diff --git a/FSharpActivePatterns/lib/inferencer.ml b/FSharpActivePatterns/lib/inferencer.ml
index ba8a27f83..bafd5b1bd 100644
--- a/FSharpActivePatterns/lib/inferencer.ml
+++ b/FSharpActivePatterns/lib/inferencer.ml
@@ -44,7 +44,7 @@ module R : sig
   end
 
   val fresh : int t
-  val run : 'a t -> ('a, error) Result.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
@@ -112,7 +112,7 @@ end = struct
 
   (* takes current state, returns state + 1 *)
   let fresh : int t = fun last -> last + 1, Result.Ok last
-  let run m = snd (m 0)
+  let run m state = m state
 end
 
 type fresh = int
@@ -676,4 +676,4 @@ let infer_construction env = function
     return (env, types)
 ;;
 
-let infer c env = run (infer_construction env c)
+let infer c env state = run (infer_construction env c) state
diff --git a/FSharpActivePatterns/lib/inferencer.mli b/FSharpActivePatterns/lib/inferencer.mli
index 3c7b36f36..3ac24e5bf 100644
--- a/FSharpActivePatterns/lib/inferencer.mli
+++ b/FSharpActivePatterns/lib/inferencer.mli
@@ -24,4 +24,5 @@ val pp_error : formatter -> error -> unit
 val infer
   :  construction
   -> TypeEnvironment.t
-  -> (TypeEnvironment.t * typ list, error) result
+  -> int
+  -> int * (TypeEnvironment.t * typ list, error) result

From aff93bb9f7f6a1e5b5d983d27d19dfaa6ef6c201 Mon Sep 17 00:00:00 2001
From: Gleb Nasretdinov <gleb.nasretdinov@proton.me>
Date: Mon, 16 Dec 2024 14:09:59 +0300
Subject: [PATCH 11/15] fix: extend env in let rec

Signed-off-by: Gleb Nasretdinov <gleb.nasretdinov@proton.me>
---
 FSharpActivePatterns/lib/inferencer.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/FSharpActivePatterns/lib/inferencer.ml b/FSharpActivePatterns/lib/inferencer.ml
index bafd5b1bd..a012b12f5 100644
--- a/FSharpActivePatterns/lib/inferencer.ml
+++ b/FSharpActivePatterns/lib/inferencer.ml
@@ -646,8 +646,9 @@ and infer_let_bind env is_rec = function
 
 let infer_statement env = function
   | Let (Rec, let_bind, let_binds) ->
-    let* env = extend_env_with_bind_names env (let_bind :: let_binds) in
-    let* env, _ = extend_env_with_let_binds env Rec (let_bind :: let_binds) in
+    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_names_from_let_binds let_binds in
     let bind_types =
       List.map bind_names ~f:(fun name ->

From 4324824184c43d120b8b404a998e222201411d5d Mon Sep 17 00:00:00 2001
From: Gleb Nasretdinov <gleb.nasretdinov@proton.me>
Date: Mon, 16 Dec 2024 16:17:08 +0300
Subject: [PATCH 12/15] fix: apply parser

Signed-off-by: Gleb Nasretdinov <gleb.nasretdinov@proton.me>
---
 FSharpActivePatterns/lib/parser.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/FSharpActivePatterns/lib/parser.ml b/FSharpActivePatterns/lib/parser.ml
index a85b8706a..35740d110 100644
--- a/FSharpActivePatterns/lib/parser.ml
+++ b/FSharpActivePatterns/lib/parser.ml
@@ -242,7 +242,7 @@ let p_let p_expr =
   return (Let (rec_flag, Let_bind (name, args, body), let_bind_list))
 ;;
 
-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)

From 6323cd6af7c2773d302042f34304845df4d54d9c Mon Sep 17 00:00:00 2001
From: Gleb Nasretdinov <gleb.nasretdinov@proton.me>
Date: Mon, 16 Dec 2024 17:04:19 +0300
Subject: [PATCH 13/15] feat: implement match inference

Signed-off-by: Gleb Nasretdinov <gleb.nasretdinov@proton.me>
---
 FSharpActivePatterns/lib/inferencer.ml | 20 +++++++++++++++++++-
 1 file changed, 19 insertions(+), 1 deletion(-)

diff --git a/FSharpActivePatterns/lib/inferencer.ml b/FSharpActivePatterns/lib/inferencer.ml
index a012b12f5..ee1419735 100644
--- a/FSharpActivePatterns/lib/inferencer.ml
+++ b/FSharpActivePatterns/lib/inferencer.ml
@@ -582,7 +582,25 @@ let rec infer_expr env = function
     let* subst2, typ = infer_expr env e in
     let* subst_final = Substitution.compose subst1 subst2 in
     return (subst_final, typ)
-  | _ -> fail (`WIP "Expr inference WIP")
+  | Match (e, p1, e1, rest) ->
+    let* subst_init, match_type = infer_expr env e in
+    let env = TypeEnvironment.apply subst_init env in
+    let* fresh_typevar = make_fresh_var in
+    let* subst, typ =
+      List.fold
+        ((p1, e1) :: rest)
+        ~init:(return (subst_init, fresh_typevar))
+        ~f:(fun acc (pat, expr) ->
+          let* subst1, return_type = acc in
+          let* pat, env = infer_pattern env pat in
+          let* subst2 = unify match_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, typ)
 
 and extend_env_with_let_binds env is_rec let_binds =
   List.fold

From a8908e2bac0b7fbce43f7178b46ea03247024b53 Mon Sep 17 00:00:00 2001
From: Gleb Nasretdinov <gleb.nasretdinov@proton.me>
Date: Mon, 16 Dec 2024 17:21:46 +0300
Subject: [PATCH 14/15] fix: let bind inference

Signed-off-by: Gleb Nasretdinov <gleb.nasretdinov@proton.me>
---
 FSharpActivePatterns/lib/inferencer.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/FSharpActivePatterns/lib/inferencer.ml b/FSharpActivePatterns/lib/inferencer.ml
index ee1419735..631cdda6a 100644
--- a/FSharpActivePatterns/lib/inferencer.ml
+++ b/FSharpActivePatterns/lib/inferencer.ml
@@ -638,7 +638,7 @@ and infer_let_bind env is_rec = function
         fresh_vars
     in
     let* subst1, typ1 = infer_expr env_with_args e in
-    let bind_type = arrow_of_types fresh_vars typ1 in
+    let bind_type = Substitution.apply subst1 (arrow_of_types fresh_vars typ1) in
     (* If let_bind is recursive, then bind_varname was already in environment *)
     let* bind_typevar =
       match is_rec with

From f793c5f084875f8d60c85ff3c83153b184456652 Mon Sep 17 00:00:00 2001
From: Gleb Nasretdinov <gleb.nasretdinov@proton.me>
Date: Mon, 16 Dec 2024 17:49:58 +0300
Subject: [PATCH 15/15] ref: lint and fmt

Signed-off-by: Gleb Nasretdinov <gleb.nasretdinov@proton.me>
---
 FSharpActivePatterns/lib/inferencer.ml | 6 +-----
 FSharpActivePatterns/lib/parser.ml     | 4 +++-
 2 files changed, 4 insertions(+), 6 deletions(-)

diff --git a/FSharpActivePatterns/lib/inferencer.ml b/FSharpActivePatterns/lib/inferencer.ml
index 631cdda6a..80f89e2b3 100644
--- a/FSharpActivePatterns/lib/inferencer.ml
+++ b/FSharpActivePatterns/lib/inferencer.ml
@@ -623,11 +623,7 @@ and infer_let_bind env is_rec = function
         let* acc = acc in
         return (fresh_var :: acc))
     in
-    let arg_names =
-      List.map args ~f:(fun arg ->
-        match arg with
-        | Ident (name, _) -> name)
-    in
+    let arg_names = List.map args ~f:(function Ident (name, _) -> name) in
     let* env_with_args =
       List.fold2_exn
         ~init:(return env)
diff --git a/FSharpActivePatterns/lib/parser.ml b/FSharpActivePatterns/lib/parser.ml
index 35740d110..6b7a84491 100644
--- a/FSharpActivePatterns/lib/parser.ml
+++ b/FSharpActivePatterns/lib/parser.ml
@@ -242,7 +242,9 @@ let p_let p_expr =
   return (Let (rec_flag, Let_bind (name, args, body), let_bind_list))
 ;;
 
-let p_apply p_expr = chainl1 (p_expr <* peek_sep1) (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)