%%% -*- erlang-indent-level:4; indent-tabs-mode: nil -*-
%%%-------------------------------------------------------------------
%%% @copyright (C) 2018, Aeternity Anstalt
%%% @doc Test Sophia language compiler.
%%%
%%% @end
%%%-------------------------------------------------------------------

-module(aeso_compiler_tests).

-compile([export_all, nowarn_export_all]).

-include_lib("eunit/include/eunit.hrl").

run_test(Test) ->
    TestFun = list_to_atom(lists:concat([Test, "_test_"])),
    [ begin
          io:format("~s\n", [Label]),
          Fun()
      end || {Label, Fun} <- ?MODULE:TestFun() ],
    ok.

%%  Very simply test compile the given contracts. Only basic checks
%%  are made on the output, just that it is a binary which indicates
%%  that the compilation worked.
simple_compile_test_() ->
    [ {"Testing the " ++ ContractName ++ " contract",
       fun() ->
           case compile(ContractName) of
               #{fate_code := Code} ->
                   Code1 = aeb_fate_code:deserialize(aeb_fate_code:serialize(Code)),
                   ?assertMatch({X, X}, {Code1, Code});
               Error -> io:format("\n\n~p\n\n", [Error]), print_and_throw(Error)
           end
       end} || ContractName <- compilable_contracts()] ++
    [ {"Test file not found error",
       fun() ->
           {error, Errors} = aeso_compiler:file("does_not_exist.aes"),
           ExpErr = <<"File error:\ndoes_not_exist.aes: no such file or directory">>,
           check_errors([ExpErr], Errors)
       end} ] ++
    [ {"Testing error messages of " ++ ContractName,
       fun() ->
           Errors = compile(ContractName, [warn_all, warn_error]),
           check_errors(ExpectedErrors, Errors)
       end} ||
           {ContractName, ExpectedErrors} <- failing_contracts() ] ++
    [ {"Testing include with explicit files",
       fun() ->
           FileSystem = maps:from_list(
               [ begin
                   {ok, Bin} = file:read_file(filename:join([aeso_test_utils:contract_path(), File])),
                   {File, Bin}
                 end || File <- ["included.aes", "../contracts/included2.aes"] ]),
           #{byte_code := Code1} = compile("include", [{include, {explicit_files, FileSystem}}]),
           #{byte_code := Code2} = compile("include"),
           ?assertMatch(true, Code1 == Code2)
       end} ] ++
    [ {"Testing deadcode elimination",
       fun() ->
           #{ byte_code := NoDeadCode } = compile("nodeadcode"),
           #{ byte_code := DeadCode   } = compile("deadcode"),
           SizeNoDeadCode = byte_size(NoDeadCode),
           SizeDeadCode   = byte_size(DeadCode),
           Delta          = 20,
           ?assertMatch({_, _, true}, {SizeDeadCode, SizeNoDeadCode, SizeDeadCode + Delta < SizeNoDeadCode}),
           ok
       end} ] ++
    [ {"Testing warning messages",
       fun() ->
           #{ warnings := Warnings } = compile("warnings", [warn_all]),
           #{ warnings := [] } = compile("warning_unused_include_no_include", [warn_all]),
           #{ warnings := [] } = compile("warning_used_record_typedef", [warn_all]),
           check_warnings(warnings(), Warnings)
       end} ] ++
    [].

