diff --git a/src/parser/ligodity.ml b/src/parser/ligodity.ml
index 81ee4183e..fba239b59 100644
--- a/src/parser/ligodity.ml
+++ b/src/parser/ligodity.ml
@@ -3,7 +3,7 @@ open Parser_ligodity
 module Parser = Parser_ligodity.Parser
 module AST = Parser_ligodity.AST
 
-let parse_file (source: string) : AST.t result =  
+let parse_file (source: string) : AST.t result =
   (* let pp_input =
    *   let prefix = Filename.(source |> basename |> remove_extension)
    *   and suffix = ".pp.ligo"
@@ -50,7 +50,7 @@ let parse_file (source: string) : AST.t result =
   ok raw
 
 let parse_string (s:string) : AST.t result =
-  
+
   let lexbuf = Lexing.from_string s in
   let read = Lexer.get_token in
   specific_try (function
@@ -94,5 +94,5 @@ let parse_expression (s:string) : AST.expr result =
               start.pos_fname s
           in
           simple_error str
-    ) @@ (fun () -> Parser.expr read lexbuf) >>? fun raw ->
+    ) @@ (fun () -> Parser.interactive_expr read lexbuf) >>? fun raw ->
   ok raw
diff --git a/src/parser/ligodity/Parser.mly b/src/parser/ligodity/Parser.mly
index 7221f6fd8..cc76a8867 100644
--- a/src/parser/ligodity/Parser.mly
+++ b/src/parser/ligodity/Parser.mly
@@ -47,9 +47,9 @@ let rec mk_field_path (rank, tail) =
 
 (* Entry points *)
 
-%start program expr
+%start program interactive_expr
 %type <AST.t> program
-%type <AST.expr> expr
+%type <AST.expr> interactive_expr
 
 %%
 
@@ -285,7 +285,7 @@ entry_binding:
     {bindings = pattern :: hd :: tl; lhs_type=$3; eq=$4; let_rhs}
   }
   | ident type_annotation? eq fun_expr(expr) {
-    let pattern = PVar $1 in	    
+    let pattern = PVar $1 in
     {bindings = [pattern]; lhs_type=$2; eq=$3; let_rhs=$4} }
 
 (* Top-level non-recursive definitions *)
@@ -382,6 +382,9 @@ tail:
 
 (* Expressions *)
 
+interactive_expr:
+  expr EOF                                                       { $1 }
+
 expr:
   base_cond__open(expr)                                    {       $1 }
 | reg(match_expr(base_cond))                               { ECase $1 }
@@ -468,7 +471,7 @@ fun_expr(right_expr):
     } in
     EFun { region=$1.region; value=f }
   }
-	 
+
 disj_expr_level:
   reg(disj_expr)                          { ELogic (BoolExpr (Or $1)) }
 | conj_expr_level                                                { $1 }
diff --git a/src/simplify/ligodity.ml b/src/simplify/ligodity.ml
index b217325ce..3681ba6f7 100644
--- a/src/simplify/ligodity.ml
+++ b/src/simplify/ligodity.ml
@@ -20,13 +20,92 @@ let get_value : 'a Raw.reg -> 'a = fun x -> x.value
 module Errors = struct
   let wrong_pattern expected_name actual =
     let title () = "wrong pattern" in
-    let message () = Format.asprintf "expected a %s, got something else" expected_name in
+    let message () = "" in
     let data = [
+      ("expected", fun () -> expected_name);
       ("actual_loc" , fun () -> Format.asprintf "%a" Location.pp_lift @@ Raw.region_of_pattern actual)
     ] in
     error ~data title message
 
