Move

* Update sophia_stdlib.md

add more precise description of oracle TTLs

* Update sophia_stdlib.md

docs/sophia_stdlib.md

@@ -812,8 +812,8 @@ Registers new oracle answering questions of type `'a` with answers of type `'b`.
   private key of the account, proving you have the private key of the oracle to be. If the
   address is the same as the contract `sign` is ignored and can be left out entirely.
 * The `qfee` is the minimum query fee to be paid by a user when asking a question of the oracle.
-* The `ttl` is the Time To Live for the oracle, either relative to the current
-  height (`RelativeTTL(delta)`) or a fixed height (`FixedTTL(height)`).
+* The `ttl` is the Time To Live for the oracle in key blocks, either relative to the current
+  key block height (`RelativeTTL(delta)`) or a fixed key block height (`FixedTTL(height)`).
 * The type `'a` is the type of the question to ask.
 * The type `'b` is the type of the oracle answers.
 

src/aeso_aci.erl

@@ -83,7 +83,7 @@ from_typed_ast(Type, TypedAst) ->
         string -> do_render_aci_json(JArray)
     end.
 
-encode_contract(Contract = {Head, _, {con, _, Name}, _}) when ?IS_CONTRACT_HEAD(Head) ->
+encode_contract(Contract = {Head, _, {con, _, Name}, _, _}) when ?IS_CONTRACT_HEAD(Head) ->
     C0 = #{name => encode_name(Name)},
 
     Tdefs0 = [ encode_typedef(T) || T <- sort_decls(contract_types(Contract)) ],
@@ -341,10 +341,12 @@ stateful(false) -> "".
 
 %% #contract{Ann, Con, [Declarations]}.
 
-contract_funcs({C, _, _, Decls}) when ?IS_CONTRACT_HEAD(C); C == namespace ->
+contract_funcs({C, _, _, _, Decls}) when ?IS_CONTRACT_HEAD(C) ->
     [ D || D <- Decls, is_fun(D)].
 
-contract_types({C, _, _, Decls}) when ?IS_CONTRACT_HEAD(C); C == namespace ->
+contract_types({namespace, _, _, Decls}) ->
+    [ D || D <- Decls, is_type(D) ];
+contract_types({C, _, _, _, Decls}) when ?IS_CONTRACT_HEAD(C) ->
     [ D || D <- Decls, is_type(D) ].
 
 is_fun({letfun, _, _, _, _, _}) -> true;

src/aeso_ast_to_fcode.erl

@@ -326,7 +326,7 @@ get_option(Opt, Env, Default) ->
 %% -- Compilation ------------------------------------------------------------
 
 -spec to_fcode(env(), aeso_syntax:ast()) -> {env(), fcode()}.
-to_fcode(Env, [{Contract, Attrs, Con = {con, _, Name}, Decls}|Rest])
+to_fcode(Env, [{Contract, Attrs, Con = {con, _, Name}, _Impls, Decls}|Rest])
   when ?IS_CONTRACT_HEAD(Contract) ->
     case Contract =:= contract_interface of
         false ->

src/aeso_compiler.erl

@@ -238,8 +238,8 @@ insert_init_function(Code, Options) ->
 
 last_contract_indent(Decls) ->
     case lists:last(Decls) of
-        {_, _, _, [Decl | _]} -> aeso_syntax:get_ann(col, Decl, 1) - 1;
-        _                     -> 0
+        {_, _, _, _, [Decl | _]} -> aeso_syntax:get_ann(col, Decl, 1) - 1;
+        _                        -> 0
     end.
 
 -spec to_sophia_value(string(), string(), ok | error | revert, binary()) ->
@@ -338,7 +338,7 @@ decode_calldata(ContractString, FunName, Calldata, Options0) ->
     end.
 
 -dialyzer({nowarn_function, get_decode_type/2}).
-get_decode_type(FunName, [{Contract, Ann, _, Defs}]) when ?IS_CONTRACT_HEAD(Contract) ->
+get_decode_type(FunName, [{Contract, Ann, _, _, Defs}]) when ?IS_CONTRACT_HEAD(Contract) ->
     GetType = fun({letfun, _, {id, _, Name}, Args, Ret, _})               when Name == FunName -> [{Args, Ret}];
                  ({fun_decl, _, {id, _, Name}, {fun_t, _, _, Args, Ret}}) when Name == FunName -> [{Args, Ret}];
                  (_) -> [] end,

src/aeso_parser.erl

@@ -96,17 +96,29 @@ decl() ->
     choice(
       %% Contract declaration
     [ ?RULE(token(main), keyword(contract),
-            con(), tok('='), maybe_block(decl()), {contract_main, _2, _3, _5})
+            con(), tok('='), maybe_block(decl()), {contract_main, _2, _3, [], _5})
+    , ?RULE(token(main), keyword(contract),
+            con(), tok(':'), comma_sep(con()), tok('='), maybe_block(decl()), {contract_main, _2, _3, _5, _7})
     , ?RULE(keyword(contract),
-            con(), tok('='), maybe_block(decl()), {contract_child, _1, _2, _4})
+            con(), tok('='), maybe_block(decl()), {contract_child, _1, _2, [], _4})
+    , ?RULE(keyword(contract),
+            con(), tok(':'), comma_sep(con()), tok('='), maybe_block(decl()), {contract_child, _1, _2, _4, _6})
     , ?RULE(keyword(contract), token(interface),
-            con(), tok('='), maybe_block(decl()), {contract_interface, _1, _3, _5})
+            con(), tok('='), maybe_block(decl()), {contract_interface, _1, _3, [], _5})
+    , ?RULE(keyword(contract), token(interface),
+            con(), tok(':'), comma_sep(con()), tok('='), maybe_block(decl()), {contract_interface, _1, _3, _5, _7})
     , ?RULE(token(payable), token(main), keyword(contract),
-            con(), tok('='), maybe_block(decl()), add_modifiers([_1], {contract_main, _3, _4, _6}))
+            con(), tok('='), maybe_block(decl()), add_modifiers([_1], {contract_main, _3, _4, [], _6}))
+    , ?RULE(token(payable), token(main), keyword(contract),
+            con(), tok(':'), comma_sep(con()), tok('='), maybe_block(decl()), add_modifiers([_1], {contract_main, _3, _4, _6, _8}))
     , ?RULE(token(payable), keyword(contract),
-            con(), tok('='), maybe_block(decl()), add_modifiers([_1], {contract_child, _2, _3, _5}))
+            con(), tok('='), maybe_block(decl()), add_modifiers([_1], {contract_child, _2, _3, [], _5}))
+    , ?RULE(token(payable), keyword(contract),
+            con(), tok(':'), comma_sep(con()), tok('='), maybe_block(decl()), add_modifiers([_1], {contract_child, _2, _3, _5, _7}))
     , ?RULE(token(payable), keyword(contract), token(interface),
-            con(), tok('='), maybe_block(decl()), add_modifiers([_1], {contract_interface, _2, _4, _6}))
+            con(), tok('='), maybe_block(decl()), add_modifiers([_1], {contract_interface, _2, _4, [], _6}))
+    , ?RULE(token(payable), keyword(contract), token(interface),
+            con(), tok(':'), comma_sep(con()), tok('='), maybe_block(decl()), add_modifiers([_1], {contract_interface, _2, _4, _6, _8}))
 
 
     , ?RULE(keyword(namespace), con(), tok('='), maybe_block(decl()), {namespace, _1, _2, _4})

src/aeso_pretty.erl

@@ -151,12 +151,16 @@ decl(D, Options) ->
     with_options(Options, fun() -> decl(D) end).
 
 -spec decl(aeso_syntax:decl()) -> doc().
-decl({Con, Attrs, C, Ds}) when ?IS_CONTRACT_HEAD(Con) ->
+decl({Con, Attrs, C, Is, Ds}) when ?IS_CONTRACT_HEAD(Con) ->
     Mod = fun({Mod, true}) when Mod == payable ->
                   text(atom_to_list(Mod));
              (_) -> empty() end,
+    ImplsList = case Is of
+                    [] -> [empty()];
+                    _  -> [text(":"), par(punctuate(text(","), lists:map(fun name/1, Is)), 0)]
+                end,
     block(follow( hsep(lists:map(Mod, Attrs) ++ [contract_head(Con)])
-                , hsep(name(C), text("="))), decls(Ds));
+                , hsep([name(C)] ++ ImplsList ++ [text("=")])), decls(Ds));
 decl({namespace, _, C, Ds}) ->
     block(follow(text("namespace"), hsep(name(C), text("="))), decls(Ds));
 decl({pragma, _, Pragma}) -> pragma(Pragma);

src/aeso_syntax.erl

@@ -38,9 +38,9 @@
 -type namespace_alias() :: none | con().
 -type namespace_parts() :: none | {for, [id()]} | {hiding, [id()]}.
 
--type decl() :: {contract_main, ann(), con(), [decl()]}
-              | {contract_child, ann(), con(), [decl()]}
-              | {contract_interface, ann(), con(), [decl()]}
+-type decl() :: {contract_main, ann(), con(), [con()], [decl()]}
+              | {contract_child, ann(), con(), [con()], [decl()]}
+              | {contract_interface, ann(), con(), [con()], [decl()]}
               | {namespace, ann(), con(), [decl()]}
               | {pragma, ann(), pragma()}
               | {type_decl, ann(), id(), [tvar()]} % Only for error msgs

src/aeso_type_env.erl

