errors for compare in the new typer

src/passes/09-typing/08-typer-common/errors.ml

@@ -1,6 +1,7 @@
 open Trace
 open Simple_utils.Display
 
+
 let stage = "typer"
 
 type typer_error = [
@@ -70,6 +71,27 @@ type typer_error = [
   | `Typer_match_variant_tracer of Ast_core.matching_expr * typer_error
   | `Typer_unrecognized_type_operator of Ast_core.type_expression
   | `Typer_expected_ascription of Ast_core.expression
+  | `Typer_different_kinds of Ast_typed.type_expression * Ast_typed.type_expression
+  | `Typer_different_constants of Ast_typed.type_constant * Ast_typed.type_constant
+  | `Typer_different_operators of Ast_typed.type_operator * Ast_typed.type_operator
+  | `Typer_operator_number_of_arguments of Ast_typed.type_operator * Ast_typed.type_operator * int * int
+  | `Typer_different_record_props of
+    Ast_typed.type_expression * Ast_typed.type_expression * Ast_typed.te_lmap * Ast_typed.te_lmap * string * string
+  | `Typer_different_kind_record_tuple of
+    Ast_typed.type_expression * Ast_typed.type_expression * Ast_typed.te_lmap * Ast_typed.te_lmap
+  | `Typer_different_size_records_tuples of
+    Ast_typed.type_expression * Ast_typed.type_expression * Ast_typed.te_lmap * Ast_typed.te_lmap
+  | `Typer_different_size_sums of
+    Ast_typed.type_expression * Ast_typed.type_expression
+  | `Typer_different_types of string * Ast_typed.type_expression * Ast_typed.type_expression * typer_error
+  | `Typer_different_literals of string * Ast_typed.literal * Ast_typed.literal
+  | `Typer_different_values of string * Ast_typed.expression * Ast_typed.expression
+  | `Typer_different_literals_because_different_types of string * Ast_typed.literal * Ast_typed.literal
+  | `Typer_different_values_because_different_types of string * Ast_typed.expression * Ast_typed.expression
+  | `Typer_uncomparable_literals of string * Ast_typed.literal * Ast_typed.literal
+  | `Typer_uncomparable_values of string * Ast_typed.expression * Ast_typed.expression
+  | `Typer_missing_key_in_record_value of string
+  | `Typer_compare_tracer of typer_error
 ]
 
 let michelson_comb_no_record (loc:Location.t) = `Typer_michelson_comb_no_record loc
@@ -150,6 +172,23 @@ let constant_declaration_tracer (name: Ast_core.expression_variable) (ae:Ast_cor
   `Typer_constant_decl_tracer (name,ae,expected,err)
 let in_match_variant_tracer (ae:Ast_core.matching_expr) (err:typer_error) =
   `Typer_match_variant_tracer (ae,err)
+let different_kinds a b = `Typer_different_kinds (a,b)
+let different_constants a b = `Typer_different_constants (a,b)
+let different_operators a b = `Typer_different_operators (a,b)
+let different_operator_number_of_arguments opa opb lena lenb = `Typer_operator_number_of_arguments (opa, opb, lena, lenb)
+let different_props_in_record a b ra rb ka kb = `Typer_different_record_props (a,b,ra,rb,ka,kb)
+let different_kind_record_tuple a b ra rb = `Typer_different_kind_record_tuple (a,b,ra,rb)
+let different_size_records_tuples a b ra rb = `Typer_different_size_records_tuples (a,b,ra,rb)
+let different_size_sums a b = `Typer_different_size_sums (a,b)
+let different_types name a b err = `Typer_different_types (name,a,b,err)
+let different_literals name a b = `Typer_different_literals (name,a,b)
+let different_values name a b = `Typer_different_values (name,a,b)
+let different_literals_because_different_types name a b = `Typer_different_literals_because_different_types (name,a,b)
+let different_values_because_different_types name a b = `Typer_different_values_because_different_types (name,a,b)
+let error_uncomparable_literals name a b = `Typer_uncomparable_literals (name,a,b)
+let error_uncomparable_values name a b = `Typer_uncomparable_values (name,a,b)
+let missing_key_in_record_value k = `Typer_missing_key_in_record_value k
+let compare_tracer err = `Typer_compare_tracer err
 
 let rec error_ppformat : display_format:string display_format ->
   Format.formatter -> typer_error -> unit =
@@ -470,6 +509,75 @@ let rec error_ppformat : display_format:string display_format ->
         "@[<hv>%a@ expected ascription but got %a@]"
         Location.pp t.location
         Ast_core.PP.expression t
+    | `Typer_different_kinds (a,b) ->
+      Format.fprintf f
+        "@[<hv> different kinds %a@ %a@]"
+        Ast_typed.PP.type_expression a
+        Ast_typed.PP.type_expression b
+    | `Typer_different_constants (a,b) ->
+      Format.fprintf f
+        "@[<hv> different type constructors.@ \
+        Expected these two constant type constructors to be the same, but they're different@ %a@ %a@]"
+        Ast_typed.PP.type_constant a
+        Ast_typed.PP.type_constant b
+    | `Typer_different_operators (a,b) ->
+      Format.fprintf f
+        "@[<hv> different type constructors.@ \
+        Expected these two n-ary type constructors to be the same, but they're different@ %a@ %a@]"
+        (Ast_typed.PP.type_operator Ast_typed.PP.type_expression) a
+        (Ast_typed.PP.type_operator Ast_typed.PP.type_expression) b
+    | `Typer_operator_number_of_arguments (opa, _opb, lena, lenb) ->
+      Format.fprintf f
+        "@[<hv> different number of arguments to type constructors.@ \
+        Expected these two n-ary type constructors to be the same, but they have different number\
+        of arguments (both use the %s type constructor, but they have %d and %d arguments, respectively)@]"
+        (Ast_typed.Helpers.type_operator_name opa) lena lenb
+    | `Typer_different_record_props (_a,_b,ra,rb,_ka,_kb) ->
+      let names = if Ast_typed.Helpers.is_tuple_lmap ra &&Ast_typed.Helpers.is_tuple_lmap rb
+        then "tuples" else "records" in
+      Format.fprintf f
+        "@[<hv> different keys in %s@]"
+        names
+    | `Typer_different_kind_record_tuple (_a,_b,ra,rb) ->
+      let name_a = if Ast_typed.Helpers.is_tuple_lmap ra then "tuple" else "record" in
+      let name_b = if Ast_typed.Helpers.is_tuple_lmap rb then "tuple" else "record" in
+      Format.fprintf f
+        "@[<hv> different keys.@ Expected these two types to be the same, but they're different (one is a %s\ 
+        and the other is a %s)@]"
+        name_a name_b
+    | `Typer_different_size_records_tuples (_a,_b,ra,rb) ->
+      let n = if Ast_typed.Helpers.is_tuple_lmap ra && Ast_typed.Helpers.is_tuple_lmap rb
+        then "tuples" else "records" in
+      Format.fprintf f 
+        "@[<hv> %s have different sizes.@ Expected these two types to be the same, but they're \
+        different (both are %s, but with a different number of arguments)@]"
+        n n
+    | `Typer_different_size_sums (_a,_b) ->
+      Format.fprintf f 
+        "@[<hv> sum types have different sizes.@ Expected these two types to be the same, but they're \
+        different"
+    | `Typer_different_types (name,_a,_b,err) ->
+      Format.fprintf f
+      "@[<hv> %s are different.\ 
+      Expected these two types to be the same, but they're different.@ %a@]"
+      name
+      (error_ppformat ~display_format) err
+    | `Typer_different_literals (name,_a,_b) ->
+      Format.fprintf f "@[<hv> %s are different@]" name
+    | `Typer_different_values (name,_a,_b) ->
+      Format.fprintf f "@[<hv> %s are different@]" name
+    | `Typer_different_literals_because_different_types (name,_a,_b) ->
+      Format.fprintf f "@[<hv> Literals have different types: %s@]" name
+    | `Typer_different_values_because_different_types (name,_a,_b) ->
+      Format.fprintf f "@[<hv> Values have different types: %s@]" name
+    | `Typer_uncomparable_literals (name,_a,_b) ->
+      Format.fprintf f "@[<hv> %s are not comparable @]" name
+    | `Typer_uncomparable_values (name,_a,_b) ->
+      Format.fprintf f "@[<hv> %s are not comparable @]" name
+    | `Typer_missing_key_in_record_value k ->
+      Format.fprintf f "@[<hv> missing %s in one of the record @]" k
+    | `Typer_compare_tracer err ->
+      error_ppformat ~display_format f err 
   )
 
 let rec error_jsonformat : typer_error -> J.t = fun a ->
@@ -1151,3 +1259,189 @@ let rec error_jsonformat : typer_error -> J.t = fun a ->
       ("value", value) ;
     ] in
     json_error ~stage ~content
+  | `Typer_different_kinds (a,b) ->
+    let message = `String "different kinds" in
+    let a = `String (Format.asprintf "%a" Ast_typed.PP.type_expression a) in
+    let b = `String (Format.asprintf "%a" Ast_typed.PP.type_expression b) in
+    let content = `Assoc [
+      ("message", message) ;
+      ("a", a) ;
+      ("b", b) ;
+    ] in
+    json_error ~stage ~content
+  | `Typer_different_constants (a,b) ->
+    let message = `String "different type constructors.\
+      Expected these two constant type constructors to be the same, but they're different" in
+    let a = `String (Format.asprintf "%a" Ast_typed.PP.type_constant a) in
+    let b = `String (Format.asprintf "%a" Ast_typed.PP.type_constant b) in
+    let content = `Assoc [
+      ("message", message) ;
+      ("a", a) ;
+      ("b", b) ;
+    ] in
+    json_error ~stage ~content
+  | `Typer_different_operators (a,b) ->
+    let message = `String "different type constructors.\
+      Expected these two n-ary type constructors to be the same, but they're different" in
+    let a = `String (Format.asprintf "%a" (Ast_typed.PP.type_operator Ast_typed.PP.type_expression) a) in
+    let b = `String (Format.asprintf "%a" (Ast_typed.PP.type_operator Ast_typed.PP.type_expression) b) in
+    let content = `Assoc [
+      ("message", message) ;
+      ("a", a) ;
+      ("b", b) ;
+    ] in
+    json_error ~stage ~content
+  | `Typer_operator_number_of_arguments (opa, opb, lena, lenb) ->
+    let message = `String "different number of arguments to type constructors.\ 
+      Expected these two n-ary type constructors to be the same, but they have different number\ 
+      of arguments" in
+    let a = `String (Format.asprintf "%a" (Ast_typed.PP.type_operator Ast_typed.PP.type_expression) opa) in
+    let b = `String (Format.asprintf "%a" (Ast_typed.PP.type_operator Ast_typed.PP.type_expression) opb) in
+    let op = `String (Ast_typed.Helpers.type_operator_name opa) in
+    let len_a = `Int lena in
+    let len_b = `Int lenb in
+    let content = `Assoc [
+      ("message", message) ;
+      ("a", a) ;
+      ("b", b) ;
+      ("op", op) ;
+      ("len_a", len_a) ;
+      ("len_b", len_b) ;
+    ] in
+    json_error ~stage ~content
+  | `Typer_different_record_props (a,b,ra,rb,ka,kb) ->
+    let names = if Ast_typed.Helpers.is_tuple_lmap ra &&Ast_typed.Helpers.is_tuple_lmap rb
+      then "tuples" else "records" in
+    let message = `String ("different keys in " ^ names) in
+    let a = `String (Format.asprintf "%a" Ast_typed.PP.type_expression a) in
+    let b = `String (Format.asprintf "%a" Ast_typed.PP.type_expression b) in
+    let content = `Assoc [
+      ("message", message) ;
+      ("a", a) ;
+      ("b", b) ;
+      ("ka", `String ka) ;
+      ("kb", `String kb) ;
+    ] in
+    json_error ~stage ~content
+  | `Typer_different_kind_record_tuple (a,b,ra,rb) ->
+    let name_a = if Ast_typed.Helpers.is_tuple_lmap ra then "tuple" else "record" in
+    let name_b = if Ast_typed.Helpers.is_tuple_lmap rb then "tuple" else "record" in
+    let message = `String ("different keys. Expected these two types to be the same, but they're different (one is a "
+      ^ name_a ^ " and the other is a " ^ name_b ^ ")") in
+    let a = `String (Format.asprintf "%a" Ast_typed.PP.type_expression a) in
+    let b = `String (Format.asprintf "%a" Ast_typed.PP.type_expression b) in
+    let content = `Assoc [
+      ("message", message) ;
+      ("a", a) ;
+      ("b", b) ;
+    ] in
+    json_error ~stage ~content
+  | `Typer_different_size_records_tuples (a,b,ra,rb) ->
+    let n = if Ast_typed.Helpers.is_tuple_lmap ra && Ast_typed.Helpers.is_tuple_lmap rb
+       then "tuples" else "records" in
+    let message = `String (n^ " have different sizes. Expected these two types to be the same, but they're \
+      different (both are " ^ n ^ ", but with a different number of arguments)") in
+    let a = `String (Format.asprintf "%a" Ast_typed.PP.type_expression a) in
+    let b = `String (Format.asprintf "%a" Ast_typed.PP.type_expression b) in
+    let content = `Assoc [
+      ("message", message) ;
+      ("a", a) ;
+      ("b", b) ;
+    ] in
+    json_error ~stage ~content
+  | `Typer_different_size_sums (a,b) ->
+    let message = `String (" sum types have different sizes. Expected these two types to be the same, but they're \
+      different") in
+    let a = `String (Format.asprintf "%a" Ast_typed.PP.type_expression a) in
+    let b = `String (Format.asprintf "%a" Ast_typed.PP.type_expression b) in
+    let content = `Assoc [
+      ("message", message) ;
+      ("a", a) ;
+      ("b", b) ;
+    ] in
+    json_error ~stage ~content
+  | `Typer_different_types (name,a,b,err) ->
+    let message = `String (name ^" are different.\ 
+      Expected these two types to be the same, but they're different") in
+    let a = `String (Format.asprintf "%a" Ast_typed.PP.type_expression a) in
+    let b = `String (Format.asprintf "%a" Ast_typed.PP.type_expression b) in
+    let content = `Assoc [
+      ("message", message) ;
+      ("a", a) ;
+      ("b", b) ;
+      ("children", error_jsonformat err)
+    ] in
+    json_error ~stage ~content
+  | `Typer_different_literals (name,a,b) ->
+    let message = `String (name ^ " are different") in
+    let a = `String (Format.asprintf "%a" Ast_typed.PP.literal a) in
+    let b = `String (Format.asprintf "%a" Ast_typed.PP.literal b) in
+    let content = `Assoc [
+      ("message", message) ;
+      ("a", a) ;
+      ("b", b) ;
+    ] in
+    json_error ~stage ~content
+  | `Typer_different_values (name,a,b) ->
+    let message = `String (name ^ " are different") in
+    let a = `String (Format.asprintf "%a" Ast_typed.PP.expression a) in
+    let b = `String (Format.asprintf "%a" Ast_typed.PP.expression b) in
+    let content = `Assoc [
+      ("message", message) ;
+      ("a", a) ;
+      ("b", b) ;
+    ] in
+    json_error ~stage ~content
+  | `Typer_different_literals_because_different_types (name,a,b) ->
+    let message = `String ("literals have different types: " ^ name) in
+    let a = `String (Format.asprintf "%a" Ast_typed.PP.literal a) in
+    let b = `String (Format.asprintf "%a" Ast_typed.PP.literal b) in
+    let content = `Assoc [
+      ("message", message) ;
+      ("a", a) ;
+      ("b", b) ;
+    ] in
+    json_error ~stage ~content
+  | `Typer_different_values_because_different_types (name,a,b) ->
+    let message = `String ("values have different types: " ^ name) in
+    let a = `String (Format.asprintf "%a" Ast_typed.PP.expression a) in
+    let b = `String (Format.asprintf "%a" Ast_typed.PP.expression b) in
+    let content = `Assoc [
+      ("message", message) ;
+      ("a", a) ;
+      ("b", b) ;
+    ] in
+    json_error ~stage ~content
+  | `Typer_uncomparable_literals (name,a,b) ->
+    let message = `String (name ^ " are not comparable") in
+    let a = `String (Format.asprintf "%a" Ast_typed.PP.literal a) in
+    let b = `String (Format.asprintf "%a" Ast_typed.PP.literal b) in
+    let content = `Assoc [
+      ("message", message) ;
+      ("a", a) ;
+      ("b", b) ;
+    ] in
+    json_error ~stage ~content
+  | `Typer_uncomparable_values (name,a,b) ->
+    let message = `String (name ^ " are not comparable") in
+    let a = `String (Format.asprintf "%a" Ast_typed.PP.expression a) in
+    let b = `String (Format.asprintf "%a" Ast_typed.PP.expression b) in
+    let content = `Assoc [
+      ("message", message) ;
+      ("a", a) ;
+      ("b", b) ;
+    ] in
+    json_error ~stage ~content
+  | `Typer_missing_key_in_record_value k ->
+    let message = `String "missing keys in one of the records" in
+    let content = `Assoc [
+      ("message", message) ;
+      ("missing_key", `String k) ;
+    ] in
+    json_error ~stage ~content
+  | `Typer_compare_tracer err ->
+    let content = `Assoc [
+      ("message", `String "not equal") ;
+      ("children", error_jsonformat err)
+    ] in
+    json_error ~stage ~content

src/passes/09-typing/08-typer-new/compare.ml

@@ -0,0 +1,165 @@
+open Ast_typed
+open Trace
+open Typer_common.Errors
+
+let rec assert_type_expression_eq (a, b: (type_expression * type_expression)) : (unit, typer_error) result = match (a.type_content, b.type_content) with
+  | T_constant ca, T_constant cb -> (
+      Assert.assert_true (different_constants ca cb) (ca = cb)
+    )
+  | T_constant _, _ -> fail @@ different_kinds a b
+  | T_operator opa, T_operator opb -> (
+    let%bind (lsta, lstb) = match (opa, opb) with
+      | TC_option la, TC_option lb
+      | TC_list la, TC_list lb
+      | TC_contract la, TC_contract lb
+      | TC_set la, TC_set lb -> ok @@ ([la], [lb])
+      | (TC_map {k=ka;v=va} | TC_map_or_big_map {k=ka;v=va}), (TC_map {k=kb;v=vb} | TC_map_or_big_map {k=kb;v=vb})
+      | (TC_big_map {k=ka;v=va} | TC_map_or_big_map {k=ka;v=va}), (TC_big_map {k=kb;v=vb} | TC_map_or_big_map {k=kb;v=vb})
+        -> ok @@ ([ka;va] ,[kb;vb]) 
+      | (TC_option _ | TC_list _ | TC_contract _ | TC_set _ | TC_map _ | TC_big_map _ | TC_map_or_big_map _ ),
+        (TC_option _ | TC_list _ | TC_contract _ | TC_set _ | TC_map _ | TC_big_map _ | TC_map_or_big_map _ )
+        -> fail @@ different_operators opa opb
+      in
+      if List.length lsta <> List.length lstb then
+        fail @@ different_operator_number_of_arguments opa opb (List.length lsta) (List.length lstb)
+      else
+        trace (different_types "arguments to type operators" a b)
+        @@ bind_list_iter (fun (a,b) -> assert_type_expression_eq (a,b) )(List.combine lsta lstb)
+  )
+  | T_operator _, _ -> fail @@ different_kinds a b
+  | T_sum sa, T_sum sb -> (
+      let sa' = CMap.to_kv_list sa in
+      let sb' = CMap.to_kv_list sb in
+      let aux ((ka, {ctor_type=va;_}), (kb, {ctor_type=vb;_})) =
+        let%bind _ =
+          Assert.assert_true (corner_case "different keys in sum types")
+          @@ (ka = kb) in
+        assert_type_expression_eq (va, vb)
+      in
+      let%bind _ =
+        Assert.assert_list_same_size (different_size_sums a b)
+        sa' sb'
+      in
+      trace (different_types "sum type" a b) @@
+      bind_list_iter aux (List.combine sa' sb')
+    )
+  | T_sum _, _ -> fail @@ different_kinds a b
+  | T_record ra, T_record rb
+       when Helpers.is_tuple_lmap ra <> Helpers.is_tuple_lmap rb -> (
+    fail @@ different_kind_record_tuple a b ra rb
+  )
+  | T_record ra, T_record rb -> (
+      let sort_lmap r' = List.sort (fun (Label a,_) (Label b,_) -> String.compare a b) r' in
+      let ra' = sort_lmap @@ LMap.to_kv_list ra in
+      let rb' = sort_lmap @@ LMap.to_kv_list rb in
+      let aux ((ka, {field_type=va;_}), (kb, {field_type=vb;_})) =
+        let%bind _ =
+          trace (different_types "records" a b) @@
+          let Label ka = ka in
+          let Label kb = kb in
+          Assert.assert_true (different_props_in_record a b ra rb ka kb) (ka = kb) in
+        assert_type_expression_eq (va, vb)
+      in
+      let%bind _ =
+        Assert.assert_list_same_size (different_size_records_tuples a b ra rb) ra' rb' in
+      trace (different_types "record type" a b)
+      @@ bind_list_iter aux (List.combine ra' rb')
+
+    )
+  | T_record _, _ -> fail @@ different_kinds a b
+  | T_arrow {type1;type2}, T_arrow {type1=type1';type2=type2'} ->
+      let%bind _ = assert_type_expression_eq (type1, type1') in
+      let%bind _ = assert_type_expression_eq (type2, type2') in
+      ok ()
+  | T_arrow _, _ -> fail @@ different_kinds a b
+  | T_variable x, T_variable y -> let _ = (x = y) in failwith "TODO : we must check that the two types were bound at the same location (even if they have the same name), i.e. use something like De Bruijn indices or a propper graph encoding"
+  | T_variable _, _ -> fail @@ different_kinds a b
+
+(* No information about what made it fail *)
+let type_expression_eq ab = Trace.to_bool @@ assert_type_expression_eq ab
+
+let assert_literal_eq (a, b : literal * literal) : (unit, typer_error) result =
+  match (a, b) with
+  | Literal_int a, Literal_int b when a = b -> ok ()
+  | 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 _ -> fail @@ different_literals "different nats" a b
+  | Literal_nat _, _ -> fail @@ different_literals_because_different_types "nat vs non-nat" a b
+  | Literal_timestamp a, Literal_timestamp b when a = b -> ok ()
+  | Literal_timestamp _, Literal_timestamp _ -> fail @@ different_literals "different timestamps" a b
+  | Literal_timestamp _, _ -> fail @@ different_literals_because_different_types "timestamp vs non-timestamp" a b
+  | Literal_mutez a, Literal_mutez b when a = b -> ok ()
+  | Literal_mutez _, Literal_mutez _ -> fail @@ different_literals "different tezs" a b
+  | Literal_mutez _, _ -> 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 _ -> 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 _ -> fail @@ different_literals "different bytes" a b
+  | Literal_bytes _, _ -> fail @@ different_literals_because_different_types "bytes vs non-bytes" a b
+  | Literal_void, Literal_void -> ok ()
+  | Literal_void, _ -> fail @@ different_literals_because_different_types "void vs non-void" a b
+  | Literal_unit, Literal_unit -> ok ()
+  | 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 _ -> fail @@ different_literals "different addresss" a b
+  | Literal_address _, _ -> fail @@ different_literals_because_different_types "address vs non-address" a b
+  | Literal_signature a, Literal_signature b when a = b -> ok ()
+  | Literal_signature _, Literal_signature _ -> fail @@ different_literals "different signature" a b
+  | Literal_signature _, _ -> fail @@ different_literals_because_different_types "signature vs non-signature" a b
+  | Literal_key a, Literal_key b when a = b -> ok ()
+  | Literal_key _, Literal_key _ -> fail @@ different_literals "different key" a b
+  | Literal_key _, _ -> fail @@ different_literals_because_different_types "key vs non-key" a b
+  | Literal_key_hash a, Literal_key_hash b when a = b -> ok ()
+  | Literal_key_hash _, Literal_key_hash _ -> fail @@ different_literals "different key_hash" a b
+  | Literal_key_hash _, _ -> fail @@ different_literals_because_different_types "key_hash vs non-key_hash" a b
+  | Literal_chain_id a, Literal_chain_id b when a = b -> ok ()
+  | Literal_chain_id _, Literal_chain_id _ -> fail @@ different_literals "different chain_id" a b
+  | Literal_chain_id _, _ -> fail @@ different_literals_because_different_types "chain_id vs non-chain_id" 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: (expression*expression)) : (unit, typer_error) result =
+  trace compare_tracer @@
+  match (a.expression_content, b.expression_content) with
+  | E_literal a, E_literal b ->
+      assert_literal_eq (a, b)
+  | E_constant {cons_name=ca;arguments=lsta}, E_constant {cons_name=cb;arguments=lstb} when ca = cb -> (
+      let%bind lst =
+        generic_try (corner_case "constants with different number of elements")
+          (fun () -> List.combine lsta lstb) in
+      let%bind _all = bind_list @@ List.map assert_value_eq lst in
+      ok ()
+    )
+  | E_constant _, E_constant _ ->
+      fail @@ different_values "constants" a b
+  | E_constant _, _ ->
+      fail @@ (corner_case "comparing constant with other stuff")
+
+  | E_constructor {constructor=ca;element=a}, E_constructor {constructor=cb;element=b} when ca = cb -> (
+      let%bind _eq = assert_value_eq (a, b) in
+      ok ()
+    )
+  | E_constructor _, E_constructor _ ->
+      fail @@ different_values "constructors" a b
+  | E_constructor _, _ ->
+      fail @@ different_values_because_different_types "constructor vs. non-constructor" a b
+  | E_record sma, E_record smb -> (
+      let aux (Label k) a b =
+        match a, b with
+        | Some a, Some b -> Some (assert_value_eq (a, b))
+        | _              -> Some (fail @@ missing_key_in_record_value k)
+      in
+      let%bind _all = Helpers.bind_lmap @@ LMap.merge aux sma smb in
+      ok ()
+    )
+  | E_record _, _ ->
+      fail @@ (different_values_because_different_types "record vs. non-record" a b)
+
+  | (E_literal _, _) | (E_variable _, _) | (E_application _, _)
+  | (E_lambda _, _) | (E_let_in _, _) | (E_raw_code _, _) | (E_recursive _, _)
+  | (E_record_accessor _, _) | (E_record_update _,_)
+  | (E_matching _, _)
+  -> fail @@ error_uncomparable_values "can't compare sequences nor loops" a b

src/passes/09-typing/08-typer-new/typer.ml

@@ -14,8 +14,7 @@ module Map = RedBlackTrees.PolyMap
 open Todo_use_fold_generator
 
 let assert_type_expression_eq ((tv',tv):O.type_expression * O.type_expression) : (unit,typer_error) result = 
-  trace_option (assert_equal tv' tv) @@
+  Compare.assert_type_expression_eq (tv' , tv)
-    O.assert_type_expression_eq (tv' , tv)
 
 (*
   Extract pairs of (name,type) in the declaration and add it to the environment
@@ -67,8 +66,8 @@ and type_match : environment -> O'.typer_state -> O.type_expression -> I.matchin
           let%bind acc = match acc with
             | None -> ok (Some variant)
             | Some variant' ->
-                let%bind () = trace_option (not_matching variant variant') @@
+                let%bind () =
-                  Ast_typed.assert_type_expression_eq (variant , variant') in
+                  assert_type_expression_eq (variant , variant') in
                 ok (Some variant)
             in
           ok acc in

vendors/ligo-utils/simple-utils/trace.ml

@@ -546,6 +546,9 @@ module Assert = struct
   let assert_list_empty err lst =
     assert_true err List.(length lst = 0)
   
+  let assert_list_same_size err lsta lstb =
+    assert_true err List.(length lsta = length lstb)
+
 end
 
 let json_of_error = J.to_string