diff --git a/src/ast_typed/misc.ml b/src/ast_typed/misc.ml
index c1393fe53..1094815df 100644
--- a/src/ast_typed/misc.ml
+++ b/src/ast_typed/misc.ml
@@ -17,6 +17,11 @@ module Errors = struct
     let full () = Format.asprintf "%a VS %a" PP.type_value a PP.type_value b in
     error title full ()
 
+  let different_props_in_record ka kb () =
+    let title () = "different keys in record" in
+    let content () = Format.asprintf "%s vs %s" ka kb in
+    error title content ()
+
   let different_size_constants = different_size_type "constants"
 
   let different_size_tuples = different_size_type "tuples"
@@ -25,6 +30,50 @@ module Errors = struct
 
   let different_size_records = different_size_type "records"
 
+  let different_types name a b () =
+    let title () = name ^ " are different" in
+    let full () = Format.asprintf "%a VS %a" PP.type_value a PP.type_value b in
+    info title full ()
+
+  let different_literals name a b () =
+    let title () = name ^ " are different" in
+    let full () = Format.asprintf "%a VS %a" PP.literal a PP.literal b in
+    info title full ()
+
+  let different_values name a b () =
+    let title () = name ^ " are different" in
+    let full () = Format.asprintf "%a VS %a" PP.value a PP.value b in
+    info title full ()
+
+  let different_literals_because_different_types name a b () =
+    let title () = "literals have different types: " ^ name in
+    let full () = Format.asprintf "%a VS %a" PP.literal a PP.literal b in
+    info title full ()
+
+  let different_values_because_different_types name a b () =
+    let title () = "values have different types: " ^ name in
+    let full () = Format.asprintf "%a VS %a" PP.value a PP.value b in
+    info title full ()
+
+  let error_uncomparable_literals name a b () =
+    let title () = name ^ " are different" in
+    let full () = Format.asprintf "%a VS %a" PP.literal a PP.literal b in
+    info title full ()
+
+  let error_uncomparable_values name a b () =
+    let title () = name ^ " are different" in
+    let full () = Format.asprintf "%a VS %a" PP.value a PP.value b in
+    info title full ()
+
+  let different_size_values name a b () =
+    let title () = name in
+    let full () = Format.asprintf "%a VS %a" PP.value a PP.value b in
+    error title full ()
+
+  let missing_key_in_record_value k () =
+    let title () = "missing keys in one of the records" in
+    let content () = Format.asprintf "%s" k in
+    error title content ()
 end
 
 module Free_variables = struct
@@ -186,7 +235,7 @@ let rec assert_type_value_eq (a, b: (type_value * type_value)) : unit result = m
       let%bind _ =
         trace_strong (different_constants ca cb)
         @@ Assert.assert_true (ca = cb) in
-      trace (simple_error "constant sub-expression")
+      trace (different_types "constant sub-expression" a b)
       @@ bind_list_iter assert_type_value_eq (List.combine lsta lstb)
     )
   | T_constant _, _ -> fail @@ different_kinds a b
@@ -202,7 +251,7 @@ let rec assert_type_value_eq (a, b: (type_value * type_value)) : unit result = m
       let%bind _ =
         trace_strong (different_size_sums a b)
         @@ Assert.assert_list_same_size sa' sb' in
-      trace (simple_error "sum type") @@
+      trace (different_types "sum type" a b) @@
       bind_list_iter aux (List.combine sa' sb')
     )
   | T_sum _, _ -> fail @@ different_kinds a b
@@ -211,18 +260,15 @@ let rec assert_type_value_eq (a, b: (type_value * type_value)) : unit result = m
       let rb' = SMap.to_kv_list rb in
       let aux ((ka, va), (kb, vb)) =
         let%bind _ =
-          let error =
-            let title () = "different props in record" in
-            let content () = Format.asprintf "%s vs %s" ka kb in
-            error title content in
-          trace_strong error @@
+          trace (different_types "records" a b) @@
+          trace_strong (different_props_in_record ka kb) @@
           Assert.assert_true (ka = kb) in
         assert_type_value_eq (va, vb)
       in
       let%bind _ =
         trace_strong (different_size_records a b)
         @@ Assert.assert_list_same_size ra' rb' in
-      trace (simple_error "record type")
+      trace (different_types "record type" a b)
       @@ bind_list_iter aux (List.combine ra' rb')
 
     )
@@ -239,30 +285,30 @@ let type_value_eq ab = Trace.to_bool @@ assert_type_value_eq ab
 let assert_literal_eq (a, b : literal * literal) : unit result =
   match (a, b) with
   | Literal_bool a, Literal_bool b when a = b -> ok ()
