Polymorphism support (#357)

* Add polymorphism to syntax tree and parser

* Add polymorphism to infer types

* Fix pretty printing

* Add new tests and fix old tests

* Fix the comparison between unit and empty tuple

* Report undefined interface errors before checking implemented interfaces

* Add test for implementing multiple interfaces

* Add test for implementing two interfaces with entrypoints of same names and different types

* Add tests for interfaces implementing interfaces

* Draft: Add variance switching

* Revert "Draft: Add variance switching"

This reverts commit 92dc6ac169cfbff447ed59de04994f564876b3fb.

* Add variance switching

* Fix broken tests

* Fix broken abi tests

* Add tests for variance switching

* Fix tests after rebase

* Variance switching for custom datatypes

* Fix dialyzer warning

* Add testing for custom types variance switching

* Make opposite_variance a separate function

* Make is_subtype/4 a separate function

* Fix warning

* Mark tvars as invariant

* Add type_vars_uvar ets table to ets_tables()

* Don't destroy and recreate type errors table when not needed

* Fixes from the reviews

* Use is_list to check if a var is a list

* Compare named args in fun_t

* Test only for covariance and contravariance

* Remove arrows_in_type and use infer_type_vars_variance instead

* Add tests for option and type aliases

* Fix previous commit

* Rename check_implemented_interfaces_recursive to check_implemented_interfaces1

* Make interfaces declare functions from extended interfaces

* Restore test.aes

* Add test for variance switching in records

* Enable variance switching for record types

* Handle builtin types type variables separately

* Add tests for oracles and oracle queries

* Replace compare_types with non-throwing version of unify

* Add the context to unification error

* Test variance switching for bivariant records

* Give clear names to the records in records variance switching test

* Handle comments about polymorphism_variance_switching.aes

* Rename datatypes in custom types variance switching test for readability

* Change the variance of the oracle_query type vars

* Add test for accessing maps with the wrong type

* Default to invariant when the variance of the type vars is unknown

* Rename test files to have common prefix

* Rename functions in variance switching tests for readability

* Fix variance inference

* Eliminate redundant tests

* Test all cases for bivariant

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_infer_types.erl

@@ -113,6 +113,8 @@
 
 -type type_constraints() :: none | bytes_concat | bytes_split | address_to_contract | bytecode_hash.
 
+-type variance() :: invariant | covariant | contravariant | bivariant.
+
 -type fun_info()  :: {aeso_syntax:ann(), typesig() | type()}.
 -type type_info() :: {aeso_syntax:ann(), typedef()}.
 -type var_info()  :: {aeso_syntax:ann(), utype()}.
@@ -134,11 +136,13 @@
     , 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
     }).
@@ -280,7 +284,7 @@ contract_call_type({fun_t, Ann, [], Args, Ret}) ->
      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, Contents}, Env)
+bind_contract({Contract, Ann, Id, _Impls, Contents}, Env)
   when ?IS_CONTRACT_HEAD(Contract) ->
     Key    = name(Id),
     Sys    = [{origin, system}],
@@ -818,6 +822,14 @@ infer(Contracts, Options) ->
         ets_new(defined_contracts, [bag]),
         ets_new(type_vars, [set]),
         ets_new(warnings, [bag]),
+        ets_new(type_vars_variance, [set]),
+        %% Set the variance for builtin types
+        ets_insert(type_vars_variance, {"list", [covariant]}),
+        ets_insert(type_vars_variance, {"option", [covariant]}),
+        ets_insert(type_vars_variance, {"map", [covariant, covariant]}),
+        ets_insert(type_vars_variance, {"oracle", [contravariant, covariant]}),
+        ets_insert(type_vars_variance, {"oracle_query", [covariant, covariant]}),
+
         when_warning(warn_unused_functions, fun() -> create_unused_functions() end),
         check_modifiers(Env, Contracts),
         create_type_errors(),
@@ -845,9 +857,12 @@ infer(Contracts, Options) ->
 -spec infer1(env(), [aeso_syntax:decl()], [aeso_syntax:decl()], list(option())) ->
     {env(), [aeso_syntax:decl()]}.
 infer1(Env, [], Acc, _Options) -> {Env, lists:reverse(Acc)};
