diff --git a/src/ast_simplified/PP.ml b/src/ast_simplified/PP.ml
index 725c2b908..8120fa6cc 100644
--- a/src/ast_simplified/PP.ml
+++ b/src/ast_simplified/PP.ml
@@ -44,7 +44,7 @@ let rec expression ppf (e:expression) = match e with
   | E_look_up (ds, ind) -> fprintf ppf "(%a)[%a]" annotated_expression ds annotated_expression ind
   | E_lambda {binder;input_type;output_type;result;body} ->
       fprintf ppf "lambda (%s:%a) : %a {@;  @[<v>%a@]@;} return %a"
-        binder type_annotation input_type type_annotation output_type
+        binder type_expression input_type type_expression output_type
         block body annotated_expression result
   | E_matching (ae, m) ->
       fprintf ppf "match %a with %a" annotated_expression ae (matching annotated_expression) m
@@ -63,6 +63,8 @@ let rec expression ppf (e:expression) = match e with
       name
       PP_helpers.(list_sep access (const ".")) path
       annotated_expression expr
+  | E_let_in { binder; rhs; result } ->
+      fprintf ppf "let %s = %a in %a" binder annotated_expression rhs annotated_expression result
 
 and assoc_annotated_expression ppf : (ae * ae) -> unit = fun (a, b) ->
   fprintf ppf "%a -> %a" annotated_expression a annotated_expression b
diff --git a/src/ast_simplified/combinators.ml b/src/ast_simplified/combinators.ml
index c17b457c9..6744722a6 100644
--- a/src/ast_simplified/combinators.ml
+++ b/src/ast_simplified/combinators.ml
@@ -137,8 +137,8 @@ let e_lambda (binder : string)
   : expression =
   E_lambda {
     binder = (make_name binder) ;
-    input_type = Some input_type ;
-    output_type = Some output_type ;
+    input_type = input_type ;
+    output_type = output_type ;
     result = (make_e_a result) ;
     body ;
   }
diff --git a/src/ast_simplified/types.ml b/src/ast_simplified/types.ml
index af1e1943a..75b17a667 100644
--- a/src/ast_simplified/types.ml
+++ b/src/ast_simplified/types.ml
@@ -1,3 +1,4 @@
+[@@@warning "-30"]
 module Map = Simple_utils.Map
 module Location = Simple_utils.Location
 
@@ -47,12 +48,18 @@ and type_expression =
 
 and lambda = {
   binder: name ;
-  input_type: type_expression option;
-  output_type: type_expression option;
+  input_type: type_expression;
+  output_type: type_expression;
   result: ae ;
   body: block ;
 }
 
+and let_in = {
+  binder : name;
+  rhs    : ae;
+  result : ae;
+}
+
 and expression =
   (* Base *)
   | E_literal of literal
@@ -60,6 +67,7 @@ and expression =
   | E_variable of name
   | E_lambda of lambda
   | E_application of (ae * ae)
+  | E_let_in of let_in
   (* E_Tuple *)
   | E_tuple of ae list
   (* Sum *)
diff --git a/src/ast_typed/PP.ml b/src/ast_typed/PP.ml
index 22d241ca0..6292cb650 100644
--- a/src/ast_typed/PP.ml
+++ b/src/ast_typed/PP.ml
@@ -54,6 +54,8 @@ and expression ppf (e:expression) : unit =
       name.type_name
       PP_helpers.(list_sep pre_access (const ".")) path
       annotated_expression expr
+  | E_let_in { binder; rhs; result } ->
+      fprintf ppf "let %s = %a in %a" binder annotated_expression rhs annotated_expression result
 
 and value ppf v = annotated_expression ppf v
 
diff --git a/src/ast_typed/misc.ml b/src/ast_typed/misc.ml
index f2a5005a8..e34276654 100644
--- a/src/ast_typed/misc.ml
+++ b/src/ast_typed/misc.ml
@@ -62,6 +62,11 @@ module Free_variables = struct
     | E_sequence (a , b) -> unions @@ List.map self [ a ; b ]
     | E_loop (expr , body) -> unions @@ List.map self [ expr ; body ]
     | E_assign (_ , _ , expr) -> self expr