+  let multiple_patterns construct (patterns: Raw.pattern list) =
+    let title () = "multiple patterns" in
+    let message () =
+      Format.asprintf "multiple patterns in \"%s\" are not supported yet" construct in
+    let patterns_loc =
+      List.fold_left (fun a p -> Region.cover a (Raw.region_of_pattern p))
+        Region.min patterns in
+    let data = [
+      ("patterns_loc", fun () -> Format.asprintf "%a" Location.pp_lift @@ patterns_loc)
+    ] in
+    error ~data title message
+
+  let unknown_predefined_type name =
+    let title () = "type constants" in
+    let message () =
+      Format.asprintf "unknown predefined type \"%s\"" name.Region.value in
+    let data = [
+      ("typename_loc",
+       fun () -> Format.asprintf "%a" Location.pp_lift @@ name.Region.region)
+    ] in
+    error ~data title message
+
+  let unsupported_arith_op expr =
+    let title () = "arithmetic expressions" in
+    let message () =
+      Format.asprintf "this arithmetic operator is not supported yet" in
+    let expr_loc = Raw.region_of_expr expr in
+    let data = [
+      ("expr_loc",
+       fun () -> Format.asprintf "%a" Location.pp_lift @@ expr_loc)
+    ] in
+    error ~data title message
+
+  let unsupported_string_catenation expr =
+    let title () = "string expressions" in
+    let message () =
+      Format.asprintf "string concatenation is not supported yet" in
+    let expr_loc = Raw.region_of_expr expr in
+    let data = [
+      ("expr_loc",
+       fun () -> Format.asprintf "%a" Location.pp_lift @@ expr_loc)
+    ] in
+    error ~data title message
+
+  let untyped_fun_param var =
+    let title () = "function parameter" in
+    let message () =
+      Format.asprintf "untyped function parameters are not supported yet" in
+    let param_loc = var.Region.region in
+    let data = [
+      ("param_loc",
+       fun () -> Format.asprintf "%a" Location.pp_lift @@ param_loc)
+    ] in
+    error ~data title message
+
+  let unsupported_tuple_pattern p =
+    let title () = "tuple pattern" in
+    let message () =
+      Format.asprintf "tuple patterns are not supported yet" in
+    let pattern_loc = Raw.region_of_pattern p in
+    let data = [
+      ("pattern_loc",
+       fun () -> Format.asprintf "%a" Location.pp_lift @@ pattern_loc)
+    ] in
+    error ~data title message
+
+  let unsupported_cst_constr p =
+    let title () = "constant constructor" in
+    let message () =
+      Format.asprintf "constant constructors are not supported yet" in
+    let pattern_loc = Raw.region_of_pattern p in
+    let data = [
+      ("pattern_loc",
+       fun () -> Format.asprintf "%a" Location.pp_lift @@ pattern_loc)
+    ] in
+    error ~data title message
+
 end
+
 open Errors
 
 open Operators.Simplify.Ligodity
@@ -48,7 +127,7 @@ let rec pattern_to_typed_var : Raw.pattern -> _ = fun p ->
       ok (v , Some tp.type_expr)
     )
   | Raw.PVar v -> ok (v , None)
-  | _ -> fail @@ wrong_pattern "var/typed" p
+  | _ -> fail @@ wrong_pattern "typed variable" p
 
 let rec expr_to_typed_expr : Raw.expr -> _ = fun e ->
   match e with
@@ -59,7 +138,7 @@ let rec expr_to_typed_expr : Raw.expr -> _ = fun e ->
 let patterns_to_var : Raw.pattern list -> _ = fun ps ->
   match ps with
   | [ pattern ] -> pattern_to_var pattern
-  | _ -> fail (simple_error "multiple patterns not supported on lets yet")
+  | _ -> fail @@ multiple_patterns "let" ps
 
 let rec simpl_type_expression : Raw.type_expr -> type_expression result = fun te ->
   trace (simple_info "simplifying this type expression...") @@
@@ -83,7 +162,7 @@ let rec simpl_type_expression : Raw.type_expr -> type_expression result = fun te
       let (name, tuple) = x.value in
       let lst = npseq_to_list tuple.value.inside in
       let%bind cst =
-        trace_option (simple_error "unrecognized type constants") @@
+        trace_option (unknown_predefined_type name) @@
         List.assoc_opt name.value type_constants
       in
       let%bind lst' = bind_map_list simpl_type_expression lst in
@@ -260,7 +339,8 @@ let rec simpl_expression :
       let n = Z.to_int @@ snd @@ n in
       return @@ e_literal ~loc (Literal_tez n)
     )