@@ -0,0 +1,730 @@
+-module(aeso_type_env).
+
+
+-type utype() :: {fun_t, aeso_syntax:ann(), named_args_t(), [utype()] | var_args, utype()}
+               | {app_t, aeso_syntax:ann(), utype(), [utype()]}
+               | {tuple_t, aeso_syntax:ann(), [utype()]}
+               | aeso_syntax:id()  | aeso_syntax:qid()
+               | aeso_syntax:con() | aeso_syntax:qcon()  %% contracts
+               | aeso_syntax:tvar()
+               | {if_t, aeso_syntax:ann(), aeso_syntax:id(), utype(), utype()}  %% Can branch on named argument (protected)
+               | uvar().
+
+-type uvar() :: {uvar, aeso_syntax:ann(), reference()}.
+
+-type named_args_t() :: uvar() | [{named_arg_t, aeso_syntax:ann(), aeso_syntax:id(), utype(), aeso_syntax:expr()}].
+
+-type type_id() :: aeso_syntax:id() | aeso_syntax:qid() | aeso_syntax:con() | aeso_syntax:qcon().
+
+-define(is_type_id(T), element(1, T) =:= id orelse
+        element(1, T) =:= qid orelse
+        element(1, T) =:= con orelse
+        element(1, T) =:= qcon).
+
+
+-type access() :: public | private | internal.
+
+-type typedef() :: {[aeso_syntax:tvar()], aeso_syntax:typedef() | {contract_t, [aeso_syntax:field_t()]}}
+                 | {builtin, non_neg_integer()}.
+
+-type type() :: aeso_syntax:type().
+-type name() :: string().
+-type qname() :: [string()].
+-type typesig() :: {type_sig, aeso_syntax:ann(), type_constraints(), [aeso_syntax:named_arg_t()], [type()], type()}.
+
+-type namespace_alias() :: none | name().
+-type namespace_parts() :: none | {for, [name()]} | {hiding, [name()]}.
+-type used_namespaces() :: [{qname(), namespace_alias(), namespace_parts()}].
+
+-type type_constraints() :: none | bytes_concat | bytes_split | address_to_contract | bytecode_hash.
+
+
+-type fun_info()  :: {aeso_syntax:ann(), typesig() | type()}.
+-type type_info() :: {aeso_syntax:ann(), typedef()}.
+-type var_info()  :: {aeso_syntax:ann(), utype()}.
+
+-type fun_env()  :: [{name(), fun_info()}].
+-type type_env() :: [{name(), type_info()}].
+
+
+-record(field_info,
+        { ann      :: aeso_syntax:ann()
+        , field_t  :: utype()
+        , record_t :: utype()
+        , kind     :: contract | record }).
+
+-type field_info() :: #field_info{}.
+
+
+-record(scope, { funs   = [] :: fun_env()
+               , types  = [] :: type_env()
+               , access = public :: access()
+               , kind   = namespace :: namespace | contract
+               , ann    = [{origin, system}] :: aeso_syntax:ann()
+               }).
+
+-type scope() :: #scope{}.
+
+-record(env,
+    { scopes           = #{ [] => #scope{}} :: #{ qname() => scope() }
+    , vars             = []                 :: [{name(), var_info()}]
+    , typevars         = unrestricted       :: unrestricted | [name()]
+    , fields           = #{}                :: #{ name() => [field_info()] }    %% fields are global
+    , contract_parents = #{}                :: #{ name() => [name()] }
+    , namespace        = []                 :: qname()
+    , used_namespaces  = []                 :: used_namespaces()
+    , in_pattern       = false              :: boolean()
+    , in_guard         = false              :: boolean()
+    , stateful         = false              :: boolean()
+    , unify_throws     = true               :: boolean()
+    , current_function = none               :: none | aeso_syntax:id()
+    , what             = top                :: top | namespace | contract | contract_interface
+    }).
+
+-type env() :: #env{}.
+
+
+%% -- Environment manipulation -----------------------------------------------
+
+-spec push_scope(namespace | contract, aeso_syntax:con(), env()) -> env().
+push_scope(Kind, Con, Env) ->
+    Ann  = aeso_syntax:get_ann(Con),
+    Name = name(Con),
+    New  = Env#env.namespace ++ [Name],
+    Env#env{ namespace = New, scopes = (Env#env.scopes)#{ New => #scope{ kind = Kind, ann = Ann } } }.
+
+-spec pop_scope(env()) -> env().
+pop_scope(Env) ->
+    Env#env{ namespace = lists:droplast(Env#env.namespace) }.
+
+-spec get_scope(env(), qname()) -> false | scope().
+get_scope(#env{ scopes = Scopes }, Name) ->
+    maps:get(Name, Scopes, false).
+
+-spec on_current_scope(env(), fun((scope()) -> scope())) -> env().
+on_current_scope(Env = #env{ namespace = NS, scopes = Scopes }, Fun) ->
+    Scope = maps:get(NS, Scopes),
+    Env#env{ scopes = Scopes#{ NS => Fun(Scope) } }.
+
+-spec on_scopes(env(), fun((scope()) -> scope())) -> env().
+on_scopes(Env = #env{ scopes = Scopes }, Fun) ->
+    Env#env{ scopes = maps:map(fun(_, Scope) -> Fun(Scope) end, Scopes) }.
+
+-spec bind_var(aeso_syntax:id(), utype(), env()) -> env().
+bind_var({id, Ann, X}, T, Env = #env{ vars = Vars }) ->
+    when_warning(warn_shadowing, fun() -> warn_potential_shadowing(Ann, X, Vars) end),
+    Env#env{ vars = [{X, {Ann, T}} | Env#env.vars] }.
+
+-spec bind_vars([{aeso_syntax:id(), utype()}], env()) -> env().
+bind_vars([], Env) -> Env;
+bind_vars([{X, T} | Vars], Env) ->
+    bind_vars(Vars, bind_var(X, T, Env)).
+
+-spec bind_tvars([aeso_syntax:tvar()], env()) -> env().
+bind_tvars(Xs, Env) ->
+    Env#env{ typevars = [X || {tvar, _, X} <- Xs] }.
+
+-spec check_tvar(env(), aeso_syntax:tvar()) -> aeso_syntax:tvar() | no_return().
+check_tvar(#env{ typevars = TVars}, T = {tvar, _, X}) ->
+    case TVars == unrestricted orelse lists:member(X, TVars) of
+        true  -> ok;
+        false -> type_error({unbound_type, T})
+    end,
+    T.
+
+-spec bind_fun(name(), type() | typesig(), env()) -> env().
+bind_fun(X, Type, Env) ->
+    case lookup_env(Env, term, [], [X]) of
+        false -> force_bind_fun(X, Type, Env);
+        {_QId, {Ann1, _}} ->
+            type_error({duplicate_definition, X, [Ann1, aeso_syntax:get_ann(Type)]}),
+            Env
+    end.
+
+-spec force_bind_fun(name(), type() | typesig(), env()) -> env().
+force_bind_fun(X, Type, Env = #env{ what = What }) ->
+    Ann    = aeso_syntax:get_ann(Type),
+    NoCode = get_option(no_code, false),
+    Entry = if X == "init", What == contract, not NoCode ->
+                    {reserved_init, Ann, Type};
+               What == contract_interface -> {contract_fun, Ann, Type};
+               true -> {Ann, Type}
+            end,
+    on_current_scope(Env, fun(Scope = #scope{ funs = Funs }) ->
+                            Scope#scope{ funs = [{X, Entry} | Funs] }
+                          end).
+
+-spec bind_funs([{name(), type() | typesig()}], env()) -> env().
+bind_funs([], Env) -> Env;
+bind_funs([{Id, Type} | Rest], Env) ->
+    bind_funs(Rest, bind_fun(Id, Type, Env)).
+
+-spec bind_type(name(), aeso_syntax:ann(), typedef(), env()) -> env().
+bind_type(X, Ann, Def, Env) ->
+    on_current_scope(Env, fun(Scope = #scope{ types = Types }) ->
+                            Scope#scope{ types = [{X, {Ann, Def}} | Types] }
+                          end).
+
+%% Bind state primitives
+-spec bind_state(env()) -> env().
+bind_state(Env) ->
+    Ann   = [{origin, system}],
+    Unit  = {tuple_t, Ann, []},
+    State =
+        case lookup_type(Env, {id, Ann, "state"}) of
+            {S, _} -> {qid, Ann, S};
+            false  -> Unit
+        end,
+    Env1 = bind_funs([{"state", State},
+                      {"put", {type_sig, [stateful | Ann], none, [], [State], Unit}}], Env),
+
+    case lookup_type(Env, {id, Ann, "event"}) of
+        {E, _} ->
+            %% We bind Chain.event in a local 'Chain' namespace.
+            Event = {qid, Ann, E},
+            pop_scope(
+              bind_fun("event", {fun_t, Ann, [], [Event], Unit},
+              push_scope(namespace, {con, Ann, "Chain"}, Env1)));
+        false  -> Env1
+    end.
+
+-spec bind_field(name(), field_info(), env()) -> env().
+bind_field(X, Info, Env = #env{ fields = Fields }) ->
+    Fields1 = maps:update_with(X, fun(Infos) -> [Info | Infos] end, [Info], Fields),
+    Env#env{ fields = Fields1 }.
+
+-spec bind_fields([{name(), field_info()}], env()) -> env().
+bind_fields([], Env) -> Env;
+bind_fields([{Id, Info} | Rest], Env) ->
+    bind_fields(Rest, bind_field(Id, Info, Env)).
+
+%% Contract entrypoints take three named arguments
+%%  gas       : int  = Call.gas_left()
+%%  value     : int  = 0
+%%  protected : bool = false
+contract_call_type({fun_t, Ann, [], Args, Ret}) ->
+    Id    = fun(X) -> {id, Ann, X} end,
+    Int   = Id("int"),
+    Typed = fun(E, T) -> {typed, Ann, E, T} end,
+    Named = fun(Name, Default = {typed, _, _, T}) -> {named_arg_t, Ann, Id(Name), T, Default} end,
+    {fun_t, Ann, [Named("gas",   Typed({app, Ann, Typed({qid, Ann, ["Call", "gas_left"]},
+                                                        {fun_t, Ann, [], [], Int}),
+                                        []}, Int)),
+                  Named("value", Typed({int, Ann, 0}, Int)),
+                  Named("protected", Typed({bool, Ann, false}, Id("bool")))],
+     Args, {if_t, Ann, Id("protected"), {app_t, Ann, {id, Ann, "option"}, [Ret]}, Ret}}.
+
+-spec bind_contract(aeso_syntax:decl(), env()) -> env().
+bind_contract({Contract, Ann, Id, _Impls, Contents}, Env)
+  when ?IS_CONTRACT_HEAD(Contract) ->
+    Key    = name(Id),
+    Sys    = [{origin, system}],
+    Fields =
+        [ {field_t, AnnF, Entrypoint, contract_call_type(Type)}
+          || {fun_decl, AnnF, Entrypoint, Type} <- Contents ] ++
+        [ {field_t, AnnF, Entrypoint,
+           contract_call_type(
+             {fun_t, AnnF, [], [ArgT || {typed, _, _, ArgT} <- Args], RetT})
+          }
+          || {letfun, AnnF, Entrypoint = {id, _, Name}, Args, _Type, [{guarded, _, [], {typed, _, _, RetT}}]} <- Contents,
+             Name =/= "init"
+        ] ++
+        %% Predefined fields
+        [ {field_t, Sys, {id, Sys, "address"}, {id, Sys, "address"}} ] ++
+        [ {field_t, Sys, {id, Sys, ?CONSTRUCTOR_MOCK_NAME},
+           contract_call_type(
+             case [ [ArgT || {typed, _, _, ArgT} <- Args]
+                    || {letfun, AnnF, {id, _, "init"}, Args, _, _} <- Contents,
+                       aeso_syntax:get_ann(entrypoint, AnnF, false)]
+                 ++ [ Args
+                      || {fun_decl, AnnF, {id, _, "init"}, {fun_t, _, _, Args, _}} <- Contents,
+                         aeso_syntax:get_ann(entrypoint, AnnF, false)]
+                 ++ [ Args
+                      || {fun_decl, AnnF, {id, _, "init"}, {type_sig, _, _, _, Args, _}} <- Contents,
+                         aeso_syntax:get_ann(entrypoint, AnnF, false)]
+             of
+                 [] -> {fun_t, [stateful,payable|Sys], [], [], {id, Sys, "void"}};
+                 [Args] -> {fun_t, [stateful,payable|Sys], [], Args, {id, Sys, "void"}}
+             end
+            )
+          }
+        ],
+    FieldInfo = [ {Entrypoint, #field_info{ ann      = FieldAnn,
+                                            kind     = contract,
+                                            field_t  = Type,
+                                            record_t = Id }}
+                || {field_t, _, {id, FieldAnn, Entrypoint}, Type} <- Fields ],
+    bind_type(Key, Ann, {[], {contract_t, Fields}},
+        bind_fields(FieldInfo, Env)).
+
+%% What scopes could a given name come from?
+-spec possible_scopes(env(), qname()) -> [qname()].
+possible_scopes(#env{ namespace = Current, used_namespaces = UsedNamespaces }, Name) ->
+    Qual = lists:droplast(Name),
+    NewQuals = case lists:filter(fun(X) -> element(2, X) == Qual end, UsedNamespaces) of
+                   [] ->
+                       [Qual];
+                   Namespaces ->
+                       lists:map(fun(X) -> element(1, X) end, Namespaces)
+               end,
+    Ret1 = [ lists:sublist(Current, I) ++ Q || I <- lists:seq(0, length(Current)), Q <- NewQuals ],
+    Ret2 = [ Namespace ++ Q || {Namespace, none, _} <- UsedNamespaces, Q <- NewQuals ],
+    lists:usort(Ret1 ++ Ret2).
+
+-spec visible_in_used_namespaces(used_namespaces(), qname()) -> boolean().
+visible_in_used_namespaces(UsedNamespaces, QName) ->
+    Qual = lists:droplast(QName),
+    Name = lists:last(QName),
+    case lists:filter(fun({Ns, _, _}) -> Qual == Ns end, UsedNamespaces) of
+        [] ->
+            true;
+        Namespaces ->
+            IsVisible = fun(Namespace) ->
+                            case Namespace of
+                                {_, _, {for, Names}} ->
+                                    lists:member(Name, Names);
+                                {_, _, {hiding, Names}} ->
+                                    not lists:member(Name, Names);
+                                _ ->
+                                    true
+                            end
+                        end,
+            lists:any(IsVisible, Namespaces)
+    end.
+
+-spec lookup_type(env(), type_id()) -> false | {qname(), type_info()}.
+lookup_type(Env, Id) ->
+    lookup_env(Env, type, aeso_syntax:get_ann(Id), qname(Id)).
+
+-spec lookup_env(env(), term, aeso_syntax:ann(), qname()) -> false | {qname(), fun_info()};
+                (env(), type, aeso_syntax:ann(), qname()) -> false | {qname(), type_info()}.
+lookup_env(Env, Kind, Ann, Name) ->
+    Var = case Name of
+            [X] when Kind == term -> proplists:get_value(X, Env#env.vars, false);
+            _                     -> false
+          end,
+    case Var of
+        {Ann1, Type} -> {Name, {Ann1, Type}};
+        false ->
+            Names = [ Qual ++ [lists:last(Name)] || Qual <- possible_scopes(Env, Name) ],
+            case [ Res || QName <- Names, Res <- [lookup_env1(Env, Kind, Ann, QName)], Res /= false] of
+                []    -> false;
+                [Res = {_, {AnnR, _}}] ->
+                    when_warning(warn_unused_includes,
+                                 fun() ->
+                                         %% If a file is used from a different file, we
+                                         %% can then mark it as used
+                                         F1 = proplists:get_value(file, Ann, no_file),
+                                         F2 = proplists:get_value(file, AnnR, no_file),
+                                         if
+                                             F1 /= F2 ->
+                                                 used_include(AnnR);
+                                             true ->
+                                                 ok
+                                         end
+                                 end),
+                    Res;
+                Many  ->
+                    type_error({ambiguous_name, qid(Ann, Name), [{qid, A, Q} || {Q, {A, _}} <- Many]}),
+                    false
+            end
+    end.
+
+-spec lookup_env1(env(), type | term, aeso_syntax:ann(), qname()) -> false | {qname(), fun_info()}.
+lookup_env1(#env{ namespace = Current, used_namespaces = UsedNamespaces, scopes = Scopes }, Kind, Ann, QName) ->
+    Qual = lists:droplast(QName),
+    Name = lists:last(QName),
+    AllowPrivate = lists:prefix(Qual, Current),
+    %% Get the scope
+    case maps:get(Qual, Scopes, false) of
+        false -> false; %% TODO: return reason for not in scope
+        #scope{ funs = Funs, types = Types } ->
+            Defs = case Kind of
+                     type -> Types;
+                     term -> Funs
+                   end,
+            %% Look up the unqualified name
+            case proplists:get_value(Name, Defs, false) of
+                false -> false;
+                {reserved_init, Ann1, Type} ->
+                    type_error({cannot_call_init_function, Ann}),
+                    {QName, {Ann1, Type}};  %% Return the type to avoid an extra not-in-scope error
+                {contract_fun, Ann1, Type} ->
+                    type_error({contract_treated_as_namespace, Ann, QName}),
+                    {QName, {Ann1, Type}};
+                {Ann1, _} = E ->
+                    %% Check that it's not private (or we can see private funs)
+                    case not is_private(Ann1) orelse AllowPrivate of
+                        true  ->
+                            case visible_in_used_namespaces(UsedNamespaces, QName) of
+                                true -> {QName, E};
+                                false -> false
+                            end;
+                        false -> false
+                    end
+            end
+    end.
+
+-spec lookup_record_field(env(), name()) -> [field_info()].
+lookup_record_field(Env, FieldName) ->
+    maps:get(FieldName, Env#env.fields, []).
+
+%% For 'create' or 'update' constraints we don't consider contract types.
+-spec lookup_record_field(env(), name(), create | project | update) -> [field_info()].
+lookup_record_field(Env, FieldName, Kind) ->
+    [ Fld || Fld = #field_info{ kind = K } <- lookup_record_field(Env, FieldName),
+             Kind == project orelse K /= contract ].
+
+%% -- Name manipulation ------------------------------------------------------
+
+-spec qname(type_id()) -> qname().
+qname({id,   _, X})  -> [X];
+qname({qid,  _, Xs}) -> Xs;
+qname({con,  _, X})  -> [X];
+qname({qcon, _, Xs}) -> Xs.
+
+-spec name(aeso_syntax:id() | aeso_syntax:con()) -> name().
+name({_, _, X}) -> X.
+
+-spec qid(aeso_syntax:ann(), qname()) -> aeso_syntax:id() | aeso_syntax:qid().
+qid(Ann, [X]) -> {id, Ann, X};
+qid(Ann, Xs)  -> {qid, Ann, Xs}.
+
+-spec qcon(aeso_syntax:ann(), qname()) -> aeso_syntax:con() | aeso_syntax:qcon().
+qcon(Ann, [X]) -> {con, Ann, X};
+qcon(Ann, Xs)  -> {qcon, Ann, Xs}.
+
+-spec set_qname(qname(), type_id()) -> type_id().
+set_qname(Xs, {id,   Ann, _}) -> qid(Ann, Xs);
+set_qname(Xs, {qid,  Ann, _}) -> qid(Ann, Xs);
+set_qname(Xs, {con,  Ann, _}) -> qcon(Ann, Xs);
+set_qname(Xs, {qcon, Ann, _}) -> qcon(Ann, Xs).
+
+is_private(Ann) -> proplists:get_value(private, Ann, false).
+
+%% -- The rest ---------------------------------------------------------------
+
+%% Environment containing language primitives
+-spec global_env() -> env().
+global_env() ->
+    Ann     = [{origin, system}],
+    Int     = {id, Ann, "int"},
+    Char    = {id, Ann, "char"},
+    Bool    = {id, Ann, "bool"},
+    String  = {id, Ann, "string"},
+    Address = {id, Ann, "address"},
+    Hash    = {id, Ann, "hash"},
+    Bits    = {id, Ann, "bits"},
+    Bytes   = fun(Len) -> {bytes_t, Ann, Len} end,
+    Oracle  = fun(Q, R) -> {app_t, Ann, {id, Ann, "oracle"}, [Q, R]} end,
+    Query   = fun(Q, R) -> {app_t, Ann, {id, Ann, "oracle_query"}, [Q, R]} end,
+    Unit    = {tuple_t, Ann, []},
+    List    = fun(T) -> {app_t, Ann, {id, Ann, "list"}, [T]} end,
+    Option  = fun(T) -> {app_t, Ann, {id, Ann, "option"}, [T]} end,
+    Map     = fun(A, B) -> {app_t, Ann, {id, Ann, "map"}, [A, B]} end,
+    Pair    = fun(A, B) -> {tuple_t, Ann, [A, B]} end,
+    FunC    = fun(C, Ts, T) -> {type_sig, Ann, C, [], Ts, T} end,
+    FunC1   = fun(C, S, T) -> {type_sig, Ann, C, [], [S], T} end,
+    Fun     = fun(Ts, T) -> FunC(none, Ts, T) end,
+    Fun1    = fun(S, T) -> Fun([S], T) end,
+    FunCN   = fun(C, Named, Normal, Ret) -> {type_sig, Ann, C, Named, Normal, Ret} end,
+    FunN    = fun(Named, Normal, Ret) -> FunCN(none, Named, Normal, Ret) end,
+    %% Lambda    = fun(Ts, T) -> {fun_t, Ann, [], Ts, T} end,
+    %% Lambda1   = fun(S, T) -> Lambda([S], T) end,
+    StateFun  = fun(Ts, T) -> {type_sig, [stateful|Ann], none, [], Ts, T} end,
+    TVar      = fun(X) -> {tvar, Ann, "'" ++ X} end,
+    SignId    = {id, Ann, "signature"},
+    SignDef   = {bytes, Ann, <<0:64/unit:8>>},
+    Signature = {named_arg_t, Ann, SignId, SignId, {typed, Ann, SignDef, SignId}},
+    SignFun   = fun(Ts, T) -> {type_sig, [stateful|Ann], none, [Signature], Ts, T} end,
+    TTL       = {qid, Ann, ["Chain", "ttl"]},
+    Pointee   = {qid, Ann, ["AENS", "pointee"]},
+    AENSName  = {qid, Ann, ["AENS", "name"]},
+    Fr        = {qid, Ann, ["MCL_BLS12_381", "fr"]},
+    Fp        = {qid, Ann, ["MCL_BLS12_381", "fp"]},
+    Fp2       = {tuple_t, Ann, [Fp, Fp]},
+    G1        = {tuple_t, Ann, [Fp, Fp, Fp]},
+    G2        = {tuple_t, Ann, [Fp2, Fp2, Fp2]},
+    GT        = {tuple_t, Ann, lists:duplicate(12, Fp)},
+    Tx        = {qid, Ann, ["Chain", "tx"]},
+    GAMetaTx  = {qid, Ann, ["Chain", "ga_meta_tx"]},
+    BaseTx    = {qid, Ann, ["Chain", "base_tx"]},
+    PayForTx  = {qid, Ann, ["Chain", "paying_for_tx"]},
+
+    FldT      = fun(Id, T) -> {field_t, Ann, {id, Ann, Id}, T} end,
+    TxFlds    = [{"paying_for", Option(PayForTx)}, {"ga_metas", List(GAMetaTx)},
+                 {"actor", Address}, {"fee", Int}, {"ttl", Int}, {"tx", BaseTx}],
+    TxType    = {record_t, [FldT(N, T) || {N, T} <- TxFlds ]},
+    Stateful  = fun(T) -> setelement(2, T, [stateful|element(2, T)]) end,
+
+    Fee       = Int,
+    [A, Q, R, K, V] = lists:map(TVar, ["a", "q", "r", "k", "v"]),
+
+    MkDefs = fun(Defs) -> [{X, {Ann, if is_integer(T) -> {builtin, T}; true -> T end}} || {X, T} <- Defs] end,
+
+    TopScope = #scope
+        { funs  = MkDefs(
+                     %% Option constructors
+                    [{"None", Option(A)},
+                     {"Some", Fun1(A, Option(A))},
+                     %% TTL constructors
+                     {"RelativeTTL", Fun1(Int, TTL)},
+                     {"FixedTTL",    Fun1(Int, TTL)},
+                     %% Abort
+                     {"abort", Fun1(String, A)},
+                     {"require", Fun([Bool, String], Unit)}])
+        , types = MkDefs(
+                    [{"int", 0}, {"bool", 0}, {"char", 0}, {"string", 0}, {"address", 0},
+                     {"void", 0},
+                     {"unit", {[], {alias_t, Unit}}},
+                     {"hash", {[], {alias_t, Bytes(32)}}},
+                     {"signature", {[], {alias_t, Bytes(64)}}},
+                     {"bits", 0},
+                     {"option", 1}, {"list", 1}, {"map", 2},
+                     {"oracle", 2}, {"oracle_query", 2}
+                     ]) },
+
+    ChainScope = #scope
+        { funs = MkDefs(
+                     %% Spend transaction.
+                    [{"spend",        StateFun([Address, Int], Unit)},
+                     %% Chain environment
+                     {"balance",      Fun1(Address, Int)},
+                     {"block_hash",   Fun1(Int, Option(Hash))},
+                     {"coinbase",     Address},
+                     {"timestamp",    Int},
+                     {"block_height", Int},
+                     {"difficulty",   Int},
+                     {"gas_limit",    Int},
+                     {"bytecode_hash",FunC1(bytecode_hash, A, Option(Hash))},
+                     {"create",       Stateful(
+                                        FunN([ {named_arg_t, Ann, {id, Ann, "value"}, Int, {typed, Ann, {int, Ann, 0}, Int}}
+                                             ], var_args, A))},
+                     {"clone",        Stateful(
+                                        FunN([ {named_arg_t, Ann, {id, Ann, "gas"}, Int,
+                                                {typed, Ann,
+                                                 {app, Ann,
+                                                  {typed, Ann, {qid, Ann, ["Call","gas_left"]},
+                                                   typesig_to_fun_t(Fun([], Int))
+                                                  },
+                                                  []}, Int
+                                                }}
+                                             , {named_arg_t, Ann, {id, Ann, "value"}, Int, {typed, Ann, {int, Ann, 0}, Int}}
+                                             , {named_arg_t, Ann, {id, Ann, "protected"}, Bool, {typed, Ann, {bool, Ann, false}, Bool}}
+                                             , {named_arg_t, Ann, {id, Ann, "ref"}, A, undefined}
+                                             ], var_args, A))},
+                     %% Tx constructors
+                     {"GAMetaTx",     Fun([Address, Int], GAMetaTx)},
+                     {"PayingForTx",  Fun([Address, Int], PayForTx)},
+                     {"SpendTx",      Fun([Address, Int, String], BaseTx)},
+                     {"OracleRegisterTx",       BaseTx},
+                     {"OracleQueryTx",          BaseTx},
+                     {"OracleResponseTx",       BaseTx},
+                     {"OracleExtendTx",         BaseTx},
+                     {"NamePreclaimTx",         BaseTx},
+                     {"NameClaimTx",            Fun([String], BaseTx)},
+                     {"NameUpdateTx",           Fun([Hash], BaseTx)},
+                     {"NameRevokeTx",           Fun([Hash], BaseTx)},
+                     {"NameTransferTx",         Fun([Address, Hash], BaseTx)},
+                     {"ChannelCreateTx",        Fun([Address], BaseTx)},
+                     {"ChannelDepositTx",       Fun([Address, Int], BaseTx)},
+                     {"ChannelWithdrawTx",      Fun([Address, Int], BaseTx)},
+                     {"ChannelForceProgressTx", Fun([Address], BaseTx)},
+                     {"ChannelCloseMutualTx",   Fun([Address], BaseTx)},
+                     {"ChannelCloseSoloTx",     Fun([Address], BaseTx)},
+                     {"ChannelSlashTx",         Fun([Address], BaseTx)},
+                     {"ChannelSettleTx",        Fun([Address], BaseTx)},
+                     {"ChannelSnapshotSoloTx",  Fun([Address], BaseTx)},
+                     {"ContractCreateTx",       Fun([Int], BaseTx)},
+                     {"ContractCallTx",         Fun([Address, Int], BaseTx)},
+                     {"GAAttachTx",             BaseTx}
+                    ])
+        , types = MkDefs([{"ttl", 0}, {"tx", {[], TxType}},
+                          {"base_tx", 0},
+                          {"paying_for_tx", 0}, {"ga_meta_tx", 0}]) },
+
+    ContractScope = #scope
+        { funs = MkDefs(
+                    [{"address", Address},
+                     {"creator", Address},
+                     {"balance", Int}]) },
+
+    CallScope = #scope
+        { funs = MkDefs(
+                    [{"origin",    Address},
+                     {"caller",    Address},
+                     {"value",     Int},
+                     {"gas_price", Int},
+                     {"fee",       Int},
+                     {"gas_left",  Fun([], Int)}])
+        },
+
+    OracleScope = #scope
+        { funs = MkDefs(
+                    [{"register",     SignFun([Address, Fee, TTL], Oracle(Q, R))},
+                     {"expiry",       Fun([Oracle(Q, R)], Fee)},
+                     {"query_fee",    Fun([Oracle(Q, R)], Fee)},
+                     {"query",        StateFun([Oracle(Q, R), Q, Fee, TTL, TTL], Query(Q, R))},
+                     {"get_question", Fun([Oracle(Q, R), Query(Q, R)], Q)},
+                     {"respond",      SignFun([Oracle(Q, R), Query(Q, R), R], Unit)},
+                     {"extend",       SignFun([Oracle(Q, R), TTL], Unit)},
+                     {"get_answer",   Fun([Oracle(Q, R), Query(Q, R)], option_t(Ann, R))},
+                     {"check",        Fun([Oracle(Q, R)], Bool)},
+                     {"check_query",  Fun([Oracle(Q,R), Query(Q, R)], Bool)}]) },
+
+    AENSScope = #scope
+        { funs = MkDefs(
+                     [{"resolve",  Fun([String, String], option_t(Ann, A))},
+                      {"preclaim", SignFun([Address, Hash], Unit)},
+                      {"claim",    SignFun([Address, String, Int, Int], Unit)},
+                      {"transfer", SignFun([Address, Address, String], Unit)},
+                      {"revoke",   SignFun([Address, String], Unit)},
+                      {"update",   SignFun([Address, String, Option(TTL), Option(Int), Option(Map(String, Pointee))], Unit)},
+                      {"lookup",   Fun([String], option_t(Ann, AENSName))},
+                      %% AENS pointee constructors
+                      {"AccountPt",  Fun1(Address, Pointee)},
+                      {"OraclePt",   Fun1(Address, Pointee)},
+                      {"ContractPt", Fun1(Address, Pointee)},
+                      {"ChannelPt",  Fun1(Address, Pointee)},
+                      %% Name object constructor
+                      {"Name",   Fun([Address, TTL, Map(String, Pointee)], AENSName)}
+                     ])
+        , types = MkDefs([{"pointee", 0}, {"name", 0}]) },
+
+    MapScope = #scope
+        { funs = MkDefs(
+                     [{"from_list",      Fun1(List(Pair(K, V)), Map(K, V))},
+                      {"to_list",        Fun1(Map(K, V), List(Pair(K, V)))},
+                      {"lookup",         Fun([K, Map(K, V)], Option(V))},
+                      {"lookup_default", Fun([K, Map(K, V), V], V)},
+                      {"delete",         Fun([K, Map(K, V)], Map(K, V))},
+                      {"member",         Fun([K, Map(K, V)], Bool)},
+                      {"size",           Fun1(Map(K, V), Int)}]) },
+
+    %% Crypto/Curve operations
+    CryptoScope = #scope
+        { funs = MkDefs(
+                     [{"verify_sig",           Fun([Hash, Address, SignId], Bool)},
+                      {"verify_sig_secp256k1", Fun([Hash, Bytes(64), SignId], Bool)},
+                      {"ecverify_secp256k1",   Fun([Hash, Bytes(20), Bytes(65)], Bool)},
+                      {"ecrecover_secp256k1",  Fun([Hash, Bytes(65)], Option(Bytes(20)))},
+                      {"sha3",     Fun1(A, Hash)},
+                      {"sha256",   Fun1(A, Hash)},
+                      {"blake2b",  Fun1(A, Hash)}]) },
+
+    %% Fancy BLS12-381 crypto operations
+    MCL_BLS12_381_Scope = #scope
+        { funs = MkDefs(
+                     [{"g1_neg",     Fun1(G1, G1)},
+                      {"g1_norm",    Fun1(G1, G1)},
+                      {"g1_valid",   Fun1(G1, Bool)},
+                      {"g1_is_zero", Fun1(G1, Bool)},
+                      {"g1_add",     Fun ([G1, G1], G1)},
+                      {"g1_mul",     Fun ([Fr, G1], G1)},
+
+                      {"g2_neg",     Fun1(G2, G2)},
+                      {"g2_norm",    Fun1(G2, G2)},
+                      {"g2_valid",   Fun1(G2, Bool)},
+                      {"g2_is_zero", Fun1(G2, Bool)},
+                      {"g2_add",     Fun ([G2, G2], G2)},
+                      {"g2_mul",     Fun ([Fr, G2], G2)},
+
+                      {"gt_inv",      Fun1(GT, GT)},
+                      {"gt_add",      Fun ([GT, GT], GT)},
+                      {"gt_mul",      Fun ([GT, GT], GT)},
+                      {"gt_pow",      Fun ([GT, Fr], GT)},
+                      {"gt_is_one",   Fun1(GT, Bool)},
+                      {"pairing",     Fun ([G1, G2], GT)},
+                      {"miller_loop", Fun ([G1, G2], GT)},
+                      {"final_exp",   Fun1(GT, GT)},
+
+                      {"int_to_fr", Fun1(Int, Fr)},
+                      {"int_to_fp", Fun1(Int, Fp)},
+                      {"fr_to_int", Fun1(Fr, Int)},
+                      {"fp_to_int", Fun1(Fp, Int)}
+                     ]),
+          types = MkDefs(
+                     [{"fr",  0}, {"fp",  0}]) },
+
+    %% Authentication
+    AuthScope = #scope
+        { funs = MkDefs(
+                     [{"tx_hash", Option(Hash)},
+                      {"tx",      Option(Tx)}  ]) },
+
+    %% Strings
+    StringScope = #scope
+        { funs = MkDefs(
+                     [{"length",    Fun1(String, Int)},
+                      {"concat",    Fun([String, String], String)},
+                      {"to_list",   Fun1(String, List(Char))},
+                      {"from_list", Fun1(List(Char), String)},
+                      {"to_upper",  Fun1(String, String)},
+                      {"to_lower",  Fun1(String, String)},
+                      {"sha3",      Fun1(String, Hash)},
+                      {"sha256",    Fun1(String, Hash)},
+                      {"blake2b",   Fun1(String, Hash)}
+                     ]) },
+
+    %% Chars
+    CharScope = #scope
+        { funs = MkDefs(
+                     [{"to_int",   Fun1(Char, Int)},
+                      {"from_int", Fun1(Int, Option(Char))}]) },
+
+    %% Bits
+    BitsScope = #scope
+        { funs = MkDefs(
+                     [{"set",          Fun([Bits, Int], Bits)},
+                      {"clear",        Fun([Bits, Int], Bits)},
+                      {"test",         Fun([Bits, Int], Bool)},
+                      {"sum",          Fun1(Bits, Int)},
+                      {"intersection", Fun([Bits, Bits], Bits)},
+                      {"union",        Fun([Bits, Bits], Bits)},
+                      {"difference",   Fun([Bits, Bits], Bits)},
+                      {"none",         Bits},
+                      {"all",          Bits}]) },
+
+    %% Bytes
+    BytesScope = #scope
+        { funs = MkDefs(
+                   [{"to_int", Fun1(Bytes(any), Int)},
+                    {"to_str", Fun1(Bytes(any), String)},
+                    {"concat", FunC(bytes_concat, [Bytes(any), Bytes(any)], Bytes(any))},
+                    {"split",  FunC(bytes_split, [Bytes(any)], Pair(Bytes(any), Bytes(any)))}
+                   ]) },
+
+    %% Conversion
+    IntScope     = #scope{ funs = MkDefs([{"to_str", Fun1(Int,     String)}]) },
+    AddressScope = #scope{ funs = MkDefs([{"to_str", Fun1(Address, String)},
+                                          {"to_contract", FunC(address_to_contract, [Address], A)},
+                                          {"is_oracle", Fun1(Address, Bool)},
+                                          {"is_contract", Fun1(Address, Bool)},
+                                          {"is_payable", Fun1(Address, Bool)}]) },
+
+
+    #env{ scopes =
+            #{ []           => TopScope
+             , ["Chain"]    => ChainScope
+             , ["Contract"] => ContractScope
+             , ["Call"]     => CallScope
+             , ["Oracle"]   => OracleScope
+             , ["AENS"]     => AENSScope
+             , ["Map"]      => MapScope
+             , ["Auth"]     => AuthScope
+             , ["Crypto"]   => CryptoScope
+             , ["MCL_BLS12_381"] => MCL_BLS12_381_Scope
+             , ["StringInternal"] => StringScope
+             , ["Char"]     => CharScope
+             , ["Bits"]     => BitsScope
+             , ["Bytes"]    => BytesScope
+             , ["Int"]      => IntScope
+             , ["Address"]  => AddressScope
+             }
+          , fields =
+             maps:from_list([{N, [#field_info{ ann = [], field_t = T, record_t = Tx, kind = record }]}
+                             || {N, T} <- TxFlds ])
+        }.
+
+option_t(As, T) -> {app_t, As, {id, As, "option"}, [T]}.
+map_t(As, K, V) -> {app_t, As, {id, As, "map"}, [K, V]}.

test/aeso_calldata_tests.erl

@@ -39,7 +39,7 @@ calldata_aci_test_() ->
         end} || {ContractName, Fun, Args} <- compilable_contracts()].
 
 parse_args(Fun, Args) ->
-    [{contract_main, _, _, [{letfun, _, _, _, _, [{guarded, _, [], {app, _, _, AST}}]}]}] =
+    [{contract_main, _, _, _, [{letfun, _, _, _, _, [{guarded, _, [], {app, _, _, AST}}]}]}] =
         aeso_parser:string("main contract Temp = function foo() = " ++ Fun ++ "(" ++ string:join(Args, ", ") ++ ")"),
     strip_ann(AST).
 

test/aeso_compiler_tests.erl

@@ -202,6 +202,12 @@ compilable_contracts() ->
      "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",
      "test" % Custom general-purpose test file. Keep it last on the list.
     ].
 
@@ -564,7 +570,7 @@ failing_contracts() ->
       ])
     , ?TYPE_ERROR(list_comp_bad_shadow,
       [<<?Pos(2, 53)
-         "Cannot unify `int` and `string`\n"
+         "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,
@@ -837,6 +843,188 @@ failing_contracts() ->
                    <<?Pos(60, 5)
                      "The function `dec` 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(4,20)
+                     "Unimplemented function `f` from the interface `I1` in the contract `I2`">>])
+    , ?TYPE_ERROR(polymorphism_contract_missing_implementation,
+                  [<<?Pos(4,20)
+                     "Unimplemented function `f` from the interface `I1` in the contract `I2`">>
+                  ])
+    , ?TYPE_ERROR(polymorphism_contract_same_decl_multi_interface,
+                  [<<?Pos(7,10)
+                     "Unimplemented function `f` from the interface `J` in the contract `C`">>
+                  ])
+    , ?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(9,5)
+                     "Duplicate definitions of `f` at\n"
+                     "  - line 8, column 5\n"
+                     "  - line 9, column 5">>
+                  ])
+    , ?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(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(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(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(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)`">>])
     ].
 
 -define(Path(File), "code_errors/" ??File).

test/aeso_parser_tests.erl

@@ -15,7 +15,7 @@ simple_contracts_test_() ->
             Text = "main contract Identity =\n"
                    "  function id(x) = x\n",
             ?assertMatch(
-                [{contract_main, _, {con, _, "Identity"},
+                [{contract_main, _, {con, _, "Identity"}, _,
                     [{letfun, _, {id, _, "id"}, [{id, _, "x"}], {id, _, "_"},
                         [{guarded, _, [], {id, _, "x"}}]}]}], parse_string(Text)),
             ok

test/contracts/polymorphism_contract_implements_interface.aes

@@ -0,0 +1,5 @@
+contract interface Strokable =
+  entrypoint stroke : () => string
+
+contract Cat : Strokable =
+  entrypoint stroke() = "Cat stroke"

test/contracts/polymorphism_contract_interface_extends_interface.aes

@@ -0,0 +1,10 @@
+contract interface II =
+    entrypoint f : () => unit
+
+contract interface I : II =
+    entrypoint f : () => unit
+    entrypoint g : () => unit
+
+contract C : I =
+    entrypoint f() = ()
+    entrypoint g() = ()

test/contracts/polymorphism_contract_interface_extensions.aes

@@ -0,0 +1,9 @@
+contract interface I0 =
+  entrypoint f : () => int
+
+contract interface I1 : I0 =
+  entrypoint f : () => int
+  entrypoint something_else : () => int
+
+main contract C =
+  entrypoint f(x : I1) = x.f() // Here we should know that x has f

test/contracts/polymorphism_contract_interface_recursive.aes

@@ -0,0 +1,13 @@
+contract interface X : Z =
+    entrypoint x : () => int
+
+contract interface Y : X =
+    entrypoint y : () => int
+
+contract interface Z : Y =
+    entrypoint z : () => int
+
+contract C : Z =
+    entrypoint x() = 1
+    entrypoint y() = 1
+    entrypoint z() = 1

test/contracts/polymorphism_contract_interface_same_decl_multi_interface.aes

@@ -0,0 +1,8 @@
+contract interface I =
+    entrypoint f : () => int
+
+contract interface II : I =
+    entrypoint f : () => int
+
+contract C : II =
+    entrypoint f() = 1

test/contracts/polymorphism_contract_interface_same_name_different_type.aes

@@ -0,0 +1,9 @@
+contract interface I1 =
+    entrypoint f : () => int
+
+contract interface I2 : I1 =
+    entrypoint f : () => char
+
+contract C : I2 =
+    entrypoint f() = 1
+    entrypoint f() = 'c'

test/contracts/polymorphism_contract_interface_same_name_same_type.aes

@@ -0,0 +1,8 @@
+contract interface I1 =
+    entrypoint f : () => int
+
+contract interface I2 : I1 =
+    entrypoint f : () => int
+
+contract C : I2 =
+    entrypoint f() = 1

test/contracts/polymorphism_contract_interface_undefined_interface.aes

@@ -0,0 +1,5 @@
+contract interface I : H =
+    entrypoint f : () => unit
+
+contract C =
+    entrypoint g() = ()

test/contracts/polymorphism_contract_missing_implementation.aes

@@ -0,0 +1,8 @@
+contract interface I1 =
+    entrypoint f : () => int
+
+contract interface I2 : I1 =
+    entrypoint g : () => int
+
+contract C : I2 =
+    entrypoint g() = 1

test/contracts/polymorphism_contract_multi_interface.aes

@@ -0,0 +1,9 @@
+contract interface I =
+    entrypoint f : () => int
+
+contract interface J =
+    entrypoint g : () => char
+
+contract C : I, J =
+    entrypoint f() = 1
+    entrypoint g() = 'c'

test/contracts/polymorphism_contract_same_decl_multi_interface.aes

@@ -0,0 +1,8 @@
+contract interface I =
+    entrypoint f : () => int
+
+contract interface J =
+    entrypoint f : () => int
+
+contract C : I, J =
+    entrypoint f() = 1

test/contracts/polymorphism_contract_same_name_different_type_multi_interface.aes

@@ -0,0 +1,9 @@
+contract interface I =
+    entrypoint f : () => int
+
+contract interface J =
+    entrypoint f : () => char
+
+contract C : I, J =
+    entrypoint f() = 1
+    entrypoint f() = 'c'

test/contracts/polymorphism_contract_undefined_interface.aes

@@ -0,0 +1,2 @@
+contract C : I =
+    entrypoint f() = ()

test/contracts/polymorphism_variance_switching.aes

@@ -0,0 +1,75 @@
+contract interface Creature =
+    entrypoint is_alive : () => bool
+
+contract interface Animal : Creature =
+    entrypoint is_alive : () => bool
+    entrypoint sound : () => string
+
+contract Cat : Animal =
+    entrypoint sound() = "meow"
+    entrypoint is_alive() = true
+
+main contract Main =
+    entrypoint init() = ()
+
+    stateful function g0(_ : Creature) : Cat = Chain.create()
+    stateful function f0(x : Cat) : Creature = g0(x)
+    stateful function h0() =
+        let a : Animal = (Chain.create() : Cat)
+        let c : Creature = (Chain.create() : Cat)
+        let c1 : Creature = a
+        ()
+
+    stateful function g1(x : Animal) : Cat = Chain.create()
+    stateful function f1(x : Cat) : Animal = g1(x)
+
+    stateful function g11(x : list(Animal)) : list(Cat) = [Chain.create()]
+    stateful function f11(x : list(Cat)) : list(Animal) = g11(x)
+
+    stateful function g12(x : Animal * Animal) : Cat * Cat = (Chain.create(), Chain.create())
+    stateful function f12(x : Cat * Cat) : Animal * Animal = g12(x)
+
+    stateful function g13() : map(Cat, Cat) = { [Chain.create()] = Chain.create() }
+    stateful function f13() : map(Animal, Animal) = g13()
+
+    stateful function g2(x : Cat) : Cat = Chain.create()
+    stateful function f2(x : Animal) : Animal = g2(x)  // fail
+
+    stateful function g3(x : Cat) : Animal = f1(x)
+    stateful function f3(x : Cat) : Cat = g3(x)  // fail
+
+    stateful function g4(x : (Cat => Animal)) : Cat = Chain.create()
+    stateful function f4(x : (Animal => Cat)) : Animal = g4(x)
+
+    stateful function g44(x : list(list(Cat) => list(Animal))) : Cat = Chain.create()
+    stateful function f44(x : list(list(Animal) => list(Cat))) : Animal = g44(x)
+
+    stateful function g5(x : (Animal => Animal)) : Cat = Chain.create()
+    stateful function f5(x : (Cat => Cat)) : Animal = g5(x)  // fail
+
+    stateful function g6() : option(Cat) = Some(Chain.create())
+    stateful function f6() : option(Animal) = g6()
+    stateful function h6() : option(Cat) = f6()  // fail
+
+    type cat_type = Cat
+    type animal_type = Animal
+    type cat_cat_map = map(cat_type, cat_type)
+    type animal_animal_map = map(animal_type, animal_type)
+
+    stateful function g71(x : animal_type) : cat_type = Chain.create()
+    stateful function f71(x : cat_type) : animal_type = g1(x)
+
+    stateful function g72() : cat_cat_map = { [Chain.create()] = Chain.create() }
+    stateful function f72() : animal_animal_map = g13()
+
+    stateful function g73() =
+        let some_cat : Cat = Chain.create()
+        let some_animal : Animal = some_cat
+
+        let some_cat_cat_map : map(Cat, Cat) = g13()
+        let some_animal_animal_map : map(Animal, Animal) = some_cat_cat_map
+
+        let x : Animal = some_animal_animal_map[some_cat]  // success
+        let y : Cat    = some_cat_cat_map[some_animal]     // fail
+
+        ()

test/contracts/polymorphism_variance_switching_custom_types.aes

@@ -0,0 +1,135 @@
+contract interface Animal =
+    entrypoint sound : () => string
+
+contract Cat : Animal =
+    entrypoint sound() = "meow"
+
+main contract Main =
+    datatype dt_contra('a) = DT_CONTRA('a => unit)
+    datatype dt_co('a) = DT_CO(unit => 'a)
+    datatype dt_inv('a) = DT_INV('a => 'a)
+    datatype dt_biv('a) = DT_BIV(unit => unit)
+    datatype dt_inv_sep('a) = DT_INV_SEP_A('a => unit) | DT_INV_SEP_B(unit => 'a)
+    datatype dt_co_nest_a('a) = DT_CO_NEST_A(dt_contra('a) => unit)
+    datatype dt_contra_nest_a('a) = DT_CONTRA_NEST_A(dt_co('a) => unit)
+    datatype dt_contra_nest_b('a) = DT_CONTRA_NEST_B(unit => dt_contra('a))
+    datatype dt_co_nest_b('a) = DT_CO_NEST_B(unit => dt_co('a))
+    datatype dt_co_twice('a) = DT_CO_TWICE(('a => unit) => 'a)
+    datatype dt_contra_twice('a) = DT_CONTRA_TWICE('a => 'a => unit)
+    datatype dt_a_contra_b_contra('a, 'b) = DT_A_CONTRA_B_CONTRA('a => 'b => unit)
+
+    function f_a_to_a_to_u(_ : Animal) : (Animal => unit) = f_a_to_u
+    function f_a_to_c_to_u(_ : Animal) : (Cat => unit) = f_c_to_u
+    function f_c_to_a_to_u(_ : Cat) : (Animal => unit) = f_a_to_u
+    function f_c_to_c_to_u(_ : Cat) : (Cat => unit) = f_c_to_u
+
+    function f_u_to_u(_ : unit) : unit = ()
+    function f_a_to_u(_ : Animal) : unit = ()
+    function f_c_to_u(_ : Cat) : unit = ()
+
+    function f_dt_contra_a_to_u(_ : dt_contra(Animal)) : unit = ()
+    function f_dt_contra_c_to_u(_ : dt_contra(Cat)) : unit = ()
+    function f_dt_co_a_to_u(_ : dt_co(Animal)) : unit = ()
+    function f_dt_co_c_to_u(_ : dt_co(Cat)) : unit = ()
+    function f_u_to_dt_contra_a(_ : unit) : dt_contra(Animal) = DT_CONTRA(f_a_to_u)
+    function f_u_to_dt_contra_c(_ : unit) : dt_contra(Cat) = DT_CONTRA(f_c_to_u)
+
+    stateful function f_c() : Cat = Chain.create()
+    stateful function f_a() : Animal = f_c()
+
+    stateful function f_u_to_a(_ : unit) : Animal = f_a()
+    stateful function f_u_to_c(_ : unit) : Cat = f_c()
+    stateful function f_a_to_a(_ : Animal) : Animal = f_a()
+    stateful function f_a_to_c(_ : Animal) : Cat = f_c()
+    stateful function f_c_to_a(_ : Cat) : Animal = f_a()
+    stateful function f_c_to_c(_ : Cat) : Cat = f_c()
+
+    stateful function f_a_to_u_to_c(_ : (Animal => unit)) : Cat = f_c()
+    stateful function f_c_to_u_to_a(_ : (Cat => unit)) : Animal = f_a()
+    stateful function f_c_to_u_to_c(_ : (Cat => unit)) : Cat = f_c()
+
+    stateful function f_u_to_dt_co_a(_ : unit) : dt_co(Animal) = DT_CO(f_u_to_a)
+    stateful function f_u_to_dt_co_c(_ : unit) : dt_co(Cat) = DT_CO(f_u_to_c)
+
+    stateful entrypoint init() =
+        let va1 : dt_contra(Animal) = DT_CONTRA(f_a_to_u)  // success
+        let va2 : dt_contra(Animal) = DT_CONTRA(f_c_to_u)  // fail
+        let va3 : dt_contra(Cat)    = DT_CONTRA(f_a_to_u)  // success
+        let va4 : dt_contra(Cat)    = DT_CONTRA(f_c_to_u)  // success
+
+        let vb1 : dt_co(Animal) = DT_CO(f_u_to_a)  // success
+        let vb2 : dt_co(Animal) = DT_CO(f_u_to_c)  // success
+        let vb3 : dt_co(Cat)    = DT_CO(f_u_to_a)  // fail
+        let vb4 : dt_co(Cat)    = DT_CO(f_u_to_c)  // success
+
+        let vc1 : dt_inv(Animal) = DT_INV(f_a_to_a)  // success
+        let vc2 : dt_inv(Animal) = DT_INV(f_a_to_c)  // success
+        let vc3 : dt_inv(Animal) = DT_INV(f_c_to_a)  // fail
+        let vc4 : dt_inv(Animal) = DT_INV(f_c_to_c)  // fail
+        let vc5 : dt_inv(Cat)    = DT_INV(f_a_to_a)  // fail
+        let vc6 : dt_inv(Cat)    = DT_INV(f_a_to_c)  // fail
+        let vc7 : dt_inv(Cat)    = DT_INV(f_c_to_a)  // fail
+        let vc8 : dt_inv(Cat)    = DT_INV(f_c_to_c)  // success
+
+        let vd1 : dt_biv(Animal) = DT_BIV(f_u_to_u) : dt_biv(Animal)  // success
+        let vd2 : dt_biv(Animal) = DT_BIV(f_u_to_u) : dt_biv(Cat)     // success
+        let vd3 : dt_biv(Cat)    = DT_BIV(f_u_to_u) : dt_biv(Animal)  // success
+        let vd4 : dt_biv(Cat)    = DT_BIV(f_u_to_u) : dt_biv(Cat)     // success
+
+        let ve1 : dt_inv_sep(Animal) = DT_INV_SEP_A(f_a_to_u)  // success
+        let ve2 : dt_inv_sep(Animal) = DT_INV_SEP_A(f_c_to_u)  // fail
+        let ve3 : dt_inv_sep(Animal) = DT_INV_SEP_B(f_u_to_a)  // success
+        let ve4 : dt_inv_sep(Animal) = DT_INV_SEP_B(f_u_to_c)  // fail
+        let ve5 : dt_inv_sep(Cat)    = DT_INV_SEP_A(f_a_to_u)  // fail
+        let ve6 : dt_inv_sep(Cat)    = DT_INV_SEP_A(f_c_to_u)  // success
+        let ve7 : dt_inv_sep(Cat)    = DT_INV_SEP_B(f_u_to_a)  // fail
+        let ve8 : dt_inv_sep(Cat)    = DT_INV_SEP_B(f_u_to_c)  // success
+
+        let vf1 : dt_co_nest_a(Animal) = DT_CO_NEST_A(f_dt_contra_a_to_u)  // success
+        let vf2 : dt_co_nest_a(Animal) = DT_CO_NEST_A(f_dt_contra_c_to_u)  // success
+        let vf3 : dt_co_nest_a(Cat)    = DT_CO_NEST_A(f_dt_contra_a_to_u)  // fail
+        let vf4 : dt_co_nest_a(Cat)    = DT_CO_NEST_A(f_dt_contra_c_to_u)  // success
+
+        let vg1 : dt_contra_nest_a(Animal) = DT_CONTRA_NEST_A(f_dt_co_a_to_u)  // success
+        let vg2 : dt_contra_nest_a(Animal) = DT_CONTRA_NEST_A(f_dt_co_c_to_u)  // fail
+        let vg3 : dt_contra_nest_a(Cat)    = DT_CONTRA_NEST_A(f_dt_co_a_to_u)  // success
+        let vg4 : dt_contra_nest_a(Cat)    = DT_CONTRA_NEST_A(f_dt_co_c_to_u)  // success
+
+        let vh1 : dt_contra_nest_b(Animal) = DT_CONTRA_NEST_B(f_u_to_dt_contra_a)  // success
+        let vh2 : dt_contra_nest_b(Animal) = DT_CONTRA_NEST_B(f_u_to_dt_contra_c)  // fail
+        let vh3 : dt_contra_nest_b(Cat)    = DT_CONTRA_NEST_B(f_u_to_dt_contra_a)  // success
+        let vh4 : dt_contra_nest_b(Cat)    = DT_CONTRA_NEST_B(f_u_to_dt_contra_c)  // success
+
+        let vi1 : dt_co_nest_b(Animal) = DT_CO_NEST_B(f_u_to_dt_co_a)  // success
+        let vi2 : dt_co_nest_b(Animal) = DT_CO_NEST_B(f_u_to_dt_co_c)  // success
+        let vi3 : dt_co_nest_b(Cat)    = DT_CO_NEST_B(f_u_to_dt_co_a)  // fail
+        let vi4 : dt_co_nest_b(Cat)    = DT_CO_NEST_B(f_u_to_dt_co_c)  // success
+
+        let vj1 : dt_co_twice(Animal) = DT_CO_TWICE(f_a_to_u_to_c : (Animal => unit) => Animal) : dt_co_twice(Animal)  // success
+        let vj2 : dt_co_twice(Animal) = DT_CO_TWICE(f_c_to_u_to_c : (Cat    => unit) => Cat   ) : dt_co_twice(Cat)     // success
+        let vj3 : dt_co_twice(Cat)    = DT_CO_TWICE(f_c_to_u_to_a : (Animal => unit) => Animal) : dt_co_twice(Animal)  // fail
+        let vj4 : dt_co_twice(Cat)    = DT_CO_TWICE(f_c_to_u_to_c : (Cat    => unit) => Cat   ) : dt_co_twice(Cat)     // success
+
+        let vk01 : dt_a_contra_b_contra(Animal, Animal) = DT_A_CONTRA_B_CONTRA(f_a_to_a_to_u)  // success
+        let vk02 : dt_a_contra_b_contra(Animal, Animal) = DT_A_CONTRA_B_CONTRA(f_a_to_c_to_u)  // fail
+        let vk03 : dt_a_contra_b_contra(Animal, Animal) = DT_A_CONTRA_B_CONTRA(f_c_to_a_to_u)  // fail
+        let vk04 : dt_a_contra_b_contra(Animal, Animal) = DT_A_CONTRA_B_CONTRA(f_c_to_c_to_u)  // fail
+        let vk05 : dt_a_contra_b_contra(Animal, Cat)    = DT_A_CONTRA_B_CONTRA(f_a_to_a_to_u)  // success
+        let vk06 : dt_a_contra_b_contra(Animal, Cat)    = DT_A_CONTRA_B_CONTRA(f_a_to_c_to_u)  // success
+        let vk07 : dt_a_contra_b_contra(Animal, Cat)    = DT_A_CONTRA_B_CONTRA(f_c_to_a_to_u)  // fail
+        let vk08 : dt_a_contra_b_contra(Animal, Cat)    = DT_A_CONTRA_B_CONTRA(f_c_to_c_to_u)  // fail
+        let vk09 : dt_a_contra_b_contra(Cat, Animal)    = DT_A_CONTRA_B_CONTRA(f_a_to_a_to_u)  // success
+        let vk10 : dt_a_contra_b_contra(Cat, Animal)    = DT_A_CONTRA_B_CONTRA(f_a_to_c_to_u)  // fail
+        let vk11 : dt_a_contra_b_contra(Cat, Animal)    = DT_A_CONTRA_B_CONTRA(f_c_to_a_to_u)  // success
+        let vk12 : dt_a_contra_b_contra(Cat, Animal)    = DT_A_CONTRA_B_CONTRA(f_c_to_c_to_u)  // fail
+        let vk13 : dt_a_contra_b_contra(Cat, Cat)       = DT_A_CONTRA_B_CONTRA(f_a_to_a_to_u)  // success
+        let vk14 : dt_a_contra_b_contra(Cat, Cat)       = DT_A_CONTRA_B_CONTRA(f_a_to_c_to_u)  // success
+        let vk15 : dt_a_contra_b_contra(Cat, Cat)       = DT_A_CONTRA_B_CONTRA(f_c_to_a_to_u)  // success
+        let vk16 : dt_a_contra_b_contra(Cat, Cat)       = DT_A_CONTRA_B_CONTRA(f_c_to_c_to_u)  // success
+
+        let vl1 : dt_contra_twice(Animal) = DT_CONTRA_TWICE(f_a_to_a_to_u : Animal => Animal => unit) : dt_contra_twice(Animal)  // success
+        let vl2 : dt_contra_twice(Animal) = DT_CONTRA_TWICE(f_a_to_c_to_u : Cat    => Cat    => unit) : dt_contra_twice(Cat)     // fail
+        let vl3 : dt_contra_twice(Cat)    = DT_CONTRA_TWICE(f_a_to_a_to_u : Animal => Animal => unit) : dt_contra_twice(Animal)  // success
+        let vl4 : dt_contra_twice(Cat)    = DT_CONTRA_TWICE(f_c_to_a_to_u : Cat    => Cat    => unit) : dt_contra_twice(Cat)     // success
+
+        ()

test/contracts/polymorphism_variance_switching_oracles.aes

@@ -0,0 +1,47 @@
+contract interface Animal =
+    entrypoint sound : () => string
+
+contract Cat : Animal =
+    entrypoint sound() = "meow"
+
+main contract Main =
+    entrypoint oracle() = ok_2YNyxd6TRJPNrTcEDCe9ra59SVUdp9FR9qWC5msKZWYD9bP9z5
+
+    entrypoint query() = oq_2oRvyowJuJnEkxy58Ckkw77XfWJrmRgmGaLzhdqb67SKEL1gPY
+
+    entrypoint init() =
+        let o01 : oracle(Animal, Animal) = oracle() : oracle(Animal, Animal)  // success
+        let o02 : oracle(Animal, Animal) = oracle() : oracle(Animal, Cat)     // success
+        let o03 : oracle(Animal, Animal) = oracle() : oracle(Cat, Animal)     // fail
+        let o04 : oracle(Animal, Animal) = oracle() : oracle(Cat, Cat)        // fail
+        let o05 : oracle(Animal, Cat)    = oracle() : oracle(Animal, Animal)  // fail
+        let o06 : oracle(Animal, Cat)    = oracle() : oracle(Animal, Cat)     // success
+        let o07 : oracle(Animal, Cat)    = oracle() : oracle(Cat, Animal)     // fail
+        let o08 : oracle(Animal, Cat)    = oracle() : oracle(Cat, Cat)        // fail
+        let o09 : oracle(Cat, Animal)    = oracle() : oracle(Animal, Animal)  // success
+        let o10 : oracle(Cat, Animal)    = oracle() : oracle(Animal, Cat)     // success
+        let o11 : oracle(Cat, Animal)    = oracle() : oracle(Cat, Animal)     // success
+        let o12 : oracle(Cat, Animal)    = oracle() : oracle(Cat, Cat)        // success
+        let o13 : oracle(Cat, Cat)       = oracle() : oracle(Animal, Animal)  // fail
+        let o14 : oracle(Cat, Cat)       = oracle() : oracle(Animal, Cat)     // success
+        let o15 : oracle(Cat, Cat)       = oracle() : oracle(Cat, Animal)     // fail
+        let o16 : oracle(Cat, Cat)       = oracle() : oracle(Cat, Cat)        // success
+
+        let q01 : oracle_query(Animal, Animal) = query() : oracle_query(Animal, Animal)  // success
+        let q02 : oracle_query(Animal, Animal) = query() : oracle_query(Animal, Cat)     // success
+        let q03 : oracle_query(Animal, Animal) = query() : oracle_query(Cat, Animal)     // success
+        let q04 : oracle_query(Animal, Animal) = query() : oracle_query(Cat, Cat)        // success
+        let q05 : oracle_query(Animal, Cat)    = query() : oracle_query(Animal, Animal)  // fail
+        let q06 : oracle_query(Animal, Cat)    = query() : oracle_query(Animal, Cat)     // success
+        let q07 : oracle_query(Animal, Cat)    = query() : oracle_query(Cat, Animal)     // fail
+        let q08 : oracle_query(Animal, Cat)    = query() : oracle_query(Cat, Cat)        // success
+        let q09 : oracle_query(Cat, Animal)    = query() : oracle_query(Animal, Animal)  // fail
+        let q10 : oracle_query(Cat, Animal)    = query() : oracle_query(Animal, Cat)     // fail
+        let q11 : oracle_query(Cat, Animal)    = query() : oracle_query(Cat, Animal)     // success
+        let q12 : oracle_query(Cat, Animal)    = query() : oracle_query(Cat, Cat)        // success
+        let q13 : oracle_query(Cat, Cat)       = query() : oracle_query(Animal, Animal)  // fail
+        let q14 : oracle_query(Cat, Cat)       = query() : oracle_query(Animal, Cat)     // fail
+        let q15 : oracle_query(Cat, Cat)       = query() : oracle_query(Cat, Animal)     // fail
+        let q16 : oracle_query(Cat, Cat)       = query() : oracle_query(Cat, Cat)        // success
+
+        ()

test/contracts/polymorphism_variance_switching_records.aes

@@ -0,0 +1,51 @@
+contract interface Animal =
+    entrypoint sound : () => string
+
+contract Cat : Animal =
+    entrypoint sound() = "meow"
+
+main contract Main =
+    record rec_co('a)     = { x : 'a ,
+                              y : () => 'a }
+    record rec_contra('a) = { x : 'a => unit }
+    record rec_inv('a)    = { x : 'a => unit,
+                              y : () => 'a }
+    record rec_biv('a)    = { x : int }
+
+    stateful entrypoint new_cat() : Cat = Chain.create()
+    stateful entrypoint new_animal() : Animal = new_cat()
+    stateful entrypoint animal_to_unit(_ : Animal) : unit = ()
+    stateful entrypoint cat_to_unit(_ : Cat) : unit = ()
+    stateful entrypoint unit_to_animal() : Animal = new_animal()
+    stateful entrypoint unit_to_cat() : Cat = new_cat()
+
+    stateful entrypoint init() =
+        let ra  : rec_co(Animal) = { x = new_animal(), y = unit_to_animal }
+        let rc  : rec_co(Cat)    = { x = new_cat(), y = unit_to_cat }
+        let r01 : rec_co(Animal) = ra  // success
+        let r02 : rec_co(Animal) = rc  // success
+        let r03 : rec_co(Cat)    = ra  // fail
+        let r04 : rec_co(Cat)    = rc  // sucess
+
+        let ratu : rec_contra(Animal) = { x = animal_to_unit }
+        let rctu : rec_contra(Cat)    = { x = cat_to_unit }
+        let r05  : rec_contra(Animal) = ratu  // success
+        let r06  : rec_contra(Animal) = rctu  // fail
+        let r07  : rec_contra(Cat)    = ratu  // success
+        let r08  : rec_contra(Cat)    = rctu  // success
+
+        let rxaya : rec_inv(Animal) = { x = animal_to_unit, y = unit_to_animal }
+        let rxcyc : rec_inv(Cat)    = { x = cat_to_unit, y = unit_to_cat }
+        let r09   : rec_inv(Animal) = rxaya  // success
+        let r10   : rec_inv(Animal) = rxcyc  // fail
+        let r11   : rec_inv(Cat)    = rxaya  // fail
+        let r12   : rec_inv(Cat)    = rxcyc  // success
+
+        let rba : rec_biv(Animal) = { x = 1 }
+        let rbc : rec_biv(Cat)    = { x = 1 }
+        let r13 : rec_biv(Animal) = rba  // success
+        let r14 : rec_biv(Animal) = rbc  // success
+        let r15 : rec_biv(Cat)    = rba  // success
+        let r16 : rec_biv(Cat)    = rbc  // success
+
+        ()

test/contracts/test.aes

@@ -1,4 +1,12 @@
-contract ShareTwo =                                                                           
-  record state = {s1 : int, s2 : int}                                                         
-  entrypoint init() = {s1 = 0, s2 = 0}                                                        
-  stateful entrypoint buy() = ()
+// This is a custom test file if you need to run a compiler without
+// changing aeso_compiler_tests.erl
+
+include "List.aes"
+
+contract IntegerHolder =
+  type state = int
+  entrypoint init(x) = x
+  entrypoint get() = state
+
+main contract Test =
+  stateful entrypoint f(c) = Chain.clone(ref=c, 123)