+    | E_let_in { binder; rhs; result } ->
+      let b' = union (singleton binder) b in
+      union
+        (annotated_expression b' result)
+        (annotated_expression b rhs)
 
   and lambda : bindings -> lambda -> bindings = fun b l ->
     let b' = union (singleton l.binder) b in
diff --git a/src/ast_typed/misc_smart.ml b/src/ast_typed/misc_smart.ml
index cbd5b1c4a..b4ac2f93c 100644
--- a/src/ast_typed/misc_smart.ml
+++ b/src/ast_typed/misc_smart.ml
@@ -94,14 +94,14 @@ module Captured_variables = struct
       let%bind cs' = matching_expression b cs in
       ok @@ union a' cs'
     | E_failwith a -> self a
-    | E_sequence (a , b) ->
-      let%bind lst' = bind_map_list self [ a ; b ] in
-      ok @@ unions lst'
+    | E_sequence (_ , b) -> self b
     | E_loop (expr , body) ->
       let%bind lst' = bind_map_list self [ expr ; body ] in
       ok @@ unions lst'
     | E_assign (_ , _ , expr) -> self expr
-
+    | E_let_in li ->
+      let b' = union (singleton li.binder) b in
+      annotated_expression b' li.result
 
   and instruction' : bindings -> instruction -> (bindings * bindings) result = fun b i ->
     match i with
diff --git a/src/ast_typed/types.ml b/src/ast_typed/types.ml
index c6178730d..72cd5ef34 100644
--- a/src/ast_typed/types.ml
+++ b/src/ast_typed/types.ml
@@ -75,6 +75,12 @@ and lambda = {
   body: block ;
 }
 
+and let_in = {
+  binder: name;
+  rhs: ae;
+  result: ae;
+}
+
 and expression =
   (* Base *)
   | E_literal of literal
@@ -82,6 +88,7 @@ and expression =
   | E_variable of name
   | E_application of (ae * ae)
   | E_lambda of lambda
+  | E_let_in of let_in
   (* Tuple *)
   | E_tuple of ae list
   | E_tuple_accessor of (ae * int) (* Access n'th tuple's element *)
diff --git a/src/simplify/camligo.ml b/src/simplify/camligo.ml
index bba10ebc1..7a99abcb4 100644
--- a/src/simplify/camligo.ml
+++ b/src/simplify/camligo.ml
@@ -461,8 +461,8 @@ let let_entry : _ -> _ result = fun l ->
   let lambda =
     O.{
       binder = input_nty.type_name ;
-      input_type = Some input_type';
-      output_type = Some output_type';
+      input_type = input_type';
+      output_type = output_type';
       result ;
       body = tpl_declarations @ body' ;
     } in
diff --git a/src/simplify/pascaligo.ml b/src/simplify/pascaligo.ml
index ad686959f..be8526b19 100644
--- a/src/simplify/pascaligo.ml
+++ b/src/simplify/pascaligo.ml
@@ -350,8 +350,8 @@ and simpl_fun_declaration : Raw.fun_decl -> named_expression result = fun x ->
        let%bind result = simpl_expression return in
        let%bind output_type = simpl_type_expression ret_type in
        let body = local_declarations @ instructions in
-       let expression = E_lambda {binder ; input_type = Some input_type;
-                                  output_type = Some output_type; result ; body } in
+       let expression = E_lambda {binder ; input_type = input_type;
+                                  output_type = output_type; result ; body } in
        let type_annotation = Some (T_function (input_type, output_type)) in
        ok {name;annotated_expression = {expression;type_annotation}}
      )
@@ -390,8 +390,8 @@ and simpl_fun_declaration : Raw.fun_decl -> named_expression result = fun x ->
 
        let body = tpl_declarations @ local_declarations @ instructions in
        let%bind result = simpl_expression return in
-       let expression = E_lambda {binder ; input_type = Some input_type;
-                                  output_type = Some output_type; result ; body } in
+       let expression = E_lambda {binder ; input_type = input_type;
+                                  output_type = output_type; result ; body } in
        let type_annotation = Some (T_function (input_type, output_type)) in
        ok {name = name.value;annotated_expression = {expression;type_annotation}}
      )