-  | Literal_bool _, Literal_bool _ -> simple_fail "different bools"
-  | Literal_bool _, _ -> simple_fail "bool vs non-bool"
+  | Literal_bool _, Literal_bool _ -> fail @@ different_literals "booleans" a b
+  | Literal_bool _, _ -> fail @@ different_literals_because_different_types "bool vs non-bool" a b
   | Literal_int a, Literal_int b when a = b -> ok ()
-  | Literal_int _, Literal_int _ -> simple_fail "different ints"
-  | Literal_int _, _ -> simple_fail "int vs non-int"
+  | Literal_int _, Literal_int _ -> fail @@ different_literals "different ints" a b
+  | Literal_int _, _ -> fail @@ different_literals_because_different_types "int vs non-int" a b
   | Literal_nat a, Literal_nat b when a = b -> ok ()
-  | Literal_nat _, Literal_nat _ -> simple_fail "different nats"
-  | Literal_nat _, _ -> simple_fail "nat vs non-nat"
+  | Literal_nat _, Literal_nat _ -> fail @@ different_literals "different nats" a b
+  | Literal_nat _, _ -> fail @@ different_literals_because_different_types "nat vs non-nat" a b
   | Literal_tez a, Literal_tez b when a = b -> ok ()
-  | Literal_tez _, Literal_tez _ -> simple_fail "different tezs"
-  | Literal_tez _, _ -> simple_fail "tez vs non-tez"
+  | Literal_tez _, Literal_tez _ -> fail @@ different_literals "different tezs" a b
+  | Literal_tez _, _ -> fail @@ different_literals_because_different_types "tez vs non-tez" a b
   | Literal_string a, Literal_string b when a = b -> ok ()
-  | Literal_string _, Literal_string _ -> simple_fail "different strings"
-  | Literal_string _, _ -> simple_fail "string vs non-string"
+  | Literal_string _, Literal_string _ -> fail @@ different_literals "different strings" a b
+  | Literal_string _, _ -> fail @@ different_literals_because_different_types "string vs non-string" a b
   | Literal_bytes a, Literal_bytes b when a = b -> ok ()
-  | Literal_bytes _, Literal_bytes _ -> simple_fail "different bytess"
-  | Literal_bytes _, _ -> simple_fail "bytes vs non-bytes"
+  | Literal_bytes _, Literal_bytes _ -> fail @@ different_literals "different bytes" a b
+  | Literal_bytes _, _ -> fail @@ different_literals_because_different_types "bytes vs non-bytes" a b
   | Literal_unit, Literal_unit -> ok ()
-  | Literal_unit, _ -> simple_fail "unit vs non-unit"
+  | Literal_unit, _ -> fail @@ different_literals_because_different_types "unit vs non-unit" a b
   | Literal_address a, Literal_address b when a = b -> ok ()
-  | Literal_address _, Literal_address _ -> simple_fail "different addresss"
-  | Literal_address _, _ -> simple_fail "address vs non-address"
-  | Literal_operation _, Literal_operation _ -> simple_fail "can't compare operations"
-  | Literal_operation _, _ -> simple_fail "operation vs non-operation"
+  | Literal_address _, Literal_address _ -> fail @@ different_literals "different addresss" a b
+  | Literal_address _, _ -> fail @@ different_literals_because_different_types "address vs non-address" a b
+  | Literal_operation _, Literal_operation _ -> fail @@ error_uncomparable_literals "can't compare operations" a b
+  | Literal_operation _, _ -> fail @@ different_literals_because_different_types "operation vs non-operation" a b
 
 
 let rec assert_value_eq (a, b: (value*value)) : unit result =
@@ -275,13 +321,13 @@ let rec assert_value_eq (a, b: (value*value)) : unit result =
       assert_literal_eq (a, b)
   | E_constant (ca, lsta), E_constant (cb, lstb) when ca = cb -> (
       let%bind lst =
-        generic_try (simple_error "constants with different number of elements")
+        generic_try (different_size_values "constants with different number of elements" a b)
           (fun () -> List.combine lsta lstb) in
       let%bind _all = bind_list @@ List.map assert_value_eq lst in
       ok ()
     )
   | E_constant _, E_constant _ ->
-      simple_fail "different constants"
+      fail @@ different_values "constants" a b
   | E_constant _, _ ->
       let error_content () =
         Format.asprintf "%a vs %a"
@@ -295,34 +341,34 @@ let rec assert_value_eq (a, b: (value*value)) : unit result =
       ok ()
     )
   | E_constructor _, E_constructor _ ->
-      simple_fail "different constructors"
+      fail @@ different_values "constructors" a b
   | E_constructor _, _ ->