-  | EArith _ -> simple_fail "arith: not supported yet"
+  | EArith _ as e ->
+       fail @@ unsupported_arith_op e
   | EString (String s) -> (
       let (s , loc) = r_split s in
       let s' =
@@ -269,7 +349,8 @@ let rec simpl_expression :
       in
       return @@ e_literal ~loc (Literal_string s')
     )
-  | EString _ -> simple_fail "string: not supported yet"
+  | EString (Cat _) as e ->
+      fail @@ unsupported_string_catenation e
   | ELogic l -> simpl_logic_expression l
   | EList l -> simpl_list_expression l
   | ECase c -> (
@@ -341,7 +422,7 @@ and simpl_fun lamb' : expr result =
       | "storage" , None ->
         ok (var , T_variable "storage")
       | _ , None ->
-        simple_fail "untyped function parameter"
+          fail @@ untyped_fun_param var
       | _ , Some ty -> (
         let%bind ty' = simpl_type_expression ty in
         ok (var , ty')
@@ -431,9 +512,11 @@ and simpl_tuple_expression ?loc (lst:Raw.expr list) : expression result =
       let%bind lst = bind_list @@ List.map simpl_expression lst in
       return @@ e_tuple ?loc lst
 
-and simpl_declaration : Raw.declaration -> declaration Location.wrap result = fun t ->
+and simpl_declaration : Raw.declaration -> declaration Location.wrap result =
+  fun t ->
   let open! Raw in
-  let loc : 'a . 'a Raw.reg -> _ -> _ = fun x v -> Location.wrap ~loc:(File x.region) v in
+  let loc : 'a . 'a Raw.reg -> _ -> _ =
+    fun x v -> Location.wrap ~loc:(File x.region) v in
   match t with
   | TypeDecl x ->
       let {name;type_expr} : Raw.type_decl = x.value in
@@ -444,8 +527,9 @@ and simpl_declaration : Raw.declaration -> declaration Location.wrap result = fu
       let _ , binding = x.value in
       let {bindings ; lhs_type ; let_rhs} = binding in
       let%bind (var , args) =
-        let%bind (hd , tl) = match bindings with
-          | [] -> simple_fail "let without bindgings"
+        let%bind (hd , tl) =
+          match bindings with
+          | [] -> simple_fail "let without bindings"
           | hd :: tl -> ok (hd , tl)
         in
         let%bind var = pattern_to_var hd in
@@ -484,21 +568,22 @@ and simpl_cases : type a . (Raw.pattern * a) list -> a matching result = fun t -
         in
         fail error
   in
-  let get_tuple (t:Raw.pattern) = match t with
+  let rec get_tuple (t:Raw.pattern) = match t with
     | PTuple v -> npseq_to_list v.value
+    | PPar p -> get_tuple p.value.inside
     | x -> [ x ]
   in
   let get_single (t:Raw.pattern) =
     let t' = get_tuple t in
     let%bind () =
-      trace_strong (simple_error "not single") @@
+      trace_strong (unsupported_tuple_pattern t) @@
       Assert.assert_list_size t' 1 in
     ok (List.hd t') in
   let get_constr (t:Raw.pattern) = match t with
     | PConstr v -> (
         let (const , pat_opt) = v.value in
         let%bind pat =
-          trace_option (simple_error "No constructor without variable yet") @@
+          trace_option (unsupported_cst_constr t) @@
           pat_opt in
         let%bind single_pat = get_single pat in
         let%bind var = get_var single_pat in
diff --git a/src/typer/typer.ml b/src/typer/typer.ml
index b2120b495..4104db3df 100644
--- a/src/typer/typer.ml
+++ b/src/typer/typer.ml
@@ -25,7 +25,43 @@ module Errors = struct
     let message () = "" in
     let data = [
       ("variable" , fun () -> Format.asprintf "%s" n) ;
-      ("in" , fun () -> Format.asprintf "%a" Environment.PP.full_environment e)
+      ("environment" , fun () -> Format.asprintf "%a" Environment.PP.full_environment e)
+    ] in
+    error ~data title message ()
+
+  let match_empty_variant : type a . a I.matching -> unit -> _ =
+    fun matching () ->
+    let title = (thunk "match with no cases") in
+    let message () = "" in
+    let data = [
+      ("variant" , fun () -> Format.asprintf "%a" I.PP.matching_type matching)
+    ] in
+    error ~data title message ()
+
+  let match_missing_case : type a . a I.matching -> unit -> _ =
+    fun matching () ->
+    let title = (thunk "missing case in match") in
+    let message () = "" in
+    let data = [
+      ("variant" , fun () -> Format.asprintf "%a" I.PP.matching_type matching)
+    ] in
+    error ~data title message ()
+
+  let match_redundant_case : type a . a I.matching -> unit -> _ =
+    fun matching () ->
+    let title = (thunk "missing case in match") in
+    let message () = "" in
+    let data = [
+      ("variant" , fun () -> Format.asprintf "%a" I.PP.matching_type matching)
+    ] in
+    error ~data title message ()
+
+  let unbound_constructor (e:environment) (n:string) () =
+    let title = (thunk "unbound constructor") in
+    let message () = "" in
+    let data = [
+      ("constructor" , fun () -> Format.asprintf "%s" n) ;
+      ("environment" , fun () -> Format.asprintf "%a" Environment.PP.full_environment e)
     ] in
     error ~data title message ()
 
@@ -73,15 +109,80 @@ module Errors = struct
     ] in
     error ~data title message ()
 
-  let match_error : type a . expected: a I.Types.matching -> actual: O.Types.type_value -> unit -> _ =
-    fun ~expected ~actual () ->
+  let match_error : type a . ?msg:string -> expected: a I.matching -> actual: O.type_value -> unit -> _ =
+    fun ?(msg = "") ~expected ~actual () ->
     let title = (thunk "typing match") in
-    let message () = "" in
+    let message () = msg in
     let data = [
       ("expected" , fun () -> Format.asprintf "%a" I.PP.matching_type expected);
       ("actual" , fun () -> Format.asprintf "%a" O.PP.type_value actual)
     ] in
     error ~data title message ()
+
+  let needs_annotation (e : I.expression) (case : string) () =
+    let title = (thunk "this expression must be annotated with its type") in
+    let message () = Format.asprintf "%s needs an annotation" case in
+    let data = [
+      ("expression" , fun () -> Format.asprintf "%a" I.PP.expression e)
+    ] in
+    error ~data title message ()
+
+  let type_error_approximate ?(msg="") ~(expected: string) ~(actual: O.type_value) ~(expression : O.value) () =
+    let title = (thunk "type error") in
+    let message () = msg in
+    let data = [
+      ("expected"   , fun () -> Format.asprintf "%s" expected);
+      ("actual"     , fun () -> Format.asprintf "%a" O.PP.type_value actual);
+      ("expression" , fun () -> Format.asprintf "%a" O.PP.value expression)
+    ] in
+    error ~data title message ()
+
+  let type_error ?(msg="") ~(expected: O.type_value) ~(actual: O.type_value) ~(expression : O.value) () =
+    let title = (thunk "type error") in
+    let message () = msg in
+    let data = [
+      ("expected"   , fun () -> Format.asprintf "%a" O.PP.type_value expected);
+      ("actual"     , fun () -> Format.asprintf "%a" O.PP.type_value actual);
+      ("expression" , fun () -> Format.asprintf "%a" O.PP.value expression)
+    ] in
+    error ~data title message ()
+
+  let bad_tuple_index (index : int) (ae : I.expression) (t : O.type_value) () =
+    let title = (thunk "invalid tuple index") in
+    let message () = "" in
+    let data = [
+      ("index" , fun () -> Format.asprintf "%d" index) ;
+      ("tuple_value" , fun () -> Format.asprintf "%a" I.PP.expression ae) ;
+      ("tuple_type" , fun () -> Format.asprintf "%a" O.PP.type_value t)
+    ] in
+    error ~data title message ()
+
+  let bad_record_access (field : string) (ae : I.expression) (t : O.type_value) () =
+    let title = (thunk "invalid record field") in
+    let message () = "" in
+    let data = [
+      ("field" , fun () -> Format.asprintf "%s" field) ;
+      ("record_value" , fun () -> Format.asprintf "%a" I.PP.expression ae) ;
+      ("tuple_type" , fun () -> Format.asprintf "%a" O.PP.type_value t)
+    ] in
+    error ~data title message ()
+
+  let not_supported_yet (message : string) (ae : I.expression) () =
+    let title = (thunk "not suported yet") in
+    let message () = message in
+    let data = [
+      ("expression" , fun () -> Format.asprintf "%a"  I.PP.expression ae)
+    ] in
+    error ~data title message ()
+
+  let not_supported_yet_untranspile (message : string) (ae : O.expression) () =
+    let title = (thunk "not suported yet") in
+    let message () = message in
+    let data = [
+      ("expression" , fun () -> Format.asprintf "%a"  O.PP.expression ae)
+    ] in
+    error ~data title message ()
+
 end
 open Errors
 
@@ -147,7 +248,7 @@ and type_match : type i o . (environment -> i -> o result) -> environment -> O.t
         trace_strong (match_error ~expected:i ~actual:t)
         @@ get_t_tuple t in
       let%bind lst' =
-        generic_try (simple_error "Matching tuple of different size")
+        generic_try (match_tuple_wrong_arity t_tuple lst)
         @@ (fun () -> List.combine lst t_tuple) in
       let aux prev (name, tv) = Environment.add_ez_binder name tv prev in
       let e' = List.fold_left aux e lst' in
@@ -157,7 +258,7 @@ and type_match : type i o . (environment -> i -> o result) -> environment -> O.t
       let%bind variant_opt =
         let aux acc ((constructor_name , _) , _) =
           let%bind (_ , variant) =
-            trace_option (simple_error "bad constructor") @@
+            trace_option (unbound_constructor e constructor_name) @@
             Environment.get_constructor constructor_name e in
           let%bind acc = match acc with
             | None -> ok (Some variant)
@@ -166,12 +267,12 @@ and type_match : type i o . (environment -> i -> o result) -> environment -> O.t
                 ok (Some variant)
               ) in
           ok acc in
-        trace (simple_error "in match variant") @@
+        trace (simple_info "in match variant") @@
         bind_fold_list aux None lst in
       let%bind variant =
-        trace_option (simple_error "empty variant") @@
+        trace_option (match_empty_variant i) @@
         variant_opt in
-      let%bind  () =
+      let%bind () =
         let%bind variant_cases' =
           trace (match_error ~expected:i ~actual:t)
           @@ Ast_typed.Combinators.get_t_sum variant in
@@ -181,17 +282,17 @@ and type_match : type i o . (environment -> i -> o result) -> environment -> O.t
           Assert.assert_true (List.mem c match_cases)
         in
         let%bind () =
-          trace (simple_error "missing case match") @@
+          trace_strong (match_missing_case i) @@
           bind_iter_list test_case variant_cases in
         let%bind () =
-          trace_strong (simple_error "redundant case match") @@
+          trace_strong (match_redundant_case i) @@
           Assert.assert_true List.(length variant_cases = length match_cases) in
         ok ()
       in
       let%bind lst' =
         let aux ((constructor_name , name) , b) =
           let%bind (constructor , _) =
-            trace_option (simple_error "bad constructor??") @@
+            trace_option (unbound_constructor e constructor_name) @@
             Environment.get_constructor constructor_name e in
           let e' = Environment.add_ez_binder name constructor e in
           let%bind b' = f e' b in
@@ -257,7 +358,7 @@ and type_expression : environment -> ?tv_opt:O.type_value -> I.expression -> O.a
   trace main_error @@
   match Location.unwrap ae with
   (* Basic *)
-  | E_failwith _ -> simple_fail "can't type failwith in isolation"
+  | E_failwith _ -> fail @@ needs_annotation ae "the failwith keyword"
   | E_variable name ->
       let%bind tv' =
         trace_option (unbound_variable e name)
@@ -297,14 +398,14 @@ and type_expression : environment -> ?tv_opt:O.type_value -> I.expression -> O.a
         | Access_tuple index -> (
             let%bind tpl_tv = get_t_tuple prev.type_annotation in
             let%bind tv =
-              generic_try (simple_error "bad tuple index")
+              generic_try (bad_tuple_index index ae prev.type_annotation)
               @@ (fun () -> List.nth tpl_tv index) in
             return (E_tuple_accessor (prev , index)) tv
           )
         | Access_record property -> (
             let%bind r_tv = get_t_record prev.type_annotation in
             let%bind tv =
-              generic_try (simple_error "bad record index")
+              generic_try (bad_record_access property ae prev.type_annotation)
               @@ (fun () -> SMap.find property r_tv) in
             return (E_record_accessor (prev , property)) tv
           )
@@ -316,7 +417,7 @@ and type_expression : environment -> ?tv_opt:O.type_value -> I.expression -> O.a
             return (E_look_up (prev , ae')) v
           )
       in
-      trace (simple_error "accessing") @@
+      trace (simple_info "accessing") @@
       bind_fold_list aux e' path
 
   (* Sum *)
@@ -360,7 +461,7 @@ and type_expression : environment -> ?tv_opt:O.type_value -> I.expression -> O.a
         let%bind ty =
           let%bind opt = bind_fold_list aux init
           @@ List.map get_type_annotation lst' in
-          trace_option (simple_error "empty list expression without annotation") opt in
+          trace_option (needs_annotation ae "empty list") opt in
         ok (t_list ty ())
       in
       return (E_list lst') tv
@@ -379,7 +480,7 @@ and type_expression : environment -> ?tv_opt:O.type_value -> I.expression -> O.a
             @@ List.map get_type_annotation
             @@ List.map fst lst' in
           let%bind annot = bind_map_option get_t_map_key tv_opt in
-          trace (simple_error "untyped empty map expression") @@
+          trace (simple_info "empty map expression without a type annotation") @@
           O.merge_annotation annot sub
         in
         let%bind value_type =
@@ -388,7 +489,7 @@ and type_expression : environment -> ?tv_opt:O.type_value -> I.expression -> O.a
             @@ List.map get_type_annotation
             @@ List.map snd lst' in
           let%bind annot = bind_map_option get_t_map_value tv_opt in
-          trace (simple_error "untyped empty map expression") @@
+          trace (simple_info "empty map expression without a type annotation") @@
           O.merge_annotation annot sub
         in
         ok (t_map key_type value_type ())
@@ -403,7 +504,7 @@ and type_expression : environment -> ?tv_opt:O.type_value -> I.expression -> O.a
       let%bind input_type =
         let%bind input_type =
           (* Hack to take care of let_in introduced by `simplify/ligodity.ml` in ECase's hack *)
-          let default_action () = simple_fail "no input type provided" in
+          let default_action e () = fail @@ (needs_annotation e "the returned value") in
           match input_type with
           | Some ty -> ok ty
           | None -> (
@@ -413,11 +514,11 @@ and type_expression : environment -> ?tv_opt:O.type_value -> I.expression -> O.a
                   | I.E_variable name when name = (fst binder) -> (
                       match snd li.binder with
                       | Some ty -> ok ty
-                      | None -> default_action ()
+                      | None -> default_action li.rhs ()
                     )
-                  | _ -> default_action ()
+                  | _ -> default_action li.rhs ()
                 )
-              | _ -> default_action ()
+              | _ -> default_action result ()
             )
         in
         evaluate_type e input_type in
@@ -441,7 +542,11 @@ and type_expression : environment -> ?tv_opt:O.type_value -> I.expression -> O.a
         | T_function (param, result) ->
             let%bind _ = O.assert_type_value_eq (param, arg.type_annotation) in
             ok result
-        | _ -> simple_fail "applying to not-a-function"
+        | _ ->
+          fail @@ type_error_approximate
+            ~expected:"should be a function type"
+            ~expression:f
+            ~actual:f.type_annotation
       in
       return (E_application (f , arg)) tv
   | E_look_up dsi ->
@@ -458,11 +563,12 @@ and type_expression : environment -> ?tv_opt:O.type_value -> I.expression -> O.a
           let%bind fw = I.get_e_failwith match_true in
           let%bind fw' = type_expression e fw in
           let%bind mf' = type_expression e match_false in
+          let t = get_type_annotation ex' in
           let%bind () =
-            trace_strong (simple_error "Matching bool on not-a-bool")
-            @@ assert_t_bool (get_type_annotation ex') in
+            trace_strong (match_error ~expected:m ~actual:t)
+            @@ assert_t_bool t in
           let%bind () =
-            trace_strong (simple_error "Matching not-unit on an assert")
+            trace_strong (match_error ~msg:"matching not-unit on an assert" ~expected:m ~actual:t)
             @@ assert_t_unit (get_type_annotation mf') in
           let mt' = make_a_e
               (E_constant ("ASSERT" , [ex' ; fw']))
@@ -491,7 +597,7 @@ and type_expression : environment -> ?tv_opt:O.type_value -> I.expression -> O.a
             ok (Some cur) in
           let%bind tv_opt = bind_fold_list aux None tvs in
           let%bind tv =
-            trace_option (simple_error "empty matching") @@
+            trace_option (match_empty_variant m) @@
             tv_opt in
           return (O.E_matching (ex', m')) tv
         )
@@ -499,19 +605,34 @@ and type_expression : environment -> ?tv_opt:O.type_value -> I.expression -> O.a
   | E_sequence (a , b) ->
     let%bind a' = type_expression e a in
     let%bind b' = type_expression e b in
+    let a'_type_annot = get_type_annotation a' in
     let%bind () =
-      trace_strong (simple_error "first part of the sequence isn't of unit type") @@
-      Ast_typed.assert_type_value_eq (t_unit () , get_type_annotation a') in
+      trace_strong (type_error
+                      ~msg:"first part of the sequence should be of unit type"
+                      ~expected:(O.t_unit ())
+                      ~actual:a'_type_annot
+                      ~expression:a') @@
+      Ast_typed.assert_type_value_eq (t_unit () , a'_type_annot) in
     return (O.E_sequence (a' , b')) (get_type_annotation b')
   | E_loop (expr , body) ->
     let%bind expr' = type_expression e expr in
     let%bind body' = type_expression e body in
+    let t_expr' = get_type_annotation expr' in
     let%bind () =
-      trace_strong (simple_error "while condition isn't of type bool") @@
-      Ast_typed.assert_type_value_eq (t_bool () , get_type_annotation expr') in
+      trace_strong (type_error
+                      ~msg:"while condition isn't of type bool"
+                      ~expected:(O.t_bool ())
+                      ~actual:t_expr'
+                      ~expression:expr') @@
+      Ast_typed.assert_type_value_eq (t_bool () , t_expr') in
+    let t_body' = get_type_annotation body' in
     let%bind () =
-      trace_strong (simple_error "while body isn't of unit type") @@
-      Ast_typed.assert_type_value_eq (t_unit () , get_type_annotation body') in
+      trace_strong (type_error
+                     ~msg:"while body isn't of unit type"
+                     ~expected:(O.t_unit ())
+                     ~actual:t_body'
+                     ~expression:body') @@
+      Ast_typed.assert_type_value_eq (t_unit () , t_body') in
     return (O.E_loop (expr' , body')) (t_unit ())
   | E_assign (name , path , expr) ->
     let%bind typed_name =
@@ -523,24 +644,30 @@ and type_expression : environment -> ?tv_opt:O.type_value -> I.expression -> O.a
         | Access_tuple index -> (
             let%bind tpl = get_t_tuple prec_tv in
             let%bind tv' =
-              trace_option (simple_error "tuple too small") @@
+              trace_option (bad_tuple_index index ae prec_tv) @@
               List.nth_opt tpl index in
             ok (tv' , prec_path @ [O.Access_tuple index])
           )
         | Access_record property -> (
             let%bind m = get_t_record prec_tv in
             let%bind tv' =
-              trace_option (simple_error "tuple too small") @@
+              trace_option (bad_record_access property ae prec_tv) @@
               Map.String.find_opt property m in
             ok (tv' , prec_path @ [O.Access_record property])
           )
-        | Access_map _ -> simple_fail "no assign expressions with maps yet"
+        | Access_map _ ->
+          fail @@ not_supported_yet "assign expressions with maps are not supported yet" ae
       in
       bind_fold_list aux (typed_name.type_value , []) path in
     let%bind expr' = type_expression e expr in
+    let t_expr' = get_type_annotation expr' in
     let%bind () =
-      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
+      trace_strong (type_error
+                     ~msg:"type of the expression to assign doesn't match left-hand-side"
+                     ~expected:assign_tv
+                     ~actual:t_expr'
+                     ~expression:expr') @@
+      Ast_typed.assert_type_value_eq (assign_tv , t_expr') in
     return (O.E_assign (typed_name , path' , expr')) (t_unit ())
   | E_let_in {binder ; rhs ; result} ->
     let%bind rhs_tv_opt = bind_map_option (evaluate_type e) (snd binder) in
@@ -637,7 +764,7 @@ let rec untype_expression (e:O.annotated_expression) : (I.expression) result =
       return (e_failwith ae')
   | E_sequence _
   | E_loop _
-  | E_assign _ -> simple_fail "not possible to untranspile statements yet"
+  | E_assign _ -> fail @@ not_supported_yet_untranspile "not possible to untranspile statements yet" e.expression
   | E_let_in {binder;rhs;result} ->
       let%bind tv = untype_type_value rhs.type_annotation in
       let%bind rhs = untype_expression rhs in