diff --git a/src/passes/3-self_ast_simplified/helpers.ml b/src/passes/3-self_ast_simplified/helpers.ml
index 70a130742..101f8d9ab 100644
--- a/src/passes/3-self_ast_simplified/helpers.ml
+++ b/src/passes/3-self_ast_simplified/helpers.ml
@@ -56,6 +56,9 @@ let rec fold_expression : 'a folder -> 'a -> expression -> 'a result = fun f ini
       let%bind res = self res let_result in
       ok res
     )
+  | E_recursive { lambda={result=e;_}; _} ->
+      let%bind res = self init' e in
+      ok res
 
 and fold_cases : 'a folder -> 'a -> matching_expr -> 'a result = fun f init m ->
   match m with
@@ -156,6 +159,10 @@ let rec map_expression : exp_mapper -> expression -> expression result = fun f e
       let%bind result = self result in
       return @@ E_lambda { binder ; input_type ; output_type ; result }
     )
+  | E_recursive { fun_name; fun_type; lambda} ->
+      let%bind result = self lambda.result in
+      let lambda = {lambda with result} in
+      return @@ E_recursive { fun_name; fun_type; lambda}
   | E_constant c -> (
       let%bind args = bind_map_list self c.arguments in
       return @@ E_constant {c with arguments=args}
@@ -295,6 +302,10 @@ let rec fold_map_expression : 'a fold_mapper -> 'a -> expression -> ('a * expres
       let%bind (res,result) = self init' result in
       ok ( res, return @@ E_lambda { binder ; input_type ; output_type ; result })
     )
+  | E_recursive { fun_name; fun_type; lambda} ->
+      let%bind (res, result) = self init' lambda.result in
+      let lambda = {lambda with result} in
+      ok ( res, return @@ E_recursive { fun_name; fun_type; lambda})
   | E_constant c -> (
       let%bind (res,args) = bind_fold_map_list self init' c.arguments in
       ok (res, return @@ E_constant {c with arguments=args})
diff --git a/src/passes/4-typer-new/solver.ml b/src/passes/4-typer-new/solver.ml
index 198cba936..aad418cb5 100644
--- a/src/passes/4-typer-new/solver.ml
+++ b/src/passes/4-typer-new/solver.ml
@@ -291,6 +291,14 @@ module Wrap = struct
         C_equation (result' , P_variable whole_expr)
       ] @ rhs_tv_opt', whole_expr
 
+  let recursive : T.type_expression -> (constraints * T.type_variable) =
+    fun fun_type ->
+      let fun_type = type_expression_to_type_value fun_type in
+      let whole_expr = Core.fresh_type_variable () in
+      O.[
+        C_equation (fun_type, P_variable whole_expr)
+        ], whole_expr
+
   let assign : T.type_expression -> T.type_expression -> (constraints * T.type_variable) =
     fun v e ->
       let v' = type_expression_to_type_value v in
diff --git a/src/passes/4-typer-new/typer.ml b/src/passes/4-typer-new/typer.ml
index 0ca9f8ef8..decd197fc 100644
--- a/src/passes/4-typer-new/typer.ml
+++ b/src/passes/4-typer-new/typer.ml
@@ -797,26 +797,16 @@ and type_expression : environment -> Solver.state -> ?tv_opt:O.type_expression -
   (* | _ -> ( … ) *)
 
 
-  | E_lambda {
-      binder ;
-      input_type ;
-      output_type ;
-      result ;
-    } -> (
-      let%bind input_type' = bind_map_option (evaluate_type e) input_type in
-      let%bind output_type' = bind_map_option (evaluate_type e) output_type in
-
-      let fresh : O.type_expression = t_variable (Wrap.fresh_binder ()) () in
-      let binder = fst binder in 
-      let e' = Environment.add_ez_binder (binder) fresh e in
-
-      let%bind (result , state') = type_expression e' state result in
-      let () = Printf.printf "this does not make use of the typed body, this code sounds buggy." in
-      let wrapped = Wrap.lambda fresh input_type' output_type' in
-      return_wrapped
-        (E_lambda {binder = binder; result}) (* TODO: is the type of the entire lambda enough to access the input_type=fresh; ? *)
+  | E_lambda lambda -> 
+    let%bind (lambda,state',wrapped) = type_lambda e state lambda in
+    return_wrapped (E_lambda lambda) (* TODO: is the type of the entire lambda enough to access the input_type=fresh; ? *)
         state' wrapped
-    )
+  | E_recursive {fun_name;fun_type;lambda} ->
+    let%bind fun_type = evaluate_type e fun_type in
+    let e = Environment.add_ez_binder fun_name fun_type e in
+    let%bind (lambda,state,_) = type_lambda e state lambda in
+    let wrapped = Wrap.recursive fun_type in
+    return_wrapped (E_recursive {fun_name;fun_type;lambda}) state wrapped
 
   | E_constant {cons_name=name; arguments=lst} ->
     let () = ignore (name , lst) in
@@ -838,7 +828,22 @@ and type_expression : environment -> Solver.state -> ?tv_opt:O.type_expression -
         type_constant name tv_lst tv_opt ae.location in
       return (E_constant (name' , lst')) tv
     *)
+and type_lambda e state {
+      binder ;
+      input_type ;
+      output_type ;
+      result ;
+    } =
+      let%bind input_type' = bind_map_option (evaluate_type e) input_type in
+      let%bind output_type' = bind_map_option (evaluate_type e) output_type in
 
+      let fresh : O.type_expression = t_variable (Solver.Wrap.fresh_binder ()) () in
+      let e' = Environment.add_ez_binder (binder) fresh e in
+
+      let%bind (result , state') = type_expression e' state result in
+      let () = Printf.printf "this does not make use of the typed body, this code sounds buggy." in
+      let wrapped = Solver.Wrap.lambda fresh input_type' output_type' in
+      ok (({binder;result}:O.lambda),state',wrapped)
 (* Advanced *)
 
 and type_constant (name:I.constant') (lst:O.type_expression list) (tv_opt:O.type_expression option) : (O.constant' * O.type_expression) result =
@@ -1040,12 +1045,10 @@ let rec untype_expression (e:O.expression) : (I.expression) result =
       let%bind f' = untype_expression expr1 in
       let%bind arg' = untype_expression expr2 in
       return (e_application f' arg')
-  | E_lambda {binder; result} -> (
-      let%bind io = get_t_function e.type_expression in
-      let%bind (input_type , output_type) = bind_map_pair untype_type_value io in
-      let%bind result = untype_expression result in
-      return (e_lambda (binder) (Some input_type) (Some output_type) result)
-    )
+  | E_lambda lambda ->
+      let%bind lambda = untype_lambda e.type_expression lambda in
+      let {binder;input_type;output_type;result} = lambda in
+      return (e_lambda (binder) (input_type) (output_type) result)
   | E_constructor {constructor; element} ->
       let%bind p' = untype_expression element in
       let Constructor n = constructor in
@@ -1092,6 +1095,16 @@ let rec untype_expression (e:O.expression) : (I.expression) result =
     let%bind rhs = untype_expression rhs in
     let%bind result = untype_expression let_result in
     return (e_let_in (let_binder , (Some tv)) false inline rhs result)
+  | E_recursive {fun_name; fun_type; lambda} ->
+      let%bind lambda = untype_lambda fun_type lambda in
+      let%bind fun_type = untype_type_expression fun_type in
+      return @@ e_recursive fun_name fun_type lambda
+
+and untype_lambda ty {binder; result} : I.lambda result =
+      let%bind io = get_t_function ty in
+      let%bind (input_type , output_type) = bind_map_pair untype_type_value io in
+      let%bind result = untype_expression result in
+      ok ({binder;input_type = Some input_type; output_type = Some output_type; result}: I.lambda)
 
 (*
   Tranform a Ast_typed matching into an ast_simplified matching
diff --git a/src/passes/4-typer-old/typer.ml b/src/passes/4-typer-old/typer.ml
index eec5d3a49..448f7be08 100644
--- a/src/passes/4-typer-old/typer.ml
+++ b/src/passes/4-typer-old/typer.ml
@@ -613,45 +613,12 @@ and type_expression' : environment -> ?tv_opt:O.type_expression -> I.expression
         ok (t_big_map key_type value_type ())
       in
       return (E_big_map lst') tv
-  | E_lambda {
-      binder ;
-      input_type ;
-      output_type ;
-      result ;
-    } -> (
-      let%bind input_type =
-        let%bind input_type =
-          (* Hack to take care of let_in introduced by `simplify/cameligo.ml` in ECase's hack *)
-          let default_action e () = fail @@ (needs_annotation e "the returned value") in
-          match input_type with
-          | Some ty -> ok ty
-          | None -> (
-              match result.expression_content with
-              | I.E_let_in li -> (
-                  match li.rhs.expression_content with
-                  | I.E_variable name when name = (fst binder) -> (
-                      match snd li.let_binder with
-                      | Some ty -> ok ty
-                      | None -> default_action li.rhs ()
-                    )
-                  | _ -> default_action li.rhs ()
-                )
-              | _ -> default_action result ()
-            )
-        in
-        evaluate_type e input_type in
-      let%bind output_type =
-        bind_map_option (evaluate_type e) output_type
-      in
-      let binder = fst binder in
-      let e' = Environment.add_ez_binder binder input_type e in
-      let%bind body = type_expression' ?tv_opt:output_type e' result in
-      let output_type = body.type_expression in
-      return (E_lambda {binder; result=body}) (t_function input_type output_type ())
-    )
+  | E_lambda lambda -> 
+   let%bind (lambda, lambda_type) = type_lambda e lambda in
+   return (E_lambda lambda ) lambda_type
   | E_constant {cons_name=( C_LIST_FOLD | C_MAP_FOLD | C_SET_FOLD) as opname ;
                 arguments=[
-                    ( { expression_content = (I.E_lambda { binder = (lname, None) ;
+                    ( { expression_content = (I.E_lambda { binder = lname ;
                                                    input_type = None ; 
                                                    output_type = None ; 
                                                    result }) ;
@@ -683,7 +650,7 @@ and type_expression' : environment -> ?tv_opt:O.type_expression -> I.expression
       return (E_constant {cons_name=opname';arguments=lst'}) tv
   | E_constant {cons_name=C_FOLD_WHILE as opname;
                 arguments = [
-                    ( { expression_content = (I.E_lambda { binder = (lname, None) ;
+                    ( { expression_content = (I.E_lambda { binder = lname ;
                                                    input_type = None ; 
                                                    output_type = None ; 
                                                    result }) ;
@@ -773,6 +740,11 @@ and type_expression' : environment -> ?tv_opt:O.type_expression -> I.expression
     let e' = Environment.add_ez_declaration (let_binder) rhs e in
     let%bind let_result = type_expression' e' let_result in
     return (E_let_in {let_binder; rhs; let_result; inline}) let_result.type_expression
+  | E_recursive {fun_name; fun_type; lambda} ->
+    let%bind fun_type = evaluate_type e fun_type in
+    let e' = Environment.add_ez_binder fun_name fun_type e in
+    let%bind (lambda,_) = type_lambda e' lambda in
+    return (E_recursive {fun_name;fun_type;lambda}) fun_type
   | E_ascription {anno_expr; type_annotation} ->
     let%bind tv = evaluate_type e type_annotation in
     let%bind expr' = type_expression' ~tv_opt:tv e anno_expr in
@@ -788,6 +760,42 @@ and type_expression' : environment -> ?tv_opt:O.type_expression -> I.expression
       | Some tv' -> O.assert_type_expression_eq (tv' , type_annotation) in
     ok {expr' with type_expression=type_annotation}
 
+and type_lambda e {
+      binder ;
+      input_type ;
+      output_type ;
+      result ;
+    } = 
+      let%bind input_type =
+        let%bind input_type =
+          (* Hack to take care of let_in introduced by `simplify/cameligo.ml` in ECase's hack *)
+          let default_action e () = fail @@ (needs_annotation e "the returned value") in
+          match input_type with
+          | Some ty -> ok ty
+          | None -> (
+              match result.expression_content with
+              | I.E_let_in li -> (
+                  match li.rhs.expression_content with
+                  | I.E_variable name when name = (binder) -> (
+                      match snd li.let_binder with
+                      | Some ty -> ok ty
+                      | None -> default_action li.rhs ()
+                    )
+                  | _ -> default_action li.rhs ()
+                )
+              | _ -> default_action result ()
+            )
+        in
+        evaluate_type e input_type in
+      let%bind output_type =
+        bind_map_option (evaluate_type e) output_type
+      in
+      let e' = Environment.add_ez_binder binder input_type e in
+      let%bind body = type_expression' ?tv_opt:output_type e' result in
+      let output_type = body.type_expression in
+      ok (({binder; result=body}:O.lambda),(t_function input_type output_type ()))
+
+
 
 and type_constant (name:I.constant') (lst:O.type_expression list) (tv_opt:O.type_expression option) : (O.constant' * O.type_expression) result =
   let%bind typer = Operators.Typer.constant_typers name in
@@ -820,9 +828,11 @@ let untype_literal (l:O.literal) : I.literal result =
   | Literal_operation s -> ok (Literal_operation s)
 
 let rec untype_expression (e:O.expression) : (I.expression) result =
+  untype_expression_content e.type_expression e.expression_content
+  and untype_expression_content ty (ec:O.expression_content) : (I.expression) result =
   let open I in
   let return e = ok e in
-  match e.expression_content with
+  match ec with
   | E_literal l ->
       let%bind l = untype_literal l in
       return (e_literal l)
@@ -836,7 +846,7 @@ let rec untype_expression (e:O.expression) : (I.expression) result =
       let%bind arg' = untype_expression expr2 in
       return (e_application f' arg')
   | E_lambda {binder ; result} -> (
-      let%bind io = get_t_function e.type_expression in
+      let%bind io = get_t_function ty in
       let%bind (input_type , output_type) = bind_map_pair untype_type_expression io in
       let%bind result = untype_expression result in
       return (e_lambda (binder) (Some input_type) (Some output_type) result)
@@ -883,7 +893,12 @@ let rec untype_expression (e:O.expression) : (I.expression) result =
       let%bind tv = untype_type_expression rhs.type_expression in
       let%bind rhs = untype_expression rhs in
       let%bind result = untype_expression let_result in
-      return (I.e_let_in (let_binder , (Some tv)) false inline rhs result)
+      return (e_let_in (let_binder , (Some tv)) false inline rhs result)
+  | E_recursive {fun_name;fun_type; lambda} ->
+      let%bind fun_type = untype_type_expression fun_type in
+      let%bind unty_expr= untype_expression_content ty @@ E_lambda lambda in
+      let lambda = match unty_expr.expression_content with I.E_lambda l -> l | _ -> failwith "impossible case" in
+      return @@ e_recursive fun_name fun_type lambda
 
 and untype_matching : (O.expression -> I.expression result) -> O.matching_expr -> I.matching_expr result = fun f m ->
   let open I in
diff --git a/src/passes/6-interpreter/interpreter.ml b/src/passes/6-interpreter/interpreter.ml
index ed9f6d6d3..3ef211f83 100644
--- a/src/passes/6-interpreter/interpreter.ml
+++ b/src/passes/6-interpreter/interpreter.ml
@@ -371,7 +371,7 @@ and eval : Ast_typed.expression -> env -> value result
       | _ -> simple_fail "not yet supported case"
         (* ((ctor,name),body) *)
     )
-    | E_look_up _ ->
+    | E_look_up _ | E_recursive _ ->
       let serr = Format.asprintf "Unsupported construct :\n %a\n" Ast_typed.PP.expression term in
       simple_fail serr
 
diff --git a/src/passes/6-transpiler/transpiler.ml b/src/passes/6-transpiler/transpiler.ml
index 8911b76fa..d3dd96b10 100644
--- a/src/passes/6-transpiler/transpiler.ml
+++ b/src/passes/6-transpiler/transpiler.ml
@@ -379,6 +379,8 @@ and transpile_annotated_expression (ae:AST.expression) : expression result =
   | E_lambda l ->
     let%bind io = AST.get_t_function ae.type_expression in
     transpile_lambda l io
+  | E_recursive r ->
+    transpile_recursive r
   | E_list lst -> (
       let%bind t =
         trace_strong (corner_case ~loc:__LOC__ "not a list") @@
@@ -518,6 +520,10 @@ and transpile_lambda l (input_type , output_type) =
   let closure = E_closure { binder; body = result'} in
   ok @@ Combinators.Expression.make_tpl (closure , tv)
 
+and transpile_recursive {fun_name; fun_type; lambda} =
+  let closure = E_closure { binder=fun_name; body} in
+  ok @@ Combinators.Expression.make closure fun_type
+
 let transpile_declaration env (d:AST.declaration) : toplevel_statement result =
   match d with
   | Declaration_constant (name,expression, inline, _) ->
diff --git a/src/stages/ast_simplified/PP.ml b/src/stages/ast_simplified/PP.ml
index f5c2283b0..f27d9ed70 100644
--- a/src/stages/ast_simplified/PP.ml
+++ b/src/stages/ast_simplified/PP.ml
@@ -11,7 +11,9 @@ let expression_variable ppf (ev : expression_variable) : unit =
 
 
 let rec expression ppf (e : expression) =
-  match e.expression_content with
+  expression_content ppf e.expression_content
+and expression_content ppf (ec : expression_content) =
+  match ec with
   | E_literal l ->
       literal ppf l
   | E_variable n ->
@@ -40,16 +42,23 @@ let rec expression ppf (e : expression) =
   | E_look_up (ds, ind) ->
       fprintf ppf "(%a)[%a]" expression ds expression ind
   | E_lambda {binder; input_type; output_type; result} ->
-      fprintf ppf "lambda (%a:%a) : %a return %a" option_type_name binder
+      fprintf ppf "lambda (%a:%a) : %a return %a" 
+        expression_variable binder
         (PP_helpers.option type_expression)
         input_type
         (PP_helpers.option type_expression)
         output_type expression result
   | E_matching {matchee; cases; _} ->
-      fprintf ppf "match %a with %a" expression matchee (matching expression)
+      fprintf ppf "match %a with %a"
+        expression matchee (matching expression)
         cases
   | E_let_in { let_binder ; mut; rhs ; let_result; inline } ->    
-    fprintf ppf "let %a%a = %a%a in %a" option_mut mut option_type_name let_binder expression rhs option_inline inline expression let_result
+      fprintf ppf "let %a%a = %a%a in %a" option_mut mut option_type_name let_binder expression rhs option_inline inline expression let_result
+  | E_recursive { fun_name; fun_type; lambda} ->
+      fprintf ppf "rec (%a:%a => %a )" 
+        expression_variable fun_name 
+        type_expression fun_type
+        expression_content (E_lambda lambda)
   | E_skip ->
       fprintf ppf "skip"
   | E_ascription {anno_expr; type_annotation} ->
diff --git a/src/stages/ast_simplified/combinators.ml b/src/stages/ast_simplified/combinators.ml
index 21c9ee183..24b292c4f 100644
--- a/src/stages/ast_simplified/combinators.ml
+++ b/src/stages/ast_simplified/combinators.ml
@@ -178,11 +178,12 @@ let e_lambda ?loc (binder : expression_variable)
     (result : expression)
   : expression =
   location_wrap ?loc @@ E_lambda {
-    binder = (binder , input_type) ;
+    binder = binder;
     input_type = input_type ;
     output_type = output_type ;
     result ;
   }
+let e_recursive ?loc fun_name fun_type lambda = location_wrap ?loc @@ E_recursive {fun_name; fun_type; lambda}
 
 
 let e_assign_with_let ?loc var access_path expr = 
diff --git a/src/stages/ast_simplified/combinators.mli b/src/stages/ast_simplified/combinators.mli
index 37e32bb5f..5dc0af74c 100644
--- a/src/stages/ast_simplified/combinators.mli
+++ b/src/stages/ast_simplified/combinators.mli
@@ -106,6 +106,7 @@ val e_typed_big_map : ?loc:Location.t -> ( expression * expression ) list  -> ty
 val e_typed_set : ?loc:Location.t -> expression list -> type_expression -> expression
 
 val e_lambda : ?loc:Location.t -> expression_variable -> type_expression option -> type_expression option -> expression -> expression
+val e_recursive : ?loc:Location.t -> expression_variable -> type_expression -> lambda -> expression
 val e_record : ?loc:Location.t -> expr Map.String.t -> expression
 val e_update : ?loc:Location.t -> expression -> string -> expression -> expression
 val e_assign_with_let : ?loc:Location.t -> string -> string list -> expression -> ((expression_variable*type_expression option)*bool*expression*bool)
diff --git a/src/stages/ast_simplified/misc.ml b/src/stages/ast_simplified/misc.ml
index bb309048e..f2094d3ca 100644
--- a/src/stages/ast_simplified/misc.ml
+++ b/src/stages/ast_simplified/misc.ml
@@ -182,7 +182,7 @@ let rec assert_value_eq (a, b: (expression * expression )) : unit result =
   | (_a' , E_ascription b) -> assert_value_eq (a , b.anno_expr)
   | (E_variable _, _) | (E_lambda _, _)
   | (E_application _, _) | (E_let_in _, _)
-  | (E_record_accessor _, _)
+  | (E_recursive _,_) | (E_record_accessor _, _)
   | (E_look_up _, _) | (E_matching _, _)
   | (E_skip, _) -> simple_fail "comparing not a value"
 
diff --git a/src/stages/ast_simplified/types.ml b/src/stages/ast_simplified/types.ml
index de0de0934..696dbd028 100644
--- a/src/stages/ast_simplified/types.ml
+++ b/src/stages/ast_simplified/types.ml
@@ -35,6 +35,7 @@ and expression_content =
   | E_application of application
   | E_lambda of lambda
   | E_let_in of let_in
+  | E_recursive of recursive
   | E_skip
   (* Variant *)
   | E_constructor of constructor (* For user defined constructors *)
@@ -60,7 +61,7 @@ and constant =
 and application = {expr1: expression; expr2: expression}
 
 and lambda =
-  { binder: expression_variable * type_expression option
+  { binder: expression_variable 
   ; input_type: type_expression option
   ; output_type: type_expression option
   ; result: expression }
@@ -72,6 +73,12 @@ and let_in =
   ; let_result: expression
   ; inline: bool }
 
+and recursive = {
+  fun_name :  expression_variable;
+  fun_type : type_expression;
+  lambda : lambda;
+}
+
 and constructor = {constructor: constructor'; element: expression}
 
 and accessor = {expr: expression; label: label}
diff --git a/src/stages/ast_typed/PP.ml b/src/stages/ast_typed/PP.ml
index a0f15514b..aed4648c5 100644
--- a/src/stages/ast_typed/PP.ml
+++ b/src/stages/ast_typed/PP.ml
@@ -11,7 +11,10 @@ let expression_variable ppf (ev : expression_variable) : unit =
 
 
 let rec expression ppf (e : expression) =
-  match e.expression_content with
+  expression_content ppf e.expression_content
+
+and expression_content ppf (ec: expression_content) =
+  match ec with
   | E_literal l ->
       literal ppf l
   | E_variable n ->
@@ -47,6 +50,11 @@ let rec expression ppf (e : expression) =
   | E_let_in {let_binder; rhs; let_result; inline} ->
       fprintf ppf "let %a = %a%a in %a" expression_variable let_binder expression
         rhs option_inline inline expression let_result
+  | E_recursive { fun_name;fun_type; lambda} ->
+      fprintf ppf "rec (%a:%a => %a )" 
+        expression_variable fun_name 
+        type_expression fun_type
+        expression_content (E_lambda lambda)
 
 and assoc_expression ppf : expr * expr -> unit =
  fun (a, b) -> fprintf ppf "%a -> %a" expression a expression b
diff --git a/src/stages/ast_typed/misc.ml b/src/stages/ast_typed/misc.ml
index 9395c511a..20a778f9c 100644
--- a/src/stages/ast_typed/misc.ml
+++ b/src/stages/ast_typed/misc.ml
@@ -221,6 +221,9 @@ module Free_variables = struct
       union
         (expression b' let_result)
         (self rhs)
+    | E_recursive {fun_name;lambda;_} ->
+      let b' = union (singleton fun_name) b in
+      expression_content b' @@ E_lambda lambda
 
   and lambda : bindings -> lambda -> bindings = fun b l ->
     let b' = union (singleton l.binder) b in
@@ -529,7 +532,7 @@ let rec assert_value_eq (a, b: (expression*expression)) : unit result =
   | E_set _, _ ->
       fail @@ different_values_because_different_types "set vs. non-set" a b
   | (E_literal _, _) | (E_variable _, _) | (E_application _, _)
-  | (E_lambda _, _) | (E_let_in _, _)
+  | (E_lambda _, _) | (E_let_in _, _) | (E_recursive _, _)
   | (E_record_accessor _, _) | (E_record_update _,_)
   | (E_look_up _, _) | (E_matching _, _)
   -> fail @@ error_uncomparable_values "can't compare sequences nor loops" a b
diff --git a/src/stages/ast_typed/misc_smart.ml b/src/stages/ast_typed/misc_smart.ml
index ebe25ace2..414f01670 100644
--- a/src/stages/ast_typed/misc_smart.ml
+++ b/src/stages/ast_typed/misc_smart.ml
@@ -45,9 +45,11 @@ module Captured_variables = struct
   let empty : bindings = []
   let of_list : expression_variable list -> bindings = fun x -> x
 
-  let rec expression : bindings -> expression -> bindings result = fun b ae ->
+  let rec expression : bindings -> expression -> bindings result = fun b e ->
+    expression_content b e.environment e.expression_content
+  and expression_content : bindings -> full_environment -> expression_content -> bindings result = fun b env ec ->
     let self = expression b in
-    match ae.expression_content with
+    match ec with
     | E_lambda l -> ok @@ Free_variables.lambda empty l
     | E_literal _ -> ok empty
     | E_constant {arguments;_} ->
@@ -56,7 +58,7 @@ module Captured_variables = struct
     | E_variable name -> (
         let%bind env_element =
           trace_option (simple_error "missing var in env") @@
-          Environment.get_opt name ae.environment in
+          Environment.get_opt name env in
         match env_element.definition with
         | ED_binder -> ok empty
         | ED_declaration {expr=_ ; free_variables=_} -> simple_fail "todo"
@@ -92,6 +94,9 @@ module Captured_variables = struct
     | E_let_in li ->
       let b' = union (singleton li.let_binder) b in
       expression b' li.let_result
+    | E_recursive r -> 
+      let b' = union (singleton r.fun_name) b in
+      expression_content b' env @@ E_lambda r.lambda
 
   and matching_variant_case : type a . (bindings -> a -> bindings result) -> bindings -> ((constructor' * expression_variable) * a) -> bindings result  = fun f b ((_,n),c) ->
     f (union (singleton n) b) c
diff --git a/src/stages/ast_typed/types.ml b/src/stages/ast_typed/types.ml
index c20eef077..af143aa89 100644
--- a/src/stages/ast_typed/types.ml
+++ b/src/stages/ast_typed/types.ml
@@ -41,6 +41,7 @@ and expression_content =
   | E_application of application
   | E_lambda of lambda
   | E_let_in of let_in
+  | E_recursive of recursive
   (* Variant *)
   | E_constructor of constructor (* For user defined constructors *)
   | E_matching of matching
@@ -76,6 +77,12 @@ and let_in = {
     inline : inline ;
   }
 
+and recursive = {
+  fun_name : expression_variable;
+  fun_type : type_expression;
+  lambda : lambda;
+}
+
 and constructor = {
     constructor: constructor';
     element: expression ;
diff --git a/src/stages/typesystem/misc.ml b/src/stages/typesystem/misc.ml
index f6618dd43..10a59f4bc 100644
--- a/src/stages/typesystem/misc.ml
+++ b/src/stages/typesystem/misc.ml
@@ -164,6 +164,12 @@ module Substitution = struct
         let%bind rhs = s_expression ~substs rhs in
         let%bind let_result = s_expression ~substs let_result in
         ok @@ T.E_let_in { let_binder; rhs; let_result; inline }
+      | T.E_recursive { fun_name; fun_type; lambda} ->
+        let%bind fun_name = s_variable ~substs fun_name in
+        let%bind fun_type = s_type_expression ~substs fun_type in
+        let%bind sec = s_expression_content ~substs (T.E_lambda lambda) in
+        let lambda = match sec with E_lambda l -> l | _ -> failwith "impossible case" in
+        ok @@ T.E_recursive { fun_name; fun_type; lambda}
       | T.E_constructor  {constructor;element} ->
         let%bind constructor = s_constructor ~substs constructor in
         let%bind element = s_expression ~substs element in