-infer1(Env, [{Contract, Ann, ConName, Code} | Rest], Acc, Options)
+infer1(Env0, [{Contract, Ann, ConName, Impls, Code} | Rest], Acc, Options)
   when ?IS_CONTRACT_HEAD(Contract) ->
     %% do type inference on each contract independently.
+    Env = Env0#env{ contract_parents = maps:put(name(ConName),
+                                                [name(Impl) || Impl <- Impls],
+                                                Env0#env.contract_parents) },
     check_scope_name_clash(Env, contract, ConName),
     What = case Contract of
                contract_main -> contract;
@@ -859,7 +874,8 @@ infer1(Env, [{Contract, Ann, ConName, Code} | Rest], Acc, Options)
         contract_interface -> ok
     end,
     {Env1, Code1} = infer_contract_top(push_scope(contract, ConName, Env), What, Code, Options),
-    Contract1 = {Contract, Ann, ConName, Code1},
+    Contract1 = {Contract, Ann, ConName, Impls, Code1},
+    check_implemented_interfaces(Env1, Contract1, Acc),
     Env2 = pop_scope(Env1),
     Env3 = bind_contract(Contract1, Env2),
     infer1(Env3, Rest, [Contract1 | Acc], Options);
@@ -879,17 +895,66 @@ infer1(Env, [{pragma, _, _} | Rest], Acc, Options) ->
     %% Pragmas are checked in check_modifiers
     infer1(Env, Rest, Acc, Options).
 