%% Check if all modules in the standard library compile
stdlib_test_() ->
    {ok, Files} = file:list_dir(aeso_stdlib:stdlib_include_path()),
    [ { "Testing " ++ File ++ " from the stdlib",
      fun() ->
          String = "include \"" ++ File ++ "\"\nmain contract Test =\n  entrypoint f(x) = x",
          Options = [{src_file, File}],
          case aeso_compiler:from_string(String, Options) of
              {ok, #{fate_code := Code}} ->
                  Code1 = aeb_fate_code:deserialize(aeb_fate_code:serialize(Code)),
                  ?assertMatch({X, X}, {Code1, Code});
              {error, Error} -> io:format("\n\n~p\n\n", [Error]), print_and_throw(Error)
          end
      end} || File <- Files,
              lists:suffix(".aes", File)
    ].

check_errors(no_error, Actual) -> ?assertMatch(#{}, Actual);
check_errors(Expect, #{}) ->
    ?assertEqual({error, Expect}, ok);
check_errors(Expect0, Actual0) ->
    Expect = lists:sort(Expect0),
    Actual = [ list_to_binary(string:trim(aeso_errors:pp(Err))) || Err <- Actual0 ],
    case {Expect -- Actual, Actual -- Expect} of
        {[], Extra}   -> ?assertMatch({unexpected, []}, {unexpected, Extra});
        {Missing, []} -> ?assertMatch({missing, []}, {missing, Missing});
        {Missing, Extra} -> ?assertEqual(Missing, Extra)
    end.

check_warnings(Expect0, Actual0) ->
    Expect = lists:sort(Expect0),
    Actual = [ list_to_binary(string:trim(aeso_warnings:pp(Warn))) || Warn <- Actual0 ],
    case {Expect -- Actual, Actual -- Expect} of
        {[], Extra}   -> ?assertMatch({unexpected, []}, {unexpected, Extra});
        {Missing, []} -> ?assertMatch({missing, []}, {missing, Missing});
        {Missing, Extra} -> ?assertEqual(Missing, Extra)
    end.

compile(Name) ->
    compile( Name, [{include, {file_system, [aeso_test_utils:contract_path()]}}]).

compile(Name, Options) ->
    String = aeso_test_utils:read_contract(Name),
    Options1 =
        case lists:member(Name, debug_mode_contracts()) of
            true  -> [debug_mode];
            false -> []
        end ++
        [ {src_file, Name ++ ".aes"}
        , {include, {file_system, [aeso_test_utils:contract_path()]}}
        ] ++ Options,
    case aeso_compiler:from_string(String, Options1) of
        {ok, Map}                                        -> Map;
        {error, ErrorString} when is_binary(ErrorString) -> ErrorString;
        {error, Errors}                                  -> Errors
    end.

%% compilable_contracts() -> [ContractName].
%%  The currently compilable contracts.

compilable_contracts() ->
    ["complex_types",
     "counter",
     "dutch_auction",
     "environment",
     "factorial",
     "functions",
     "fundme",
     "identity",
     "maps",
     "oracles",
     "remote_call",
     "remote_call_ambiguous_record",
     "simple",
     "simple_storage",
     "spend_test",
     "stack",
     "test",
     "builtin_bug",
     "builtin_map_get_bug",
     "lc_record_bug",
     "nodeadcode",
     "deadcode",
     "variant_types",
     "state_handling",
     "events",
     "include",
     "relative_include",
     "basic_auth",
     "basic_auth_tx",
     "bitcoin_auth",
     "address_literals",
     "bytes_equality",
     "address_chain",
     "namespace_bug",
     "bytes_to_x",
     "bytes_concat",
     "bytes_misc",
     "aens",
     "aens_update",
     "tuple_match",
     "cyclic_include",
     "stdlib_include",
     "double_include",
     "manual_stdlib_include",
     "list_comp",
     "payable",
     "unapplied_builtins",
     "underscore_number_literals",
     "pairing_crypto",
     "qualified_constructor",
     "let_patterns",
     "lhs_matching",
     "more_strings",
     "protected_call",
     "hermetization_turnoff",
     "multiple_contracts",
     "clone",
     "clone_simple",
     "create",
     "child_contract_init_bug",
     "using_namespace",
     "assign_patterns",
     "patterns_guards",
     "pipe_operator",
     "polymorphism_contract_implements_interface",
     "polymorphism_contract_multi_interface",
     "polymorphism_contract_interface_extends_interface",
     "polymorphism_contract_interface_extensions",
     "polymorphism_contract_interface_same_decl_multi_interface",
     "polymorphism_contract_interface_same_name_same_type",
     "polymorphism_variance_switching_chain_create",
     "polymorphism_variance_switching_void_supertype",
     "polymorphism_variance_switching_unify_with_interface_decls",
     "polymorphism_preserve_or_add_payable_contract",
     "polymorphism_preserve_or_add_payable_entrypoint",
     "polymorphism_preserve_or_remove_stateful_entrypoint",
     "missing_init_fun_state_unit",
     "complex_compare_leq",
     "complex_compare",
     "higher_order_compare",
     "higher_order_map_keys",
     "higher_order_state",
     "polymorphic_compare",
     "polymorphic_entrypoint",
     "polymorphic_entrypoint_return",
     "polymorphic_map_keys",
     "unapplied_contract_call",
     "unapplied_named_arg_builtin",
     "resolve_field_constraint_by_arity",
     "toplevel_constants",
     "ceres",
     "test" % Custom general-purpose test file. Keep it last on the list.
    ].

debug_mode_contracts() ->
    ["hermetization_turnoff"].

%% Contracts that should produce type errors

-define(Pos(Kind, File, Line, Col), (list_to_binary(Kind))/binary, " error in '",
                                    (list_to_binary(File))/binary, ".aes' at line " ??Line ", col " ??Col ":\n").
-define(Pos(Line, Col), ?Pos(__Kind, __File, Line, Col)).

-define(ERROR(Kind, Name, Errs),
    (fun() ->
        __Kind = Kind,
        __File = ??Name,
        {__File, Errs}
     end)()).

-define(TYPE_ERROR(Name, Errs), ?ERROR("Type", Name, Errs)).
-define(PARSE_ERROR(Name, Errs), ?ERROR("Parse", Name, Errs)).

-define(PosW(Kind, File, Line, Col), (list_to_binary(Kind))/binary, " in '",
                                     (list_to_binary(File))/binary, ".aes' at line " ??Line ", col " ??Col ":\n").
-define(PosW(Line, Col), ?PosW(__Kind, __File, Line, Col)).

-define(WARNING(Name, Warns),
    (fun() ->
        __Kind = "Warning",
        __File = ??Name,
        Warns
     end)()).

warnings() ->
    ?WARNING(warnings,
     [<<?PosW(0, 0)
        "The file `Triple.aes` is included but not used.">>,
      <<?PosW(13, 3)
        "The function `h` is defined but never used.">>,
      <<?PosW(19, 3)
        "The type `unused_type` is defined but never used.">>,
      <<?PosW(23, 54)
        "Negative spend.">>,
      <<?PosW(27, 9)
        "The definition of `x` shadows an older definition at line 26, column 9.">>,
      <<?PosW(30, 36)
        "Division by zero.">>,
      <<?PosW(32, 3)
        "The function `unused_stateful` is unnecessarily marked as stateful.">>,
      <<?PosW(35, 31)
        "The variable `unused_arg` is defined but never used.">>,
      <<?PosW(36, 9)
        "The variable `unused_var` is defined but never used.">>,
      <<?PosW(41, 3)
        "The function `unused_function` is defined but never used.">>,
      <<?PosW(42, 3)
        "The function `recursive_unused_function` is defined but never used.">>,
      <<?PosW(43, 3)
        "The function `called_unused_function1` is defined but never used.">>,
      <<?PosW(44, 3)
        "The function `called_unused_function2` is defined but never used.">>,
      <<?PosW(48, 5)
        "Unused return value.">>,
      <<?PosW(60, 5)
        "The function `dec` is defined but never used.">>,
      <<?PosW(73, 9)
        "The definition of `const` shadows an older definition at line 70, column 3.">>,
      <<?PosW(84, 7)
        "The constant `c` is defined but never used.">>
     ]).

failing_contracts() ->
    {ok, V} = aeso_compiler:numeric_version(),
    Version = list_to_binary(string:join([integer_to_list(N) || N <- V], ".")),
    %% Parse errors
    [ ?PARSE_ERROR(field_parse_error,
       [<<?Pos(5, 26)
          "Cannot use nested fields or keys in record construction: p.x">>])
    , ?PARSE_ERROR(vsemi,  [<<?Pos(3, 3) "Unexpected indentation. Did you forget a '}'?">>])
    , ?PARSE_ERROR(vclose, [<<?Pos(4, 3) "Unexpected indentation. Did you forget a ']'?">>])
    , ?PARSE_ERROR(indent_fail, [<<?Pos(3, 2) "Unexpected token 'entrypoint'.">>])
    , ?PARSE_ERROR(assign_pattern_to_pattern, [<<?Pos(3, 22) "Unexpected token '='.">>])

    %% Type errors
    , ?TYPE_ERROR(name_clash,
       [<<?Pos(4, 3)
          "Duplicate definitions of `double_def` at\n"
          "  - line 3, column 3\n"
          "  - line 4, column 3">>,
        <<?Pos(7, 3)
          "Duplicate definitions of `abort` at\n"
          "  - (builtin location)\n"
          "  - line 7, column 3">>,
        <<?Pos(8, 3)
          "Duplicate definitions of `require` at\n"
          "  - (builtin location)\n"
          "  - line 8, column 3">>,
        <<?Pos(9, 3)
          "Duplicate definitions of `put` at\n"
          "  - (builtin location)\n"
          "  - line 9, column 3">>,
        <<?Pos(10, 3)
          "Duplicate definitions of `state` at\n"
          "  - (builtin location)\n"
          "  - line 10, column 3">>])
    , ?TYPE_ERROR(type_errors,
       [<<?Pos(17, 23)
          "Unbound variable `zz`">>,
        <<?Pos(26, 9)
          "Cannot unify `int` and `list(int)`\n"
          "when checking the application of\n"
          "  `(::) : (int, list(int)) => list(int)`\n"
          "to arguments\n"
          "  `x : int`\n"
          "  `x : int`">>,
        <<?Pos(9, 48)
          "Cannot unify `string` and `int`\n"
          "when checking the assignment of the field `x : map(string, string)` "
          "to the old value `__x` and the new value `__x {[\"foo\"] @ x = x + 1} : map(string, int)`">>,
        <<?Pos(34, 47)
          "Cannot unify `int` and `string`\n"
          "when checking the type of the expression `1 : int` "
          "against the expected type `string`">>,
        <<?Pos(34, 52)
          "Cannot unify `string` and `int`\n"
          "when checking the type of the expression `\"bla\" : string` "
          "against the expected type `int`">>,
        <<?Pos(32, 18)
          "Cannot unify `string` and `int`\n"
          "when checking the type of the expression `\"x\" : string` "
          "against the expected type `int`">>,
        <<?Pos(11, 58)
          "Cannot unify `string` and `int`\n"
          "when checking the type of the expression `\"foo\" : string` "
          "against the expected type `int`">>,
        <<?Pos(38, 13)
          "Cannot unify `int` and `string`\n"
          "when comparing the types of the if-branches\n"
          "  - w : int (at line 38, column 13)\n"
          "  - z : string (at line 39, column 10)">>,
        <<?Pos(22, 40)
          "Not a record type: `string`\n"
          "arising from the projection of the field `y`">>,
        <<?Pos(21, 44)
          "Not a record type: `string`\n"
          "arising from an assignment of the field `y`">>,
        <<?Pos(20, 40)
          "Not a record type: `string`\n"
          "arising from an assignment of the field `y`">>,
        <<?Pos(19, 37)
          "Not a record type: `string`\n"
          "arising from an assignment of the field `y`">>,
        <<?Pos(13, 27)
          "Ambiguous record type with field `y` could be one of\n"
          "  - `r` (at line 4, column 10)\n"
          "  - `r'` (at line 5, column 10)">>,
        <<?Pos(26, 7)
          "Repeated name `x` in the pattern `x :: x`">>,
        <<?Pos(44, 14)
          "Repeated names `x`, `y` in the pattern `(x : int, y, x : string, y : bool)`">>,
        <<?Pos(44, 39)
          "Cannot unify `int` and `string`\n"
          "when checking the type of the expression `x : int` "
          "against the expected type `string`">>,
        <<?Pos(44, 72)
          "Cannot unify `int` and `string`\n"
          "when checking the type of the expression `x : int` "
          "against the expected type `string`">>,
        <<?Pos(14, 24)
          "No record type with fields `y`, `z`">>,
        <<?Pos(15, 26)
          "The field `z` is missing when constructing an element of type `r2`">>,
        <<?Pos(15, 24)
          "Record type `r2` does not have field `y`">>,
        <<?Pos(47, 5)
          "Let binding must be followed by an expression.">>,
        <<?Pos(50, 5)
          "Let binding must be followed by an expression.">>,
        <<?Pos(54, 5)
          "Let binding must be followed by an expression.">>,
        <<?Pos(58, 5)
          "Let binding must be followed by an expression.">>,
        <<?Pos(63, 5)
          "Cannot unify `int` and `bool`\n"
          "when checking the type of the expression `id(n) : int` "
          "against the expected type `bool`">>])
    , ?TYPE_ERROR(init_type_error,
       [<<?Pos(7, 3)
          "Cannot unify `string` and `map(int, int)`\n"
          "when checking that `init` returns a value of type `state`">>])
    , ?TYPE_ERROR(missing_state_type,
       [<<?Pos(5, 3)
          "Cannot unify `string` and `unit`\n"
          "when checking that `init` returns a value of type `state`">>])
    , ?TYPE_ERROR(missing_fields_in_record_expression,
       [<<?Pos(7, 42)
          "The field `x` is missing when constructing an element of type `r('a)`">>,
        <<?Pos(8, 42)
          "The field `y` is missing when constructing an element of type `r(int)`">>,
        <<?Pos(6, 42)
          "The fields `y`, `z` are missing when constructing an element of type `r('a)`">>])
    , ?TYPE_ERROR(namespace_clash_builtin,
       [<<?Pos(4, 10)
          "The contract `Call` has the same name as a namespace at (builtin location)">>])
    , ?TYPE_ERROR(namespace_clash_included,
       [<<?Pos(5, 11)
          "The namespace `BLS12_381` has the same name as a namespace at line 1, column 11 in BLS12_381.aes">>])
    , ?TYPE_ERROR(namespace_clash_same_file,
       [<<?Pos(4, 11)
          "The namespace `Nmsp` has the same name as a namespace at line 1, column 11">>])
    , ?TYPE_ERROR(bad_events,
        [<<?Pos(9, 25)
           "The indexed type `string` is not a word type">>,
         <<?Pos(10, 25)
           "The indexed type `alias_string` equals `string` which is not a word type">>])
    , ?TYPE_ERROR(bad_events2,
        [<<?Pos(9, 7)
           "The event constructor `BadEvent1` has too many non-indexed values (max 1)">>,
         <<?Pos(10, 7)
           "The event constructor `BadEvent2` has too many indexed values (max 3)">>])
    , ?TYPE_ERROR(type_clash,
        [<<?Pos(12, 42)
           "Cannot unify `int` and `string`\n"
           "when checking the type of the expression `r.foo() : map(int, string)` "
           "against the expected type `map(string, int)`">>,
         <<?Pos(12, 42)
           "Cannot unify `string` and `int`\n"
           "when checking the type of the expression `r.foo() : map(int, string)` "
           "against the expected type `map(string, int)`">>])
    , ?TYPE_ERROR(not_toplevel_include,
                  [<<?Pos(2, 11)
                     "Include of `included.aes` is not allowed, include only allowed at top level.">>])
    , ?TYPE_ERROR(not_toplevel_namespace,
                  [<<?Pos(2, 13)
                     "Nested namespaces are not allowed. Namespace `Foo` is not defined at top level.">>])
    , ?TYPE_ERROR(not_toplevel_contract,
        [<<?Pos(2, 12)
           "Nested contracts are not allowed. Contract `Con` is not defined at top level.">>])
    , ?TYPE_ERROR(bad_address_literals,
        [<<?Pos(11, 5)
           "Cannot unify `address` and `oracle(int, bool)`\n"
           "when checking the type of the expression `ak_2gx9MEFxKvY9vMG5YnqnXWv1hCsX7rgnfvBLJS4aQurustR1rt : address` "
           "against the expected type `oracle(int, bool)`">>,
         <<?Pos(9, 5)
           "Cannot unify `address` and `Remote`\n"
           "when checking the type of the expression `ak_2gx9MEFxKvY9vMG5YnqnXWv1hCsX7rgnfvBLJS4aQurustR1rt : address` "
           "against the expected type `Remote`">>,
         <<?Pos(7, 5)
           "Cannot unify `address` and `bytes(32)`\n"
           "when checking the type of the expression `ak_2gx9MEFxKvY9vMG5YnqnXWv1hCsX7rgnfvBLJS4aQurustR1rt : address` "
           "against the expected type `bytes(32)`">>,
         <<?Pos(14, 5)
           "Cannot unify `oracle('a, 'b)` and `oracle_query(int, bool)`\n"
           "when checking the type of the expression "
           "`ok_2YNyxd6TRJPNrTcEDCe9ra59SVUdp9FR9qWC5msKZWYD9bP9z5 : oracle('a, 'b)` "
           "against the expected type `oracle_query(int, bool)`">>,
         <<?Pos(16, 5)
           "Cannot unify `oracle('c, 'd)` and `bytes(32)`\n"
           "when checking the type of the expression "
           "`ok_2YNyxd6TRJPNrTcEDCe9ra59SVUdp9FR9qWC5msKZWYD9bP9z5 : oracle('c, 'd)` "
           "against the expected type `bytes(32)`">>,
         <<?Pos(18, 5)
           "Cannot unify `oracle('e, 'f)` and `Remote`\n"
           "when checking the type of the expression "
           "`ok_2YNyxd6TRJPNrTcEDCe9ra59SVUdp9FR9qWC5msKZWYD9bP9z5 : oracle('e, 'f)` "
           "against the expected type `Remote`">>,
         <<?Pos(21, 5)
           "Cannot unify `oracle_query('g, 'h)` and `oracle(int, bool)`\n"
           "when checking the type of the expression "
           "`oq_2oRvyowJuJnEkxy58Ckkw77XfWJrmRgmGaLzhdqb67SKEL1gPY : oracle_query('g, 'h)` "
           "against the expected type `oracle(int, bool)`">>,
         <<?Pos(23, 5)
           "Cannot unify `oracle_query('i, 'j)` and `bytes(32)`\n"
           "when checking the type of the expression "
           "`oq_2oRvyowJuJnEkxy58Ckkw77XfWJrmRgmGaLzhdqb67SKEL1gPY : oracle_query('i, 'j)` "
           "against the expected type `bytes(32)`">>,
         <<?Pos(25, 5)
           "Cannot unify `oracle_query('k, 'l)` and `Remote`\n"
           "when checking the type of the expression "
           "`oq_2oRvyowJuJnEkxy58Ckkw77XfWJrmRgmGaLzhdqb67SKEL1gPY : oracle_query('k, 'l)` "
           "against the expected type `Remote`">>,
         <<?Pos(28, 5)
           "The type `address` is not a contract type\n"
           "when checking that the contract literal "
           "`ct_Ez6MyeTMm17YnTnDdHTSrzMEBKmy7Uz2sXu347bTDPgVH2ifJ` "
           "has the type `address`">>,
         <<?Pos(30, 5)
           "The type `oracle(int, bool)` is not a contract type\n"
           "when checking that the contract literal "
           "`ct_Ez6MyeTMm17YnTnDdHTSrzMEBKmy7Uz2sXu347bTDPgVH2ifJ` "
           "has the type `oracle(int, bool)`">>,
         <<?Pos(32, 5)
           "The type `bytes(32)` is not a contract type\n"
           "when checking that the contract literal "
           "`ct_Ez6MyeTMm17YnTnDdHTSrzMEBKmy7Uz2sXu347bTDPgVH2ifJ` "
           "has the type `bytes(32)`">>,
         <<?Pos(34, 5),
           "The type `address` is not a contract type\n"
           "when checking that the call to `Address.to_contract` "
           "has the type `address`">>])
    , ?TYPE_ERROR(stateful,
       [<<?Pos(13, 35)
          "Cannot reference stateful function `Chain.spend` in the definition of non-stateful function `fail1`.">>,
        <<?Pos(14, 35)
          "Cannot reference stateful function `local_spend` in the definition of non-stateful function `fail2`.">>,
        <<?Pos(16, 15)
          "Cannot reference stateful function `Chain.spend` in the definition of non-stateful function `fail3`.">>,
        <<?Pos(20, 31)
          "Cannot reference stateful function `Chain.spend` in the definition of non-stateful function `fail4`.">>,
        <<?Pos(35, 47)
          "Cannot reference stateful function `Chain.spend` in the definition of non-stateful function `fail5`.">>,
        <<?Pos(48, 57)
          "Cannot pass non-zero value argument `1000` in the definition of non-stateful function `fail6`.">>,
        <<?Pos(49, 56)
          "Cannot pass non-zero value argument `1000` in the definition of non-stateful function `fail7`.">>,
        <<?Pos(52, 17)
          "Cannot pass non-zero value argument `1000` in the definition of non-stateful function `fail8`.">>])
    , ?TYPE_ERROR(bad_init_state_access,
       [<<?Pos(11, 5)
          "The `init` function should return the initial state as its result and cannot write the state, "
          "but it calls\n"
          "  - `set_state` (at line 11, column 5), which calls\n"
          "  - `roundabout` (at line 8, column 38), which calls\n"
          "  - `put` (at line 7, column 39)">>,
        <<?Pos(12, 5)
          "The `init` function should return the initial state as its result and cannot read the state, "
          "but it calls\n"
          "  - `new_state` (at line 12, column 5), which calls\n"
          "  - `state` (at line 5, column 29)">>,
        <<?Pos(13, 13)
          "The `init` function should return the initial state as its result and cannot read the state, "
          "but it calls\n"
          "  - `state` (at line 13, column 13)">>])
    , ?TYPE_ERROR(modifier_checks,
       [<<?Pos(11, 3)
          "The function `all_the_things` cannot be both public and private.">>,
        <<?Pos(3, 3)
          "Namespaces cannot contain entrypoints. Use `function` instead.">>,
        <<?Pos(5, 10)
          "The contract `Remote` has no entrypoints. Since Sophia version 3.2, "
          "public contract functions must be declared with the `entrypoint` "
          "keyword instead of `function`.">>,
        <<?Pos(12, 3)
          "The entrypoint `wha` cannot be private. Use `function` instead.">>,
        <<?Pos(6, 3)
          "Use `entrypoint` for declaration of `foo`: `entrypoint foo : () => unit`">>,
        <<?Pos(10, 3)
          "Use `entrypoint` instead of `function` for public function `foo`: `entrypoint foo() = ()`">>,
        <<?Pos(6, 3)
          "Use `entrypoint` instead of `function` for public function `foo`: `entrypoint foo : () => unit`">>])
    , ?TYPE_ERROR(list_comp_not_a_list,
      [<<?Pos(2, 36)
         "Cannot unify `int` and `list('a)`\n"
         "when checking rvalue of list comprehension binding `1 : int` against type `list('a)`">>
      ])
    , ?TYPE_ERROR(list_comp_if_not_bool,
      [<<?Pos(2, 44)
         "Cannot unify `int` and `bool`\n"
         "when checking the type of the expression `3 : int` against the expected type `bool`">>
      ])
    , ?TYPE_ERROR(list_comp_bad_shadow,
      [<<?Pos(2, 53)
         "Cannot unify `string` and `int`\n"
         "when checking the type of the pattern `x : int` against the expected type `string`">>
      ])
    , ?TYPE_ERROR(map_as_map_key,
       [<<?Pos(5, 47)
         "Invalid key type `map(int, int)`\n"
         "Map keys cannot contain other maps.">>,
        <<?Pos(6, 31)
         "Invalid key type `list(map(int, int))`\n"
         "Map keys cannot contain other maps.">>,
        <<?Pos(6, 31)
         "Invalid key type `lm`\n"
         "Map keys cannot contain other maps.">>])
    , ?TYPE_ERROR(calling_init_function,
       [<<?Pos(7, 28)
          "The 'init' function is called exclusively by the create contract transaction "
          "and cannot be called from the contract code.">>])
    , ?TYPE_ERROR(bad_top_level_decl,
        [<<?Pos(1, 1) "The definition of 'square' must appear inside a contract or namespace.">>])
    , ?TYPE_ERROR(missing_event_type,
        [<<?Pos(3, 5)
           "Unbound variable `Chain.event`\n"
           "Did you forget to define the event type?">>])
    , ?TYPE_ERROR(bad_bytes_to_x,
        [<<?Pos(3, 35)
           "Cannot resolve length of byte array in\n"
           "  the result of a call to Bytes.to_fixed_size">>,
         <<?Pos(4, 36)
           "Cannot unify `bytes()` and `bytes(4)`\nwhen checking the application of\n"
           "  `Bytes.to_fixed_size : (bytes()) => option('a)`\n"
           "to arguments\n"
           "  `b : bytes(4)`">>,
         <<?Pos(4, 36)
           "Cannot resolve length of byte array in\n"
           "  the result of a call to Bytes.to_fixed_size">>,
         <<?Pos(5, 35)
           "Cannot resolve length of byte array in\n"
           "  the first argument of a call to Bytes.to_any_size">>])
    , ?TYPE_ERROR(bad_bytes_concat,
        [<<?Pos(12, 40)
           "Failed to resolve byte array lengths in call to Bytes.concat with arguments of type\n"
           "  - 'g  (at line 12, column 20)\n"
           "  - 'h  (at line 12, column 23)\n"
           "and result type\n"
           "  - bytes(10)  (at line 12, column 28)">>,
         <<?Pos(13, 28)
           "Failed to resolve byte array lengths in call to Bytes.concat with arguments of type\n"
           "  - 'd  (at line 13, column 20)\n"
           "  - 'e  (at line 13, column 23)\n"
           "and result type\n"
           "  - 'f  (at line 13, column 14)">>,
         <<?Pos(15, 5)
           "Cannot unify `bytes(26)` and `bytes(25)`\n"
           "when checking the type of the expression `Bytes.concat(x, y) : bytes(26)` "
           "against the expected type `bytes(25)`">>,
         <<?Pos(17, 5)
           "Failed to resolve byte array lengths in call to Bytes.concat with arguments of type\n"
           "  - bytes(6)  (at line 16, column 24)\n"
           "  - 'b  (at line 16, column 34)\n"
           "and result type\n"
           "  - 'c  (at line 16, column 39)">>,
         <<?Pos(19, 25)
           "Cannot resolve type of byte array in\n"
           "  the first argument of a call to Bytes.to_str">>])
    , ?TYPE_ERROR(bad_bytes_split,
         [<<?Pos(13, 5)
            "Failed to resolve byte array lengths in call to Bytes.split with argument of type\n"
            "  - 'f  (at line 12, column 20)\n"
            "and result types\n"
            "  - 'e  (at line 12, column 25)\n"
            "  - bytes(20)  (at line 12, column 29)">>,
          <<?Pos(16, 5)
            "Failed to resolve byte array lengths in call to Bytes.split with argument of type\n"
            "  - bytes(15)  (at line 15, column 24)\n"
            "and result types\n"
            "  - 'c  (at line 16, column 5)\n"
            "  - 'd  (at line 16, column 5)">>,
          <<?Pos(19, 5)
            "Failed to resolve byte array lengths in call to Bytes.split with argument of type\n"
            "  - 'b  (at line 18, column 20)\n"
            "and result types\n"
            "  - bytes(20)  (at line 18, column 25)\n"
            "  - 'a  (at line 18, column 37)">>])
    , ?TYPE_ERROR(wrong_compiler_version,
        [<<?Pos(1, 1)
           "Cannot compile with this version of the compiler, "
           "because it does not satisfy the constraint ", Version/binary, " < 1.0">>,
         <<?Pos(2, 1)
           "Cannot compile with this version of the compiler, "
           "because it does not satisfy the constraint ", Version/binary, " == 9.9.9">>])
    , ?TYPE_ERROR(interface_with_defs,
         [<<?Pos(2, 3)
            "Contract interfaces cannot contain defined functions or entrypoints.\n"
            "Fix: replace the definition of `foo` by a type signature.">>])
    , ?TYPE_ERROR(contract_as_namespace,
         [<<?Pos(5, 28)
            "Invalid call to contract entrypoint `Foo.foo`.\n"
            "It must be called as `c.foo` for some `c : Foo`.">>])
    , ?TYPE_ERROR(empty_typedecl,
                  [<<?Pos(2, 8)
                     "Empty type declarations are not supported. "
                     "Type `t` lacks a definition">>])
    , ?TYPE_ERROR(higher_kinded_type,
                  [<<?Pos(2, 35)
                     "Type `'m` is a higher kinded type variable "
                     "(takes another type as an argument)">>])
    , ?TYPE_ERROR(bad_arity,
                  [<<?Pos(3, 20)
                     "Arity for id doesn't match. Expected 1, got 0">>,
                   <<?Pos(3, 25)
                     "Cannot unify `int` and `id`\n"
                     "when checking the type of the expression `123 : int` "
                     "against the expected type `id`">>,
                   <<?Pos(4, 20)
                     "Arity for id doesn't match. Expected 1, got 2">>,
                   <<?Pos(4, 35)
                     "Cannot unify `int` and `id(int, int)`\n"
                     "when checking the type of the expression `123 : int` "
                     "against the expected type `id(int, int)`">>])
    , ?TYPE_ERROR(bad_unnamed_map_update_default,
                  [<<?Pos(4, 17)
                     "Invalid map update with default">>])
    , ?TYPE_ERROR(non_functional_entrypoint,
                  [<<?Pos(2, 14)
                     "`f` was declared with an invalid type `int`. "
                     "Entrypoints and functions must have functional types">>])
    , ?TYPE_ERROR(bad_records,
        [<<?Pos(3, 16)
           "Mixed record fields and map keys in `{x = 0, [0] = 1}`">>,
         <<?Pos(4, 6)
           "Mixed record fields and map keys in `r {x = 0, [0] = 1}`">>,
         <<?Pos(5, 6)
           "Empty record/map update `r {}`">>
        ])
    , ?TYPE_ERROR(bad_protected_call,
        [<<?Pos(6, 22)
           "Invalid `protected` argument `(0 : int) == (1 : int) : bool`. "
           "It must be either `true` or `false`.">>
        ])
    , ?TYPE_ERROR(bad_function_block,
                  [<<?Pos(4, 5)
                     "Mismatch in the function block. Expected implementation/type declaration of g function">>,
                   <<?Pos(5, 5)
                     "Mismatch in the function block. Expected implementation/type declaration of g function">>
                  ])
    , ?TYPE_ERROR(just_an_empty_file,
                  [<<?Pos(0, 0)
                     "Empty contract">>
                  ])
    , ?TYPE_ERROR(bad_number_of_args,
                  [<<?Pos(3, 39)
                     "Cannot unify `() => unit` and `(int) => 'a`\n",
                     "when checking the application of\n"
                     "  `f : () => unit`\n"
                     "to arguments\n"
                     "  `1 : int`">>,
                   <<?Pos(4, 20)
                     "Cannot unify `(int, string) => 'e` and `(int) => 'd`\n"
                     "when checking the application of\n"
                     "  `g : (int, string) => 'e`\n"
                     "to arguments\n"
                     "  `1 : int`">>,
                   <<?Pos(5, 20)
                     "Cannot unify `(int, string) => 'c` and `(string) => 'b`\n"
                     "when checking the application of\n"
                     "  `g : (int, string) => 'c`\n"
                     "to arguments\n"
                     "  `\"Litwo, ojczyzno moja\" : string`">>
                  ])
    , ?TYPE_ERROR(bad_state,
                  [<<?Pos(4, 16)
                     "Conflicting updates for field 'foo'">>])
    , ?TYPE_ERROR(factories_type_errors,
                  [<<?Pos(10,18)
                     "Chain.clone requires `ref` named argument of contract type.">>,
                   <<?Pos(11,18)
                     "Cannot unify `(gas : int, value : int, protected : bool) => if(protected, option(void), void)` and `(gas : int, value : int, protected : bool, int, bool) => if(protected, option(void), void)`\n"
                     "when checking contract construction of type\n"
                     "  (gas : int, value : int, protected : bool) =>\n"
                     "    if(protected, option(void), void) (at line 11, column 18)\n"
                     "against the expected type\n"
                     "  (gas : int, value : int, protected : bool, int, bool) =>\n"
                     "    if(protected, option(void), void)">>,
                   <<?Pos(11,18)
                     "Cannot unify `Bakoom` and `Kaboom`\n"
                     "when checking that contract construction of type\n"
                     "  Bakoom\n"
                     "arising from resolution of variadic function `Chain.clone`\n"
                     "matches the expected type\n"
                     "  Kaboom">>,
                   <<?Pos(12,37)
                     "Cannot unify `int` and `bool`\n"
                     "when checking named argument `gas : int` against inferred type `bool`">>,
                   <<?Pos(13,18),
                     "Kaboom is not implemented.\n"
                     "when resolving arguments of variadic function `Chain.create`">>,
                   <<?Pos(18,18)
                     "Cannot unify `(gas : int, value : int, protected : bool, int, bool) => if(protected, option(void), void)` and `(gas : int, value : int, protected : bool) => 'a`\n"
                     "when checking contract construction of type\n  (gas : int, value : int, protected : bool, int, bool) =>\n    if(protected, option(void), void) (at line 18, column 18)\nagainst the expected type\n  (gas : int, value : int, protected : bool) => 'a">>,
                   <<?Pos(19,42),
                     "Named argument `protected` is not one of the expected named arguments\n  - `value : int`">>,
                   <<?Pos(20,42),
                     "Cannot unify `int` and `bool`\n"
                     "when checking named argument `value : int` against inferred type `bool`">>
                  ])
    , ?TYPE_ERROR(ambiguous_main,
                  [<<?Pos(1,1)
                    "Could not deduce the main contract. You can point it out manually with the `main` keyword.">>
                  ])
    , ?TYPE_ERROR(no_main_contract,
                  [<<?Pos(0,0)
                     "No contract defined.">>
                  ])
    , ?TYPE_ERROR(multiple_main_contracts,
                   [<<?Pos(1,6)
                      "Only one main contract can be defined.">>
                   ])
    , ?TYPE_ERROR(using_namespace_ambiguous_name,
                  [ <<?Pos(13,23)
                      "Ambiguous name `A.f` could be one of\n"
                      "  - `Xa.f` (at line 2, column 3)\n"
                      "  - `Xb.f` (at line 5, column 3)">>
                  , <<?Pos(13,23)
                      "Unbound variable `A.f`">>
                  ])
    , ?TYPE_ERROR(using_namespace_wrong_scope,
                  [ <<?Pos(19,5)
                      "Unbound variable `f`">>
                  , <<?Pos(21,23)
                      "Unbound variable `f`">>
                  ])
    , ?TYPE_ERROR(using_namespace_undefined,
                  [<<?Pos(2,3)
                     "Cannot use undefined namespace MyUndefinedNamespace">>
                  ])
    , ?TYPE_ERROR(using_namespace_undefined_parts,
                  [<<?Pos(5,3)
                     "The namespace Nsp does not define the following names: a">>
                  ])
    , ?TYPE_ERROR(using_namespace_hidden_parts,
                  [<<?Pos(8,23)
                     "Unbound variable `g`">>
                  ])
    , ?TYPE_ERROR(stateful_pattern_guard,
                  [<<?Pos(8,12)
                     "Cannot reference stateful function `g` in a pattern guard.">>
                  ])
    , ?TYPE_ERROR(non_boolean_pattern_guard,
                  [<<?Pos(4,24)
                     "Cannot unify `string` and `bool`\n"
                     "when checking the type of the expression `\"y\" : string` "
                     "against the expected type `bool`">>
                  ])
    , ?TYPE_ERROR(empty_record_definition,
                  [<<?Pos(2,5)
                     "Empty record definitions are not allowed. Cannot define the record `r`">>
                  ])
    , ?TYPE_ERROR(operator_lambdas,
                  [<<?Pos(9,32)
                     "Cannot unify `(int, int) => int` and `(int) => 'a`\n"
                     "when checking the application of\n"
                     "  `(l : _, r : _) => l + r : (int, int) => int`\n"
                     "to arguments\n"
                     "  `1 : int`">>
                  ])
    , ?TYPE_ERROR(warnings,
                  [<<?Pos(0, 0)
                      "The file `Triple.aes` is included but not used.">>,
                   <<?Pos(13, 3)
                     "The function `h` is defined but never used.">>,
                   <<?Pos(19, 3)
                     "The type `unused_type` is defined but never used.">>,
                   <<?Pos(23, 54)
                     "Negative spend.">>,
                   <<?Pos(27, 9)
                     "The definition of `x` shadows an older definition at line 26, column 9.">>,
                   <<?Pos(30, 36)
                     "Division by zero.">>,
                   <<?Pos(32, 3)
                     "The function `unused_stateful` is unnecessarily marked as stateful.">>,
                   <<?Pos(35, 31)
                     "The variable `unused_arg` is defined but never used.">>,
                   <<?Pos(36, 9)
                     "The variable `unused_var` is defined but never used.">>,
                   <<?Pos(41, 3)
                     "The function `unused_function` is defined but never used.">>,
                   <<?Pos(42, 3)
                     "The function `recursive_unused_function` is defined but never used.">>,
                   <<?Pos(43, 3)
                     "The function `called_unused_function1` is defined but never used.">>,
                   <<?Pos(44, 3)
                     "The function `called_unused_function2` is defined but never used.">>,
                   <<?Pos(48, 5)
                     "Unused return value.">>,
                   <<?Pos(60, 5)
                     "The function `dec` is defined but never used.">>,
                   <<?Pos(73, 9)
                     "The definition of `const` shadows an older definition at line 70, column 3.">>,
                   <<?Pos(84, 7)
                     "The constant `c` is defined but never used.">>
                  ])
    , ?TYPE_ERROR(polymorphism_contract_interface_recursive,
                  [<<?Pos(1,24)
                     "Trying to implement or extend an undefined interface `Z`">>
                  ])
    , ?TYPE_ERROR(polymorphism_contract_interface_same_name_different_type,
                  [<<?Pos(5,5)
                     "Cannot unify `char` and `int`\n"
                     "when implementing the entrypoint `f` from the interface `I1`">>
                  ])
    , ?TYPE_ERROR(polymorphism_contract_missing_implementation,
                  [<<?Pos(4,20)
                     "Unimplemented entrypoint `f` from the interface `I1` in the contract `I2`">>
                  ])
    , ?TYPE_ERROR(polymorphism_contract_same_decl_multi_interface,
                  [<<?Pos(7,10)
                     "Both interfaces `I` and `J` implemented by the contract `C` have a function called `f`">>
                  ])
    , ?TYPE_ERROR(polymorphism_contract_undefined_interface,
                  [<<?Pos(1,14)
                     "Trying to implement or extend an undefined interface `I`">>
                  ])
    , ?TYPE_ERROR(polymorphism_contract_same_name_different_type_multi_interface,
                  [<<?Pos(7,10)
                     "Both interfaces `I` and `J` implemented by the contract `C` have a function called `f`">>
                  ])
    , ?TYPE_ERROR(polymorphism_contract_interface_undefined_interface,
                  [<<?Pos(1,24)
                     "Trying to implement or extend an undefined interface `H`">>
                  ])
    , ?TYPE_ERROR(polymorphism_variance_switching,
                  [<<?Pos(36,49)
                     "Cannot unify `Cat` and `Animal` in a contravariant context\n"
                     "when checking the application of\n"
                     "  `g2 : (Cat) => Cat`\n"
                     "to arguments\n"
                     "  `x : Animal`">>,
                   <<?Pos(39,43)
                     "Cannot unify `Animal` and `Cat` in a covariant context\n"
                     "when checking the type of the expression `g3(x) : Animal` against the expected type `Cat`">>,
                   <<?Pos(48,55)
                     "Cannot unify `Animal` and `Cat` in a covariant context\n"
                     "when checking the application of\n"
                     "  `g5 : ((Animal) => Animal) => Cat`\n"
                     "to arguments\n"
                     "  `x : (Cat) => Cat`">>,
                   <<?Pos(52,44)
                     "Cannot unify `Animal` and `Cat` in a covariant context\n"
                     "when checking the type of the expression `f6() : option(Animal)` against the expected type `option(Cat)`">>,
                   <<?Pos(73,43)
                     "Cannot unify `Animal` and `Cat` in a covariant context\n"
                     "when checking the type of the expression `some_animal : Animal` against the expected type `Cat`">>
                  ])
    , ?TYPE_ERROR(polymorphism_variance_switching_custom_types,
                  [<<?Pos(56,39)
                     "Cannot unify `Cat` and `Animal` in a contravariant context\n"
                     "when checking the type of the expression `DT_CONTRA(f_c_to_u) : dt_contra(Cat)` against the expected type `dt_contra(Animal)`">>,
                   <<?Pos(62,35)
                     "Cannot unify `Animal` and `Cat` in a covariant context\n"
                     "when checking the type of the expression `DT_CO(f_u_to_a) : dt_co(Animal)` against the expected type `dt_co(Cat)`">>,
                   <<?Pos(67,36)
                     "Cannot unify `Cat` and `Animal` in a contravariant context\n"
                     "when checking the application of\n  `DT_INV : ((Cat) => Cat) => dt_inv(Cat)`\nto arguments\n  `f_c_to_a : (Cat) => Animal`">>,
                   <<?Pos(67,36)
                     "Cannot unify `Cat` and `Animal` in a invariant context\n"
                     "when checking the type of the expression `DT_INV(f_c_to_a) : dt_inv(Cat)` against the expected type `dt_inv(Animal)`">>,
                   <<?Pos(68,36)
                     "Cannot unify `Cat` and `Animal` in a invariant context\n"
                     "when checking the type of the expression `DT_INV(f_c_to_c) : dt_inv(Cat)` against the expected type `dt_inv(Animal)`">>,
                   <<?Pos(69,36)
                     "Cannot unify `Animal` and `Cat` in a invariant context\n"
                     "when checking the type of the expression `DT_INV(f_a_to_a) : dt_inv(Animal)` against the expected type `dt_inv(Cat)`">>,
                   <<?Pos(70,36)
                     "Cannot unify `Animal` and `Cat` in a invariant context\n"
                     "when checking the type of the expression `DT_INV(f_a_to_c) : dt_inv(Animal)` against the expected type `dt_inv(Cat)`">>,
                   <<?Pos(71,36)
                     "Cannot unify `Cat` and `Animal` in a contravariant context\n"
                     "when checking the application of\n  `DT_INV : ((Cat) => Cat) => dt_inv(Cat)`\nto arguments\n  `f_c_to_a : (Cat) => Animal`">>,
                   <<?Pos(80,40)
                     "Cannot unify `Cat` and `Animal` in a invariant context\n"
                     "when checking the type of the expression `DT_INV_SEP_A(f_c_to_u) : dt_inv_sep(Cat)` against the expected type `dt_inv_sep(Animal)`">>,
                   <<?Pos(82,40)
                     "Cannot unify `Cat` and `Animal` in a invariant context\n"
                     "when checking the type of the expression `DT_INV_SEP_B(f_u_to_c) : dt_inv_sep(Cat)` against the expected type `dt_inv_sep(Animal)`">>,
                   <<?Pos(83,40)
                     "Cannot unify `Animal` and `Cat` in a invariant context\n"
                     "when checking the type of the expression `DT_INV_SEP_A(f_a_to_u) : dt_inv_sep(Animal)` against the expected type `dt_inv_sep(Cat)`">>,
                   <<?Pos(85,40)
                     "Cannot unify `Animal` and `Cat` in a invariant context\n"
                     "when checking the type of the expression `DT_INV_SEP_B(f_u_to_a) : dt_inv_sep(Animal)` against the expected type `dt_inv_sep(Cat)`">>,
                   <<?Pos(90,42)
                     "Cannot unify `Animal` and `Cat` in a covariant context\n"
                     "when checking the type of the expression `DT_CO_NEST_A(f_dt_contra_a_to_u) : dt_co_nest_a(Animal)` against the expected type `dt_co_nest_a(Cat)`">>,
                   <<?Pos(94,46)
                     "Cannot unify `Cat` and `Animal` in a contravariant context\n"
                     "when checking the type of the expression `DT_CONTRA_NEST_A(f_dt_co_c_to_u) : dt_contra_nest_a(Cat)` against the expected type `dt_contra_nest_a(Animal)`">>,
                   <<?Pos(99,46)
                     "Cannot unify `Cat` and `Animal` in a contravariant context\n"
                     "when checking the type of the expression `DT_CONTRA_NEST_B(f_u_to_dt_contra_c) : dt_contra_nest_b(Cat)` against the expected type `dt_contra_nest_b(Animal)`">>,
                   <<?Pos(105,42)
                     "Cannot unify `Animal` and `Cat` in a covariant context\n"
                     "when checking the type of the expression `DT_CO_NEST_B(f_u_to_dt_co_a) : dt_co_nest_b(Animal)` against the expected type `dt_co_nest_b(Cat)`">>,
                   <<?Pos(110,13)
                     "Cannot unify `Animal` and `Cat` in a covariant context\n"
                     "when checking the type of the pattern `vj3 : dt_co_twice(Cat)` against the expected type `dt_co_twice(Animal)`">>,
                   <<?Pos(114,59)
                     "Cannot unify `Cat` and `Animal` in a contravariant context\n"
                     "when checking the type of the expression `DT_A_CONTRA_B_CONTRA(f_a_to_c_to_u) : dt_a_contra_b_contra(Animal, Cat)` against the expected type `dt_a_contra_b_contra(Animal, Animal)`">>,
                   <<?Pos(115,59)
                     "Cannot unify `Cat` and `Animal` in a contravariant context\n"
                     "when checking the type of the expression `DT_A_CONTRA_B_CONTRA(f_c_to_a_to_u) : dt_a_contra_b_contra(Cat, Animal)` against the expected type `dt_a_contra_b_contra(Animal, Animal)`">>,
                   <<?Pos(116,59)
                     "Cannot unify `Cat` and `Animal` in a contravariant context\n"
                     "when checking the type of the expression `DT_A_CONTRA_B_CONTRA(f_c_to_c_to_u) : dt_a_contra_b_contra(Cat, Cat)` against the expected type `dt_a_contra_b_contra(Animal, Animal)`">>,
                   <<?Pos(116,59)
                     "Cannot unify `Cat` and `Animal` in a contravariant context\n"
                     "when checking the type of the expression `DT_A_CONTRA_B_CONTRA(f_c_to_c_to_u) : dt_a_contra_b_contra(Cat, Cat)` against the expected type `dt_a_contra_b_contra(Animal, Animal)`">>,
                   <<?Pos(119,59)
                     "Cannot unify `Cat` and `Animal` in a contravariant context\n"
                     "when checking the type of the expression `DT_A_CONTRA_B_CONTRA(f_c_to_a_to_u) : dt_a_contra_b_contra(Cat, Animal)` against the expected type `dt_a_contra_b_contra(Animal, Cat)`">>,
                   <<?Pos(120,59)
                     "Cannot unify `Cat` and `Animal` in a contravariant context\n"
                     "when checking the type of the expression `DT_A_CONTRA_B_CONTRA(f_c_to_c_to_u) : dt_a_contra_b_contra(Cat, Cat)` against the expected type `dt_a_contra_b_contra(Animal, Cat)`">>,
                   <<?Pos(122,59)
                     "Cannot unify `Cat` and `Animal` in a contravariant context\n"
                     "when checking the type of the expression `DT_A_CONTRA_B_CONTRA(f_a_to_c_to_u) : dt_a_contra_b_contra(Animal, Cat)` against the expected type `dt_a_contra_b_contra(Cat, Animal)`">>,
                   <<?Pos(124,59)
                     "Cannot unify `Cat` and `Animal` in a contravariant context\n"
                     "when checking the type of the expression `DT_A_CONTRA_B_CONTRA(f_c_to_c_to_u) : dt_a_contra_b_contra(Cat, Cat)` against the expected type `dt_a_contra_b_contra(Cat, Animal)`">>,
                   <<?Pos(131,13)
                     "Cannot unify `Cat` and `Animal` in a contravariant context\n"
                     "when checking the type of the pattern `vl2 : dt_contra_twice(Animal)` against the expected type `dt_contra_twice(Cat)`">>
                  ])
    , ?TYPE_ERROR(polymorphism_variance_switching_records,
                  [<<?Pos(27,13)
                     "Cannot unify `Animal` and `Cat` in a covariant context\n"
                     "when checking the type of the pattern `r03 : rec_co(Cat)` against the expected type `Main.rec_co(Animal)`">>,
                   <<?Pos(33,13)
                     "Cannot unify `Cat` and `Animal` in a contravariant context\n"
                     "when checking the type of the pattern `r06 : rec_contra(Animal)` against the expected type `Main.rec_contra(Cat)`">>,
                   <<?Pos(40,13)
                     "Cannot unify `Cat` and `Animal` in a invariant context\n"
                     "when checking the type of the pattern `r10 : rec_inv(Animal)` against the expected type `Main.rec_inv(Cat)`">>,
                   <<?Pos(41,13)
                     "Cannot unify `Animal` and `Cat` in a invariant context\n"
                     "when checking the type of the pattern `r11 : rec_inv(Cat)` against the expected type `Main.rec_inv(Animal)`">>
                  ])
    , ?TYPE_ERROR(polymorphism_variance_switching_oracles,
                  [<<?Pos(15,13)
                     "Cannot unify `Cat` and `Animal` in a contravariant context\n"
                     "when checking the type of the pattern `o03 : oracle(Animal, Animal)` against the expected type `oracle(Cat, Animal)`">>,
                   <<?Pos(16,13)
                     "Cannot unify `Cat` and `Animal` in a contravariant context\n"
                     "when checking the type of the pattern `o04 : oracle(Animal, Animal)` against the expected type `oracle(Cat, Cat)`">>,
                   <<?Pos(17,13)
                     "Cannot unify `Animal` and `Cat` in a covariant context\n"
                     "when checking the type of the pattern `o05 : oracle(Animal, Cat)` against the expected type `oracle(Animal, Animal)`">>,
                   <<?Pos(19,13)
                     "Cannot unify `Cat` and `Animal` in a contravariant context\n"
                     "when checking the type of the pattern `o07 : oracle(Animal, Cat)` against the expected type `oracle(Cat, Animal)`">>,
                   <<?Pos(19,13)
                     "Cannot unify `Animal` and `Cat` in a covariant context\n"
                     "when checking the type of the pattern `o07 : oracle(Animal, Cat)` against the expected type `oracle(Cat, Animal)`">>,
                   <<?Pos(20,13)
                     "Cannot unify `Cat` and `Animal` in a contravariant context\n"
                     "when checking the type of the pattern `o08 : oracle(Animal, Cat)` against the expected type `oracle(Cat, Cat)`">>,
                   <<?Pos(25,13)
                     "Cannot unify `Animal` and `Cat` in a covariant context\n"
                     "when checking the type of the pattern `o13 : oracle(Cat, Cat)` against the expected type `oracle(Animal, Animal)`">>,
                   <<?Pos(27,13)
                     "Cannot unify `Animal` and `Cat` in a covariant context\n"
                     "when checking the type of the pattern `o15 : oracle(Cat, Cat)` against the expected type `oracle(Cat, Animal)`">>,
                   <<?Pos(34,13)
                     "Cannot unify `Animal` and `Cat` in a covariant context\n"
                     "when checking the type of the pattern `q05 : oracle_query(Animal, Cat)` against the expected type `oracle_query(Animal, Animal)`">>,
                   <<?Pos(36,13)
                     "Cannot unify `Animal` and `Cat` in a covariant context\n"
                     "when checking the type of the pattern `q07 : oracle_query(Animal, Cat)` against the expected type `oracle_query(Cat, Animal)`">>,
                   <<?Pos(38,13)
                     "Cannot unify `Animal` and `Cat` in a covariant context\n"
                     "when checking the type of the pattern `q09 : oracle_query(Cat, Animal)` against the expected type `oracle_query(Animal, Animal)`">>,
                   <<?Pos(39,13)
                     "Cannot unify `Animal` and `Cat` in a covariant context\n"
                     "when checking the type of the pattern `q10 : oracle_query(Cat, Animal)` against the expected type `oracle_query(Animal, Cat)`">>,
                   <<?Pos(42,13)
                     "Cannot unify `Animal` and `Cat` in a covariant context\n"
                     "when checking the type of the pattern `q13 : oracle_query(Cat, Cat)` against the expected type `oracle_query(Animal, Animal)`">>,
                   <<?Pos(42,13)
                     "Cannot unify `Animal` and `Cat` in a covariant context\n"
                     "when checking the type of the pattern `q13 : oracle_query(Cat, Cat)` against the expected type `oracle_query(Animal, Animal)`">>,
                   <<?Pos(43,13)
                     "Cannot unify `Animal` and `Cat` in a covariant context\n"
                     "when checking the type of the pattern `q14 : oracle_query(Cat, Cat)` against the expected type `oracle_query(Animal, Cat)`">>,
                   <<?Pos(44,13)
                     "Cannot unify `Animal` and `Cat` in a covariant context\n"
                     "when checking the type of the pattern `q15 : oracle_query(Cat, Cat)` against the expected type `oracle_query(Cat, Animal)`">>
                  ])
    , ?TYPE_ERROR(polymorphism_variance_switching_chain_create_fail,
                  [<<?Pos(9,22)
                     "I is not implemented.\n"
                     "when resolving arguments of variadic function `Chain.create`">>,
                   <<?Pos(10,13)
                     "Cannot unify `I` and `C` in a covariant context\n"
                     "when checking the type of the pattern `c2 : C` against the expected type `I`">>,
                   <<?Pos(10,22)
                     "I is not implemented.\n"
                     "when resolving arguments of variadic function `Chain.create`">>,
                   <<?Pos(11,22)
                     "I is not implemented.\n"
                     "when resolving arguments of variadic function `Chain.create`">>
                  ])
    , ?TYPE_ERROR(missing_definition,
                  [<<?Pos(2,14)
                     "Missing definition of function `foo`">>
                  ])
    , ?TYPE_ERROR(child_with_decls,
                  [<<?Pos(2,14)
                     "Missing definition of function `f`">>
                  ])
    , ?TYPE_ERROR(parameterised_state,
                  [<<?Pos(3,8)
                     "The state type cannot be parameterized">>
                  ])
    , ?TYPE_ERROR(parameterised_event,
                  [<<?Pos(3,12)
                     "The event type cannot be parameterized">>
                  ])
    , ?TYPE_ERROR(missing_init_fun_alias_to_type,
                  [<<?Pos(1,10)
                     "Missing `init` function for the contract `AliasToType`.\n"
                     "The `init` function can only be omitted if the state type is `unit`">>
                  ])
    , ?TYPE_ERROR(missing_init_fun_alias_to_alias_to_type,
                  [<<?Pos(1,10)
                     "Missing `init` function for the contract `AliasToAliasToType`.\n"
                     "The `init` function can only be omitted if the state type is `unit`">>
                  ])
    , ?TYPE_ERROR(higher_order_entrypoint,
                  [<<?Pos(2,20)
                     "The argument\n"
                     "  `f : (int) => int`\n"
                     "of entrypoint `apply` has a higher-order (contains function types) type">>
                  ])
    , ?TYPE_ERROR(higher_order_entrypoint_return,
                  [<<?Pos(2,3)
                     "The return type\n"
                     "  `(int) => int`\n"
                     "of entrypoint `add` is higher-order (contains function types)">>
                  ])
    , ?TYPE_ERROR(polymorphic_aens_resolve,
                  [<<?Pos(4,5)
                     "Invalid return type of `AENSv2.resolve`:\n"
                     "  `'a`\n"
                     "It must be a `string` or a pubkey type (`address`, `oracle`, etc)">>
                  ])
    , ?TYPE_ERROR(bad_aens_resolve,
                  [<<?Pos(6,5)
                     "Invalid return type of `AENSv2.resolve`:\n"
                     "  `list(int)`\n"
                     "It must be a `string` or a pubkey type (`address`, `oracle`, etc)">>
                  ])
    , ?TYPE_ERROR(bad_aens_resolve_using,
                  [<<?Pos(7,5)
                     "Invalid return type of `AENSv2.resolve`:\n"
                     "  `list(int)`\n"
                     "It must be a `string` or a pubkey type (`address`, `oracle`, etc)">>
                  ])
    , ?TYPE_ERROR(polymorphic_query_type,
                  [<<?Pos(3,5)
                     "Invalid oracle type\n"
                     "  `oracle('a, 'b)`\n"
                     "The query type must not be polymorphic (contain type variables)">>,
                   <<?Pos(3,5)
                     "Invalid oracle type\n"
                     "  `oracle('a, 'b)`\n"
                     "The response type must not be polymorphic (contain type variables)">>
                  ])
    , ?TYPE_ERROR(polymorphic_response_type,
                  [<<?Pos(3,5)
                     "Invalid oracle type\n"
                     "  `oracle(string, 'r)`\n"
                     "The response type must not be polymorphic (contain type variables)">>
                  ])
    , ?TYPE_ERROR(higher_order_query_type,
                  [<<?Pos(3,5)
                     "Invalid oracle type\n"
                     "  `oracle((int) => int, string)`\n"
                     "The query type must not be higher-order (contain function types)">>
                  ])
    , ?TYPE_ERROR(higher_order_response_type,
                  [<<?Pos(3,5)
                     "Invalid oracle type\n"
                     "  `oracle(string, (int) => int)`\n"
                     "The response type must not be higher-order (contain function types)">>
                  ])
    , ?TYPE_ERROR(var_args_unify_let,
                  [<<?Pos(3,9)
                     "Cannot infer types for variable argument list.\n"
                     "when checking the type of the pattern `x : 'a` against the expected type `(gas : int, value : int, protected : bool, ref : 'b, var_args) => 'b`">>
                  ])
    , ?TYPE_ERROR(var_args_unify_fun_call,
                  [<<?Pos(6,5)
                     "Cannot infer types for variable argument list.\n"
                     "when checking the application of\n"
                     "  `g : (() => 'b) => 'b`\n"
                     "to arguments\n"
                     "  `Chain.create : (value : int, var_args) => 'c`">>
                  ])
    , ?TYPE_ERROR(polymorphism_add_stateful_entrypoint,
                  [<<?Pos(5,25)
                     "`f` cannot be stateful because the entrypoint `f` in the interface `I` is not stateful">>
                  ])
    , ?TYPE_ERROR(polymorphism_change_entrypoint_to_function,
                  [<<?Pos(6,14)
                     "`f` must be declared as an entrypoint instead of a function in order to implement the entrypoint `f` from the interface `I`">>
                  ])
    , ?TYPE_ERROR(polymorphism_non_payable_contract_implement_payable,
                  [<<?Pos(4,10)
                     "Non-payable contract `C` cannot implement payable interface `I`">>
                  ])
    , ?TYPE_ERROR(polymorphism_non_payable_interface_implement_payable,
                  [<<?Pos(4,20)
                     "Non-payable interface `H` cannot implement payable interface `I`">>
                  ])
    , ?TYPE_ERROR(polymorphism_remove_payable_entrypoint,
                  [<<?Pos(5,16)
                     "`f` must be payable because the entrypoint `f` in the interface `I` is payable">>
                  ])
    , ?TYPE_ERROR(calling_child_contract_entrypoint,
                  [<<?Pos(5,20)
                     "Invalid call to contract entrypoint `F.g`.\n"
                     "It must be called as `c.g` for some `c : F`.">>])
    , ?TYPE_ERROR(using_contract_as_namespace,
                  [<<?Pos(5,3)
                     "Cannot use undefined namespace F">>])
    , ?TYPE_ERROR(hole_expression,
                  [<<?Pos(5,13)
                     "Found a hole of type `bool`">>,
                   <<?Pos(6,17)
                     "Found a hole of type `string`">>,
                   <<?Pos(9,37)
                     "Found a hole of type `(int) => int`">>,
                   <<?Pos(13,20)
                     "Found a hole of type `'a`">>
                  ])
    , ?TYPE_ERROR(toplevel_constants_contract_as_namespace,
                  [<<?Pos(5,13)
                     "Invalid use of the contract constant `G.const`.\n"
                     "Toplevel contract constants can only be used in the contracts where they are defined.">>,
                   <<?Pos(10,11)
                     "Record type `G` does not have field `const`">>,
                   <<?Pos(10,11)
                     "Unbound field const">>,
                   <<?Pos(11,11)
                     "Record type `G` does not have field `const`">>,
                   <<?Pos(11,11)
                     "Unbound field const">>
                  ])
    , ?TYPE_ERROR(toplevel_constants_cycles,
                  [<<?Pos(2,21)
                     "Unbound variable `selfcycle`">>,
                   <<?Pos(4,5)
                     "Mutual recursion detected between the constants\n"
                     "  - `cycle1` at line 4, column 5\n"
                     "  - `cycle2` at line 5, column 5\n"
                     "  - `cycle3` at line 6, column 5">>
                  ])
    , ?TYPE_ERROR(toplevel_constants_in_interface,
                  [<<?Pos(2,10)
                     "The name of the compile-time constant cannot have pattern matching">>,
                   <<?Pos(3,5)
                     "Cannot define toplevel constants inside a contract interface">>,
                   <<?Pos(4,5)
                     "Cannot define toplevel constants inside a contract interface">>
                  ])
    , ?TYPE_ERROR(toplevel_constants_invalid_expr,
                  [<<?Pos(10,9)
                     "Invalid expression in the definition of the constant `c01`\n"
                     "You can only use the following expressions as constants: literals, lists, tuples, maps, and other constants">>,
                   <<?Pos(11,9)
                     "Invalid expression in the definition of the constant `c02`\n"
                     "You can only use the following expressions as constants: literals, lists, tuples, maps, and other constants">>,
                   <<?Pos(12,9)
                     "Invalid expression in the definition of the constant `c03`\n"
                     "You can only use the following expressions as constants: literals, lists, tuples, maps, and other constants">>,
                   <<?Pos(13,9)
                     "Invalid expression in the definition of the constant `c04`\n"
                     "You can only use the following expressions as constants: literals, lists, tuples, maps, and other constants">>,
                   <<?Pos(14,9)
                     "Invalid expression in the definition of the constant `c05`\n"
                     "You can only use the following expressions as constants: literals, lists, tuples, maps, and other constants">>,
                   <<?Pos(17,9)
                     "Invalid expression in the definition of the constant `c07`\n"
                     "You can only use the following expressions as constants: literals, lists, tuples, maps, and other constants">>,
                   <<?Pos(18,9)
                     "Invalid expression in the definition of the constant `c08`\n"
                     "You can only use the following expressions as constants: literals, lists, tuples, maps, and other constants">>,
                   <<?Pos(19,9)
                     "Invalid expression in the definition of the constant `c09`\n"
                     "You can only use the following expressions as constants: literals, lists, tuples, maps, and other constants">>,
                   <<?Pos(20,9)
                     "Invalid expression in the definition of the constant `c10`\n"
                     "You can only use the following expressions as constants: literals, lists, tuples, maps, and other constants">>,
                   <<?Pos(21,9)
                     "Invalid expression in the definition of the constant `c11`\n"
                     "You can only use the following expressions as constants: literals, lists, tuples, maps, and other constants">>
                  ])
    , ?TYPE_ERROR(toplevel_constants_invalid_id,
                  [<<?Pos(2,9)
                     "The name of the compile-time constant cannot have pattern matching">>,
                   <<?Pos(3,9)
                     "The name of the compile-time constant cannot have pattern matching">>
                  ])
    ].

validation_test_() ->
    [{"Validation fail: " ++ C1 ++ " /= " ++ C2,
      fun() ->
        Actual = case validate(C1, C2) of
                    {error, Errs} -> Errs;
                    ok -> #{}
                 end,
        check_errors(Expect, Actual)
      end} || {C1, C2, Expect} <- validation_fails()] ++
    [{"Validation of " ++ C,
      fun() ->
        ?assertEqual(ok, validate(C, C))
      end} || C <- compilable_contracts()].

validation_fails() ->
    [{"deadcode", "nodeadcode",
      [<<"Data error:\n"
         "Byte code does not match source code.\n"
         "- Functions in the source code but not in the byte code:\n"
         "    .MyList.map2">>]},
     {"validation_test1", "validation_test2",
      [<<"Data error:\n"
         "Byte code does not match source code.\n"
         "- The implementation of the function code_fail is different.\n"
         "- The attributes of the function attr_fail differ:\n"
         "    Byte code:   payable\n"
         "    Source code: \n"
         "- The type of the function type_fail differs:\n"
         "    Byte code:   integer => integer\n"
         "    Source code: {tvar,0} => {tvar,0}">>]},
     {"validation_test1", "validation_test3",
      [<<"Data error:\n"
         "Byte code contract is not payable, but source code contract is.">>]}].

validate(Contract1, Contract2) ->
    case compile(Contract1) of
        ByteCode = #{ fate_code := FCode } ->
            FCode1   = aeb_fate_code:serialize(aeb_fate_code:strip_init_function(FCode)),
            Source   = aeso_test_utils:read_contract(Contract2),
            aeso_compiler:validate_byte_code(
              ByteCode#{ byte_code := FCode1 }, Source,
              case lists:member(Contract2, debug_mode_contracts()) of
                  true  -> [debug_mode];
                  false -> []
              end ++
                  [ {src_file, lists:concat([Contract2, ".aes"])}
                  , {include, {file_system, [aeso_test_utils:contract_path()]}}
                  ]);
        Error -> print_and_throw(Error)
    end.

print_and_throw(Err) ->
    case Err of
        ErrBin when is_binary(ErrBin) ->
            io:format("\n~s", [ErrBin]),
            error(ErrBin);
        Errors ->
            io:format("Compilation error:\n~s", [string:join([aeso_errors:pp(E) || E <- Errors], "\n\n")]),
            error(compilation_error)
    end.