diff --git a/src/transpiler/transpiler.ml b/src/transpiler/transpiler.ml
index 33d3953cf..bda44e924 100644
--- a/src/transpiler/transpiler.ml
+++ b/src/transpiler/transpiler.ml
@@ -247,12 +247,10 @@ and translate_annotated_expression (ae:AST.annotated_expression) : expression re
   let f = translate_annotated_expression in
   match ae.expression with
     (* Optimise immediate application as a let-in *)
-  | E_application ({expression = E_lambda {binder; input_type; output_type=_; body=[]; result}; _},
-                   rhs) ->
-    let%bind ty' = translate_type input_type in
+  | E_let_in {binder; rhs; result} ->
     let%bind rhs' = translate_annotated_expression rhs in
     let%bind result' = translate_annotated_expression result in
-    return (E_let_in ((binder, ty'), rhs', result'))
+    return (E_let_in ((binder, rhs'.type_value), rhs', result'))
   | E_failwith ae -> (
       let%bind ae' = translate_annotated_expression ae in
       return @@ E_constant ("FAILWITH" , [ae'])
diff --git a/src/typer/typer.ml b/src/typer/typer.ml
index 88a1da145..58220239d 100644
--- a/src/typer/typer.ml
+++ b/src/typer/typer.ml
@@ -490,16 +490,8 @@ and type_annotated_expression : environment -> I.annotated_expression -> O.annot
       result ;
       body ;
     } -> (
-      let%bind input_type =
-        let%bind input_type =
-          trace_option (simple_error "missing annotation on input type")
-            input_type in
-        evaluate_type e input_type in
-      let%bind output_type =
-        let%bind output_type =
-          trace_option (simple_error "missing annotation of output type")
-            output_type in
-        evaluate_type e output_type in
+      let%bind input_type = evaluate_type e input_type in
+      let%bind output_type = evaluate_type e output_type in
       let e' = Environment.add_ez_binder binder input_type e in
       let%bind (body, e'') = type_block_full e' body in
       let%bind result = type_annotated_expression e'' result in
@@ -619,7 +611,11 @@ and type_annotated_expression : environment -> I.annotated_expression -> O.annot
       trace_strong (simple_error "assign type doesn't match left-hand-side") @@
       Ast_typed.assert_type_value_eq (assign_tv , get_type_annotation expr') in
     return (O.E_assign (typed_name , path' , expr')) (t_unit ())
-
+  | E_let_in {binder ; rhs ; result} ->
+    let%bind rhs = type_annotated_expression e rhs in
+    let e' = Environment.add_ez_binder binder rhs.type_annotation e in
+    let%bind result = type_annotated_expression e' result in
+    return (E_let_in {binder; rhs; result}) result.type_annotation
 
 and type_constant (name:string) (lst:O.type_value list) (tv_opt:O.type_value option) : (string * O.type_value) result =
   (* Constant poorman's polymorphism *)
@@ -694,7 +690,7 @@ let rec untype_annotated_expression (e:O.annotated_expression) : (I.annotated_ex
       let%bind output_type = untype_type_value output_type in
       let%bind result = untype_annotated_expression result in
       let%bind body = untype_block body in
-      return (E_lambda {binder;input_type = Some input_type;output_type = Some output_type;body;result})
+      return (E_lambda {binder;input_type = input_type;output_type = output_type;body;result})
   | E_tuple lst ->
       let%bind lst' = bind_list
         @@ List.map untype_annotated_expression lst in
@@ -731,6 +727,10 @@ let rec untype_annotated_expression (e:O.annotated_expression) : (I.annotated_ex
   | E_sequence _
   | E_loop _
   | E_assign _ -> simple_fail "not possible to untranspile statements yet"
+  | E_let_in {binder;rhs;result} ->
+      let%bind rhs = untype_annotated_expression rhs in
+      let%bind result = untype_annotated_expression result in
+      return (E_let_in {binder;rhs;result})
 
 and untype_block (b:O.block) : (I.block) result =
   bind_list @@ List.map untype_instruction b