+check_implemented_interfaces(Env, {_Contract, _Ann, ConName, Impls, Code}, DefinedContracts) ->
+    create_type_errors(),
+    AllInterfaces = [{name(IName), I} || I = {contract_interface, _, IName, _, _} <- DefinedContracts],
+    ImplsNames = lists:map(fun name/1, Impls),
+
+    %% All implemented intrefaces should already be defined
+    lists:foreach(fun(Impl) -> case proplists:get_value(name(Impl), AllInterfaces) of
+                                   undefined -> type_error({referencing_undefined_interface, Impl});
+                                   _         -> ok
+                               end
+                  end, Impls),
+
+    ImplementedInterfaces = [I || I <- [proplists:get_value(Name, AllInterfaces) || Name <- ImplsNames],
+                                    I /= undefined],
+    Funs = [ Fun || Fun <- Code,
+                    element(1, Fun) == letfun orelse element(1, Fun) == fun_decl ],
+    check_implemented_interfaces1(Env, ImplementedInterfaces, ConName, Funs, AllInterfaces),
+    destroy_and_report_type_errors(Env).
+
+%% Recursively check that all directly and indirectly referenced interfaces are implemented
+check_implemented_interfaces1(_, [], _, _, _) ->
+    ok;
+check_implemented_interfaces1(Env, [{contract_interface, _, IName, _, Decls} | Interfaces],
+                              ConId, Impls, AllInterfaces) ->
+    Unmatched = match_impls(Env, Decls, ConId, name(IName), Impls),
+    check_implemented_interfaces1(Env, Interfaces, ConId, Unmatched, AllInterfaces).
+
+%% Match the functions of the contract with the interfaces functions, and return unmatched functions
+match_impls(_, [], _, _, Impls) ->
+    Impls;
+match_impls(Env, [{fun_decl, _, {id, _, FunName}, FunType = {fun_t, _, _, ArgsTypes, RetDecl}} | Decls], ConId, IName, Impls) ->
+    Match = fun({letfun, _, {id, _, FName}, Args, RetFun, _}) when FName == FunName ->
+                    length(ArgsTypes) == length(Args) andalso
+                    unify(Env#env{unify_throws = false}, RetDecl, RetFun, unknown) andalso
+                    lists:all(fun({T1, {typed, _, _, T2}}) -> unify(Env#env{unify_throws = false}, T1, T2, unknown) end,
+                              lists:zip(ArgsTypes, Args));
+               ({fun_decl, _, {id, _, FName}, FunT}) when FName == FunName ->
+                    unify(Env#env{unify_throws = false}, FunT, FunType, unknown);
+               (_) -> false
+            end,
+    UnmatchedImpls = case lists:search(Match, Impls) of
+                         {value, V} ->
+                             lists:delete(V, Impls);
+                         false ->
+                             type_error({unimplemented_interface_function, ConId, IName, FunName}),
+                             Impls
+                     end,
+    match_impls(Env, Decls, ConId, IName, UnmatchedImpls).
+
 %% Asserts that the main contract is somehow defined.
 identify_main_contract(Contracts, Options) ->
-    Children   = [C || C = {contract_child, _, _, _} <- Contracts],
+    Children   = [C || C = {contract_child, _, _, _, _} <- Contracts],
-    Mains      = [C || C = {contract_main, _, _, _} <- Contracts],
+    Mains      = [C || C = {contract_main, _, _, _, _} <- Contracts],
     case Mains of
         [] -> case Children of
                   [] -> type_error(
                           {main_contract_undefined,
                            [{file, File} || {src_file, File} <- Options]});
-                  [{contract_child, Ann, Con, Body}] ->
+                  [{contract_child, Ann, Con, Impls, Body}] ->
-                      (Contracts -- Children) ++ [{contract_main, Ann, Con, Body}];
+                      (Contracts -- Children) ++ [{contract_main, Ann, Con, Impls, Body}];
                   [H|_] -> type_error({ambiguous_main_contract,
                                        aeso_syntax:get_ann(H)})
               end;
@@ -1039,11 +1104,15 @@ check_typedef_sccs(Env, TypeMap, [{acyclic, Name} | SCCs], Acc) ->
                     type_error({empty_record_definition, Ann, Name}),
                     check_typedef_sccs(Env1, TypeMap, SCCs, Acc1);
                 {record_t, Fields} ->
+                    ets_insert(type_vars_variance, {Env#env.namespace ++ qname(D),
+                                                    infer_type_vars_variance(Xs, Fields)}),
                     %% check_type to get qualified name
                     RecTy = check_type(Env1, app_t(Ann, D, Xs)),
                     Env2 = check_fields(Env1, TypeMap, RecTy, Fields),
                     check_typedef_sccs(Env2, TypeMap, SCCs, Acc1);
                 {variant_t, Cons} ->
+                    ets_insert(type_vars_variance, {Env#env.namespace ++ qname(D),
+                                                    infer_type_vars_variance(Xs, Cons)}),
                     Target   = check_type(Env1, app_t(Ann, D, Xs)),
                     ConType  = fun([]) -> Target; (Args) -> {type_sig, Ann, none, [], Args, Target} end,
                     ConTypes = [ begin
@@ -1069,6 +1138,48 @@ check_typedef(Env, {variant_t, Cons}) ->
     {variant_t, [ {constr_t, Ann, Con, [ check_type(Env, Arg) || Arg <- Args ]}
                 || {constr_t, Ann, Con, Args} <- Cons ]}.
 
+infer_type_vars_variance(TypeParams, Cons) ->
+    % args from all type constructors
+    FlatArgs = lists:flatten([Args || {constr_t, _, _, Args} <- Cons]) ++ [Type || {field_t, _, _, Type} <- Cons],
+
+    Vs = lists:flatten([infer_type_vars_variance(Arg) || Arg <- FlatArgs]),
+    lists:map(fun({tvar, _, TVar}) ->
+                      S = sets:from_list([Variance || {TV, Variance} <- Vs, TV == TVar]),
+                      IsCovariant     = sets:is_element(covariant, S),
+                      IsContravariant = sets:is_element(contravariant, S),
+                      case {IsCovariant, IsContravariant} of
+                          {true,   true} -> invariant;
+                          {true,  false} -> covariant;
+                          {false,  true} -> contravariant;
+                          {false, false} -> bivariant
+                      end
+              end, TypeParams).
+
+-spec infer_type_vars_variance(utype()) -> [{name(), variance()}].
+infer_type_vars_variance(Types)
+  when is_list(Types) ->
+    lists:flatten([infer_type_vars_variance(T) || T <- Types]);
+infer_type_vars_variance({app_t, _, Type, Args}) ->
+    Variances = case ets_lookup(type_vars_variance, qname(Type)) of
+                    [{_, Vs}] -> Vs;
+                    _ -> lists:duplicate(length(Args), covariant)
+                end,
+    TypeVarsVariance = [{TVar, Variance}
+                        || {{tvar, _, TVar}, Variance} <- lists:zip(Args, Variances)],
+    TypeVarsVariance;
+infer_type_vars_variance({tvar, _, TVar}) -> [{TVar, covariant}];
+infer_type_vars_variance({fun_t, _, [], Args, Res}) ->
+    ArgsVariance = infer_type_vars_variance(Args),
+    ResVariance = infer_type_vars_variance(Res),
+    FlippedArgsVariance = lists:map(fun({TVar, Variance}) -> {TVar, opposite_variance(Variance)} end, ArgsVariance),
+    FlippedArgsVariance ++ ResVariance;
+infer_type_vars_variance(_) -> [].
+
+opposite_variance(invariant) -> invariant;
+opposite_variance(covariant) -> contravariant;
+opposite_variance(contravariant) -> covariant;
+opposite_variance(bivariant) -> bivariant.
+
 check_usings(Env, []) ->
     Env;
 check_usings(Env = #env{ used_namespaces = UsedNamespaces }, [{using, Ann, Con, Alias, Parts} | Rest]) ->
@@ -1114,7 +1225,7 @@ check_modifiers(Env, Contracts) ->
     check_modifiers_(Env, Contracts),
     destroy_and_report_type_errors(Env).
 
-check_modifiers_(Env, [{Contract, _, Con, Decls} | Rest])
+check_modifiers_(Env, [{Contract, _, Con, _Impls, Decls} | Rest])
   when ?IS_CONTRACT_HEAD(Contract) ->
     IsInterface = Contract =:= contract_interface,
     check_modifiers1(contract, Decls),
@@ -1398,7 +1509,7 @@ infer_letfun(Env = #env{ namespace = Namespace }, LetFun = {letfun, Ann, Fun, _,
     {{Name, Sig}, Clause} = infer_letfun1(Env, LetFun),
     {{Name, Sig}, desugar_clauses(Ann, Fun, Sig, [Clause])}.
 
-infer_letfun1(Env0 = #env{ namespace = NS }, {letfun, Attrib, Fun = {id, NameAttrib, Name}, Args, What,  GuardedBodies}) ->
+infer_letfun1(Env0 = #env{ namespace = NS }, {letfun, Attrib, Fun = {id, NameAttrib, Name}, Args, What, GuardedBodies}) ->
     Env = Env0#env{ stateful = aeso_syntax:get_ann(stateful, Attrib, false),
                     current_function = Fun },
     {NewEnv, {typed, _, {tuple, _, TypedArgs}, {tuple_t, _, ArgTypes}}} = infer_pattern(Env, {tuple, [{origin, system} | NameAttrib], Args}),
@@ -1908,7 +2019,7 @@ infer_case(Env = #env{ namespace = NS, current_function = {id, _, Fun} }, Attrs,
         {guarded, Ann, NewGuards, NewBranch}
     end,
     NewGuardedBranches = lists:map(InferGuardedBranches, GuardedBranches),
-    unify(Env, PatType, ExprType, {case_pat, Pattern, PatType, ExprType}),
+    unify(Env, ExprType, PatType, {case_pat, Pattern, PatType, ExprType}),
     {'case', Attrs, NewPattern, NewGuardedBranches}.
 
 %% NewStmts = infer_block(Env, Attrs, Stmts, BlockType)
@@ -2016,7 +2127,8 @@ next_count() ->
 
 ets_tables() ->
     [options, type_vars, constraints, freshen_tvars, type_errors,
-     defined_contracts, warnings, function_calls, all_functions].
+     defined_contracts, warnings, function_calls, all_functions,
+     type_vars_variance].
 
 clean_up_ets() ->
     [ catch ets_delete(Tab) || Tab <- ets_tables() ],
@@ -2556,9 +2668,11 @@ subst_tvars1(_Env, X) ->
 
 %% Unification
 
-unify(_, {id, _, "_"}, _, _When) -> true;
+unify(Env, A, B, When) -> unify0(Env, A, B, covariant, When).
-unify(_, _, {id, _, "_"}, _When) -> true;
+
-unify(Env, A, B, When) ->
+unify0(_, {id, _, "_"}, _, _Variance, _When) -> true;
+unify0(_, _, {id, _, "_"}, _Variance, _When) -> true;
+unify0(Env, A, B, Variance, When) ->
     Options =
         case When of    %% Improve source location for map_in_map_key errors
             {check_expr, E, _, _} -> [{ann, aeso_syntax:get_ann(E)}];
@@ -2566,68 +2680,129 @@ unify(Env, A, B, When) ->
         end,
     A1 = dereference(unfold_types_in_type(Env, A, Options)),
     B1 = dereference(unfold_types_in_type(Env, B, Options)),
-    unify1(Env, A1, B1, When).
+    unify1(Env, A1, B1, Variance, When).
 
-unify1(_Env, {uvar, _, R}, {uvar, _, R}, _When) ->
+unify1(_Env, {uvar, _, R}, {uvar, _, R}, _Variance, _When) ->
     true;
-unify1(_Env, {uvar, A, R}, T, When) ->
+unify1(Env, {uvar, A, R}, T, _Variance, When) ->
     case occurs_check(R, T) of
         true ->
-            cannot_unify({uvar, A, R}, T, When),
+            if
+                Env#env.unify_throws ->
+                    cannot_unify({uvar, A, R}, T, none, When);
+                true ->
+                    ok
+            end,
             false;
         false ->
             ets_insert(type_vars, {R, T}),
             true
     end;
-unify1(Env, T, {uvar, A, R}, When) ->
+unify1(Env, T, {uvar, A, R}, Variance, When) ->
-    unify1(Env, {uvar, A, R}, T, When);
+    unify1(Env, {uvar, A, R}, T, Variance, When);
-unify1(_Env, {tvar, _, X}, {tvar, _, X}, _When) -> true; %% Rigid type variables
+unify1(_Env, {tvar, _, X}, {tvar, _, X}, _Variance, _When) -> true; %% Rigid type variables
-unify1(Env, [A|B], [C|D], When) ->
+unify1(Env, [A|B], [C|D], [V|Variances], When) ->
-    unify(Env, A, C, When) andalso unify(Env, B, D, When);
+    unify0(Env, A, C, V, When) andalso unify0(Env, B, D, Variances, When);
-unify1(_Env, X, X, _When) ->
+unify1(Env, [A|B], [C|D], Variance, When) ->
+    unify0(Env, A, C, Variance, When) andalso unify0(Env, B, D, Variance, When);
+unify1(_Env, X, X, _Variance, _When) ->
     true;
-unify1(_Env, {id, _, Name}, {id, _, Name}, _When) ->
+unify1(_Env, {id, _, Name}, {id, _, Name}, _Variance, _When) ->
     true;
-unify1(_Env, {con, _, Name}, {con, _, Name}, _When) ->
+unify1(Env, A = {con, _, NameA}, B = {con, _, NameB}, Variance, When) ->
+    case is_subtype(Env, NameA, NameB, Variance) of
+        true -> true;
+        false ->
+            if
+                Env#env.unify_throws ->
+                    IsSubtype = is_subtype(Env, NameA, NameB, contravariant) orelse
+                                is_subtype(Env, NameA, NameB, covariant),
+                    Cxt = case IsSubtype of
+                              true  -> Variance;
+                              false -> none
+                          end,
+                    cannot_unify(A, B, Cxt, When);
+                true ->
+                    ok
+            end,
+            false
+    end;
+unify1(_Env, {qid, _, Name}, {qid, _, Name}, _Variance, _When) ->
     true;
-unify1(_Env, {qid, _, Name}, {qid, _, Name}, _When) ->
+unify1(_Env, {qcon, _, Name}, {qcon, _, Name}, _Variance, _When) ->
     true;
-unify1(_Env, {qcon, _, Name}, {qcon, _, Name}, _When) ->
+unify1(_Env, {bytes_t, _, Len}, {bytes_t, _, Len}, _Variance, _When) ->
     true;
-unify1(_Env, {bytes_t, _, Len}, {bytes_t, _, Len}, _When) ->
+unify1(Env, {if_t, _, {id, _, Id}, Then1, Else1}, {if_t, _, {id, _, Id}, Then2, Else2}, Variance, When) ->
-    true;
+    unify0(Env, Then1, Then2, Variance, When) andalso
-unify1(Env, {if_t, _, {id, _, Id}, Then1, Else1}, {if_t, _, {id, _, Id}, Then2, Else2}, When) ->
+    unify0(Env, Else1, Else2, Variance, When);
-    unify(Env, Then1, Then2, When) andalso
-    unify(Env, Else1, Else2, When);
 
-unify1(_Env, {fun_t, _, _, _, _}, {fun_t, _, _, var_args, _}, When) ->
+unify1(_Env, {fun_t, _, _, _, _}, {fun_t, _, _, var_args, _}, _Variance, When) ->
     type_error({unify_varargs, When});
-unify1(_Env, {fun_t, _, _, var_args, _}, {fun_t, _, _, _, _}, When) ->
+unify1(_Env, {fun_t, _, _, var_args, _}, {fun_t, _, _, _, _}, _Variance, When) ->
     type_error({unify_varargs, When});
-unify1(Env, {fun_t, _, Named1, Args1, Result1}, {fun_t, _, Named2, Args2, Result2}, When)
+unify1(Env, {fun_t, _, Named1, Args1, Result1}, {fun_t, _, Named2, Args2, Result2}, Variance, When)
   when length(Args1) == length(Args2) ->
-    unify(Env, Named1, Named2, When) andalso
+    unify0(Env, Named1, Named2, opposite_variance(Variance), When) andalso
-    unify(Env, Args1, Args2, When) andalso unify(Env, Result1, Result2, When);
+    unify0(Env, Args1, Args2, opposite_variance(Variance), When) andalso
-unify1(Env, {app_t, _, {Tag, _, F}, Args1}, {app_t, _, {Tag, _, F}, Args2}, When)
+    unify0(Env, Result1, Result2, Variance, When);
+unify1(Env, {app_t, _, {Tag, _, F}, Args1}, {app_t, _, {Tag, _, F}, Args2}, Variance, When)
   when length(Args1) == length(Args2), Tag == id orelse Tag == qid ->
-    unify(Env, Args1, Args2, When);
+    Variances = case ets_lookup(type_vars_variance, F) of
-unify1(Env, {tuple_t, _, As}, {tuple_t, _, Bs}, When)
+                    [{_, Vs}] ->
+                        case Variance of
+                            contravariant -> lists:map(fun opposite_variance/1, Vs);
+                            invariant     -> invariant;
+                            _             -> Vs
+                        end;
+                    _ -> invariant
+                end,
+    unify1(Env, Args1, Args2, Variances, When);
+unify1(Env, {tuple_t, _, As}, {tuple_t, _, Bs}, Variance, When)
   when length(As) == length(Bs) ->
-    unify(Env, As, Bs, When);
+    unify0(Env, As, Bs, Variance, When);
-unify1(Env, {named_arg_t, _, Id1, Type1, _}, {named_arg_t, _, Id2, Type2, _}, When) ->
+unify1(Env, {named_arg_t, _, Id1, Type1, _}, {named_arg_t, _, Id2, Type2, _}, Variance, When) ->
-    unify1(Env, Id1, Id2, {arg_name, Id1, Id2, When}),
+    unify1(Env, Id1, Id2, Variance, {arg_name, Id1, Id2, When}),
-    unify1(Env, Type1, Type2, When);
+    unify1(Env, Type1, Type2, Variance, When);
 %% The grammar is a bit inconsistent about whether types without
 %% arguments are represented as applications to an empty list of
 %% parameters or not. We therefore allow them to unify.
-unify1(Env, {app_t, _, T, []}, B, When) ->
+unify1(Env, {app_t, _, T, []}, B, Variance, When) ->
-    unify(Env, T, B, When);
+    unify0(Env, T, B, Variance, When);
-unify1(Env, A, {app_t, _, T, []}, When) ->
+unify1(Env, A, {app_t, _, T, []}, Variance, When) ->
-    unify(Env, A, T, When);
+    unify0(Env, A, T, Variance, When);
-unify1(_Env, A, B, When) ->
+unify1(Env, A, B, _Variance, When) ->
-    cannot_unify(A, B, When),
+    if
+        Env#env.unify_throws ->
+            cannot_unify(A, B, none, When);
+        true ->
+            ok
+    end,
     false.
 
+is_subtype(_Env, NameA, NameB, invariant) ->
+    NameA == NameB;
+is_subtype(Env, NameA, NameB, covariant) ->
+    is_subtype(Env, NameA, NameB);
+is_subtype(Env, NameA, NameB, contravariant) ->
+    is_subtype(Env, NameB, NameA);
+is_subtype(Env, NameA, NameB, bivariant) ->
+    is_subtype(Env, NameA, NameB) orelse is_subtype(Env, NameB, NameA).
+
+is_subtype(Env, Child, Base) ->
+    Parents = maps:get(Child, Env#env.contract_parents, []),
+    if
+        Child == Base ->
+            true;
+        Parents == [] ->
+            false;
+        true ->
+            case lists:member(Base, Parents) of
+                true -> true;
+                false -> lists:any(fun(Parent) -> is_subtype(Env, Parent, Base) end, Parents)
+            end
+    end.
+
 dereference(T = {uvar, _, R}) ->
     case ets_lookup(type_vars, R) of
         [] ->
@@ -2910,8 +3085,8 @@ warn_potential_negative_spend(Ann, Fun, Args) ->
 
 %% Save unification failures for error messages.
 
-cannot_unify(A, B, When) ->
+cannot_unify(A, B, Cxt, When) ->
-    type_error({cannot_unify, A, B, When}).
+    type_error({cannot_unify, A, B, Cxt, When}).
 
 type_error(Err) ->
     ets_insert(type_errors, Err).
@@ -2980,8 +3155,12 @@ mk_error({fundecl_must_have_funtype, _Ann, Id, Type}) ->
                        "Entrypoints and functions must have functional types"
                        , [pp(Id), pp(instantiate(Type))]),
     mk_t_err(pos(Id), Msg);
-mk_error({cannot_unify, A, B, When}) ->
+mk_error({cannot_unify, A, B, Cxt, When}) ->
-    Msg = io_lib:format("Cannot unify `~s` and `~s`",
+    VarianceContext = case Cxt of
+                          none -> "";
+                          _    -> io_lib:format(" in a ~p context", [Cxt])
+                      end,
+    Msg = io_lib:format("Cannot unify `~s` and `~s`" ++ VarianceContext,
                         [pp(instantiate(A)), pp(instantiate(B))]),
     {Pos, Ctxt} = pp_when(When),
     mk_t_err(Pos, Msg, Ctxt);
@@ -3112,7 +3291,7 @@ mk_error({namespace, _Pos, {con, Pos, Name}, _Def}) ->
     Msg = io_lib:format("Nested namespaces are not allowed. Namespace `~s` is not defined at top level.",
                         [Name]),
     mk_t_err(pos(Pos), Msg);
-mk_error({Contract, _Pos, {con, Pos, Name}, _Def}) when ?IS_CONTRACT_HEAD(Contract) ->
+mk_error({Contract, _Pos, {con, Pos, Name}, _Impls, _Def}) when ?IS_CONTRACT_HEAD(Contract) ->
     Msg = io_lib:format("Nested contracts are not allowed. Contract `~s` is not defined at top level.",
                         [Name]),
     mk_t_err(pos(Pos), Msg);
@@ -3299,6 +3478,12 @@ mk_error({unknown_warning, Warning}) ->
 mk_error({empty_record_definition, Ann, Name}) ->
     Msg = io_lib:format("Empty record definitions are not allowed. Cannot define the record `~s`", [Name]),
     mk_t_err(pos(Ann), Msg);
+mk_error({unimplemented_interface_function, ConId, InterfaceName, FunName}) ->
+    Msg = io_lib:format("Unimplemented function `~s` from the interface `~s` in the contract `~s`", [FunName, InterfaceName, pp(ConId)]),
+    mk_t_err(pos(ConId), Msg);
+mk_error({referencing_undefined_interface, InterfaceId}) ->
+    Msg = io_lib:format("Trying to implement or extend an undefined interface `~s`", [pp(InterfaceId)]),
+    mk_t_err(pos(InterfaceId), Msg);
 mk_error(Err) ->
     Msg = io_lib:format("Unknown error: ~p", [Err]),
     mk_t_err(pos(0, 0), Msg).

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;
+        {_, _, _, _, [Decl | _]} -> aeso_syntax:get_ann(col, Decl, 1) - 1;
-        _                     -> 0
+        _                        -> 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()]}
+-type decl() :: {contract_main, ann(), con(), [con()], [decl()]}
-              | {contract_child, ann(), con(), [decl()]}
+              | {contract_child, ann(), con(), [con()], [decl()]}
-              | {contract_interface, ann(), con(), [decl()]}
+              | {contract_interface, ann(), con(), [con()], [decl()]}
               | {namespace, ann(), con(), [decl()]}
               | {pragma, ann(), pragma()}
               | {type_decl, ann(), id(), [tvar()]} % Only for error msgs

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 =                                                                           
+// This is a custom test file if you need to run a compiler without
-  record state = {s1 : int, s2 : int}                                                         
+// changing aeso_compiler_tests.erl
-  entrypoint init() = {s1 = 0, s2 = 0}                                                        
+
-  stateful entrypoint buy() = ()
+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)