-      simple_fail "comparing constructor with other stuff"
+      fail @@ different_values_because_different_types "constructor vs. non-constructor" a b
 
   | E_tuple lsta, E_tuple lstb -> (
       let%bind lst =
-        generic_try (simple_error "tuples with different number of elements")
+        generic_try (different_size_values "tuples with different number of elements" a b)
           (fun () -> List.combine lsta lstb) in
       let%bind _all = bind_list @@ List.map assert_value_eq lst in
       ok ()
     )
   | E_tuple _, _ ->
-      simple_fail "comparing tuple with other stuff"
+      fail @@ different_values_because_different_types "tuple vs. non-tuple" a b
 
   | E_record sma, E_record smb -> (
-      let aux _ a b =
+      let aux k a b =
         match a, b with
         | Some a, Some b -> Some (assert_value_eq (a, b))
-        | _ -> Some (simple_fail "different record keys")
+        | _              -> Some (fail @@ missing_key_in_record_value k)
       in
       let%bind _all = bind_smap @@ SMap.merge aux sma smb in
       ok ()
     )
   | E_record _, _ ->
-      simple_fail "comparing record with other stuff"
+      fail @@ (different_values_because_different_types "record vs. non-record" a b)
 
   | E_map lsta, E_map lstb -> (
-      let%bind lst = generic_try (simple_error "maps of different lengths")
+      let%bind lst = generic_try (different_size_values "maps of different lengths" a b)
           (fun () ->
              let lsta' = List.sort compare lsta in
              let lstb' = List.sort compare lstb in
@@ -335,27 +381,27 @@ let rec assert_value_eq (a, b: (value*value)) : unit result =
       ok ()
     )
   | E_map _, _ ->
-      simple_fail "comparing map with other stuff"
+      fail @@ different_values_because_different_types "map vs. non-map" a b
 
   | E_list lsta, E_list lstb -> (
       let%bind lst =
-        generic_try (simple_error "list of different lengths")
+        generic_try (different_size_values "lists of different lengths" a b)
           (fun () -> List.combine lsta lstb) in
       let%bind _all = bind_map_list assert_value_eq lst in
       ok ()
     )
   | E_list _, _ ->
-      simple_fail "comparing list with other stuff"
+      fail @@ different_values_because_different_types "list vs. non-list" a b
   | (E_literal _, _) | (E_variable _, _) | (E_application _, _)
   | (E_lambda _, _) | (E_let_in _, _) | (E_tuple_accessor _, _)
   | (E_record_accessor _, _)
   | (E_look_up _, _) | (E_matching _, _) | (E_failwith _, _)
   | (E_assign _ , _)
-  | (E_sequence _, _) | (E_loop _, _)-> simple_fail "comparing not a value"
+  | (E_sequence _, _) | (E_loop _, _)-> fail @@ error_uncomparable_values "can't compare sequences nor loops" a b
 
-let merge_annotation (a:type_value option) (b:type_value option) : type_value result =
+let merge_annotation (a:type_value option) (b:type_value option) err : type_value result =
   match a, b with
-  | None, None -> simple_fail "no annotation"
+  | None, None -> fail @@ err
   | Some a, None -> ok a
   | None, Some b -> ok b
   | Some a, Some b ->
diff --git a/src/typer/typer.ml b/src/typer/typer.ml
index 1779837ce..61d2c8caf 100644
--- a/src/typer/typer.ml
+++ b/src/typer/typer.ml
@@ -504,7 +504,7 @@ and type_expression : environment -> ?tv_opt:O.type_value -> I.expression -> O.a
             @@ List.map fst lst' in
           let%bind annot = bind_map_option get_t_map_key tv_opt in
           trace (simple_info "empty map expression without a type annotation") @@
-          O.merge_annotation annot sub
+          O.merge_annotation annot sub (needs_annotation ae "this map literal")
         in
         let%bind value_type =
           let%bind sub =
@@ -513,7 +513,7 @@ and type_expression : environment -> ?tv_opt:O.type_value -> I.expression -> O.a
             @@ List.map snd lst' in
           let%bind annot = bind_map_option get_t_map_value tv_opt in
           trace (simple_info "empty map expression without a type annotation") @@
-          O.merge_annotation annot sub
+          O.merge_annotation annot sub (needs_annotation ae "this map literal")
         in
         ok (t_map key_type value_type ())
       in
@@ -710,7 +710,11 @@ and type_expression : environment -> ?tv_opt:O.type_value -> I.expression -> O.a
   | E_annotation (expr , te) ->
     let%bind tv = evaluate_type e te in
     let%bind expr' = type_expression ~tv_opt:tv e expr in
-    let%bind type_annotation = O.merge_annotation (Some tv) (Some expr'.type_annotation) in
+    let%bind type_annotation =
+      O.merge_annotation
+        (Some tv)
+        (Some expr'.type_annotation)
+        (simple_error "assertion failed") in
     ok {expr' with type_annotation}