Fix liveness

* 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_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],
-    Mains      = [C || C = {contract_main, _, _, _} <- Contracts],
+    Children   = [C || C = {contract_child, _, _, _, _} <- 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}] ->
-                      (Contracts -- Children) ++ [{contract_main, Ann, Con, Body}];
+                  [{contract_child, Ann, Con, Impls, 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(_, _, {id, _, "_"}, _When) -> true;
-unify(Env, A, B, When) ->
+unify(Env, A, B, When) -> unify0(Env, A, B, covariant, 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, {uvar, A, R}, T, When);
-unify1(_Env, {tvar, _, X}, {tvar, _, X}, _When) -> true; %% Rigid type variables
-unify1(Env, [A|B], [C|D], When) ->
-    unify(Env, A, C, When) andalso unify(Env, B, D, When);
-unify1(_Env, X, X, _When) ->
+unify1(Env, T, {uvar, A, R}, Variance, When) ->
+    unify1(Env, {uvar, A, R}, T, Variance, When);
+unify1(_Env, {tvar, _, X}, {tvar, _, X}, _Variance, _When) -> true; %% Rigid type variables
+unify1(Env, [A|B], [C|D], [V|Variances], When) ->
+    unify0(Env, A, C, V, When) andalso unify0(Env, B, D, Variances, 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) ->
-    true;
-unify1(Env, {if_t, _, {id, _, Id}, Then1, Else1}, {if_t, _, {id, _, Id}, Then2, Else2}, When) ->
-    unify(Env, Then1, Then2, When) andalso
-    unify(Env, Else1, Else2, When);
+unify1(Env, {if_t, _, {id, _, Id}, Then1, Else1}, {if_t, _, {id, _, Id}, Then2, Else2}, Variance, When) ->
+    unify0(Env, Then1, Then2, Variance, When) andalso
+    unify0(Env, Else1, Else2, Variance, 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
-    unify(Env, Args1, Args2, When) andalso unify(Env, Result1, Result2, When);
-unify1(Env, {app_t, _, {Tag, _, F}, Args1}, {app_t, _, {Tag, _, F}, Args2}, When)
+    unify0(Env, Named1, Named2, opposite_variance(Variance), When) andalso
+    unify0(Env, Args1, Args2, opposite_variance(Variance), When) andalso
+    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);
-unify1(Env, {tuple_t, _, As}, {tuple_t, _, Bs}, When)
+    Variances = case ets_lookup(type_vars_variance, F) of
+                    [{_, 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);
-unify1(Env, {named_arg_t, _, Id1, Type1, _}, {named_arg_t, _, Id2, Type2, _}, When) ->
-    unify1(Env, Id1, Id2, {arg_name, Id1, Id2, When}),
-    unify1(Env, Type1, Type2, When);
+    unify0(Env, As, Bs, Variance, When);
+unify1(Env, {named_arg_t, _, Id1, Type1, _}, {named_arg_t, _, Id2, Type2, _}, Variance, When) ->
+    unify1(Env, Id1, Id2, Variance, {arg_name, Id1, Id2, 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) ->
-    unify(Env, T, B, When);
-unify1(Env, A, {app_t, _, T, []}, When) ->
-    unify(Env, A, T, When);
-unify1(_Env, A, B, When) ->
-    cannot_unify(A, B, When),
+unify1(Env, {app_t, _, T, []}, B, Variance, When) ->
+    unify0(Env, T, B, Variance, When);
+unify1(Env, A, {app_t, _, T, []}, Variance, When) ->
+    unify0(Env, A, T, Variance, When);
+unify1(Env, A, B, _Variance, 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) ->
-    type_error({cannot_unify, A, B, When}).
+cannot_unify(A, B, Cxt, 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}) ->
-    Msg = io_lib:format("Cannot unify `~s` and `~s`",
+mk_error({cannot_unify, A, B, Cxt, When}) ->
+    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

@@ -75,6 +75,7 @@
                | {switch, fsplit()}
                | {set_state, state_reg(), fexpr()}
                | {get_state, state_reg()}
+               | {loop, fexpr(), var_name(), fexpr()} | {continue, fexpr()} | {break, fexpr()}
                %% The following (unapplied top-level functions/builtins and
                %% lambdas) are generated by the fcode compiler, but translated
                %% to closures by the lambda lifter.
@@ -326,7 +327,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 ->
@@ -651,11 +652,22 @@ expr_to_fcode(Env, {record_t, FieldTypes}, {record, _Ann, Rec, Fields}) ->
 expr_to_fcode(Env, _Type, {list, _, Es}) ->
     lists:foldr(fun(E, L) -> {op, '::', [expr_to_fcode(Env, E), L]} end,
                 nil, Es);
-
 expr_to_fcode(Env, _Type, {app, _, {'..', _}, [A, B]}) ->
-    {def_u, FromTo, _} = resolve_fun(Env, ["ListInternal", "from_to"]),
-    {def, FromTo, [expr_to_fcode(Env, A), expr_to_fcode(Env, B)]};
-
+    AV = fresh_name(), % var to keep B
+    WithA = fun(X) -> {'let', AV, expr_to_fcode(Env, A), X} end,
+    St = fresh_name(), % loop state
+    ItProj = {proj, {var, St}, 1},
+    AcProj = {proj, {var, St}, 0},
+    Init = {tuple, [nil, expr_to_fcode(Env, B)]},
+    Loop = {loop, Init, St,
+            make_if(
+              {op, '>=', [ItProj, {var, AV}]},
+              {continue, {tuple, [{op, '::', [ItProj, AcProj]},
+                                  {op, '-', [ItProj, {lit, {int, 1}}]}
+                                 ]}},
+              {break, AcProj}
+             )},
+    WithA(Loop);
 expr_to_fcode(Env, _Type, {list_comp, _, Yield, []}) ->
     {op, '::', [expr_to_fcode(Env, Yield), nil]};
 expr_to_fcode(Env, _Type, {list_comp, As, Yield, [{comprehension_bind, Pat = {typed, _, _, PatType}, BindExpr}|Rest]}) ->
@@ -1338,6 +1350,9 @@ lambda_lift_expr(Layout, Expr) ->
         {proj, A, I}           -> {proj, lambda_lift_expr(Layout, A), I};
         {set_proj, A, I, B}    -> {set_proj, lambda_lift_expr(Layout, A), I, lambda_lift_expr(Layout, B)};
         {op, Op, As}           -> {op, Op, lambda_lift_exprs(Layout, As)};
+        {loop, Init, I, Body}  -> {loop, lambda_lift_expr(Layout, Init), I, lambda_lift_expr(Layout, Body)};
+        {break, E}             -> {break, lambda_lift_expr(Layout, E)};
+        {continue, E}          -> {continue, lambda_lift_expr(Layout, E)};
         {'let', X, A, B}       -> {'let', X, lambda_lift_expr(Layout, A), lambda_lift_expr(Layout, B)};
         {funcall, A, Bs}       -> {funcall, lambda_lift_expr(Layout, A), lambda_lift_exprs(Layout, Bs)};
         {set_state, R, A}      -> {set_state, R, lambda_lift_expr(Layout, A)};
@@ -1653,6 +1668,9 @@ read_only({switch, Split})         -> read_only(Split);
 read_only({split, _, _, Cases})    -> read_only(Cases);
 read_only({nosplit, E})            -> read_only(E);
 read_only({'case', _, Split})      -> read_only(Split);
+read_only({loop, Init, _, Body})   -> read_only(Init) andalso read_only(Body);
+read_only({break, E})              -> read_only(E);
+read_only({continue, E})           -> read_only(E);
 read_only({'let', _, A, B})        -> read_only([A, B]);
 read_only({funcall, _, _})         -> false;
 read_only({closure, _, _})         -> internal_error(no_closures_here);
@@ -1850,6 +1868,9 @@ free_vars(Expr) ->
         {proj, A, _}         -> free_vars(A);
         {set_proj, A, _, B}  -> free_vars([A, B]);
         {op, _, As}          -> free_vars(As);
+        {loop, Init, Var, Body} -> free_vars(Init) ++ (free_vars(Body) -- [Var]);
+        {break, E}           -> free_vars(E);
+        {continue, E}        -> free_vars(E);
         {'let', X, A, B}     -> free_vars([A, {lam, [X], B}]);
         {funcall, A, Bs}     -> free_vars([A | Bs]);
         {set_state, _, A}    -> free_vars(A);
@@ -1881,6 +1902,9 @@ used_defs(Expr) ->
         {proj, A, _}         -> used_defs(A);
         {set_proj, A, _, B}  -> used_defs([A, B]);
         {op, _, As}          -> used_defs(As);
+        {loop, I, _, B}      -> used_defs(I) ++ used_defs(B);
+        {break, E}           -> used_defs(E);
+        {continue, E}        -> used_defs(E);
         {'let', _, A, B}     -> used_defs([A, B]);
         {funcall, A, Bs}     -> used_defs([A | Bs]);
         {set_state, _, A}    -> used_defs(A);
@@ -1917,6 +1941,9 @@ bottom_up(F, Env, Expr) ->
         {get_state, _}                   -> Expr;
         {closure, F, CEnv}               -> {closure, F, bottom_up(F, Env, CEnv)};
         {switch, Split}                  -> {switch, bottom_up(F, Env, Split)};
+        {loop, Init, Var, Body}          -> {loop, bottom_up(F, Env, Init), Var, bottom_up(F, Env, Body)};
+        {break, E}                       -> {break, bottom_up(F, Env, E)};
+        {continue, E}                    -> {continue, bottom_up(F, Env, E)};
         {lam, Xs, B}                     -> {lam, Xs, bottom_up(F, Env, B)};
         {'let', X, E, Body}              ->
             E1 = bottom_up(F, Env, E),
@@ -1978,6 +2005,11 @@ rename(Ren, Expr) ->
         {lam, Xs, B} ->
             {Zs, Ren1} = rename_bindings(Ren, Xs),
             {lam, Zs, rename(Ren1, B)};
+        {loop, Init, Var, Body} ->
+            {Z, Ren1} = rename_binding(Ren, Var),
+            {loop, rename(Ren, Init), Z, rename(Ren1, Body)};
+        {break, E}           -> {break, rename(Ren, E)};
+        {continue, E}        -> {continue, rename(Ren, E)};
         {'let', X, E, Body} ->
             {Z, Ren1} = rename_binding(Ren, X),
             {'let', Z, rename(Ren, E), rename(Ren1, Body)}
@@ -2169,6 +2201,13 @@ pp_fexpr({tuple, Es}) ->
     pp_parens(pp_par(pp_punctuate(pp_text(","), [pp_fexpr(E) || E <- Es])));
 pp_fexpr({proj, E, I}) ->
     pp_beside([pp_fexpr(E), pp_text("."), pp_int(I)]);
+pp_fexpr({loop, Init, Var, Body}) ->
+    pp_par(
+      [ pp_beside([pp_text("loop"), pp_fexpr(Init), pp_text("as"), pp_text(Var)])
+      , pp_fexpr(Body)
+      ]);
+pp_fexpr({break, E}) -> pp_beside([pp_text("break"), pp_fexpr(E)]);
+pp_fexpr({continue, E}) -> pp_beside([pp_text("continue"), pp_fexpr(E)]);
 pp_fexpr({lam, Xs, A}) ->
     pp_par([pp_fexpr({tuple, [{var, X} || X <- Xs]}), pp_text("=>"),
             prettypr:nest(2, pp_fexpr(A))]);

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

@@ -19,6 +19,7 @@
 
 -type scode()  :: [sinstr()].
 -type sinstr() :: {switch, arg(), stype(), [maybe_scode()], maybe_scode()}  %% last arg is catch-all
+                | {loop, scode(), var(), scode(), reference(), reference()}
                 | switch_body
                 | loop
                 | tuple() | atom().    %% FATE instruction
@@ -45,7 +46,7 @@
 -define(s(N), {store, N}).
 -define(void, {var, 9999}).
 
--record(env, { contract, vars = [], locals = [], current_function, tailpos = true, child_contracts = #{}, options = []}).
+-record(env, { contract, vars = [], locals = [], break_ref = none, cont_ref = none, loop_it = none, current_function, tailpos = true, child_contracts = #{}, options = []}).
 
 %% -- Debugging --------------------------------------------------------------
 
@@ -159,6 +160,9 @@ init_env(ChildContracts, ContractName, FunNames, Name, Args, Options) ->
 next_var(#env{ vars = Vars }) ->
     1 + lists:max([-1 | [J || {_, {var, J}} <- Vars]]).
 
+bind_loop(ContRef, BreakRef, It, Env) ->
+    Env#env{break_ref = BreakRef, cont_ref = ContRef, loop_it = It}.
+
 bind_var(Name, Var, Env = #env{ vars = Vars }) ->
     Env#env{ vars = [{Name, Var} | Vars] }.
 
@@ -368,7 +372,21 @@ to_scode1(Env, {set_state, Reg, Val}) ->
 
 to_scode1(Env, {closure, Fun, FVs}) ->
     to_scode(Env, {tuple, [{lit, {string, make_function_id(Fun)}}, FVs]});
-
+to_scode1(Env, {loop, Init, It, Expr}) ->
+    ContRef = make_ref(),
+    BreakRef = make_ref(),
+    {ItV, Env1} = bind_local(It, Env),
+    InitS = [to_scode(notail(Env), Init),
+             {jump, ContRef}],
+    ExprS = [aeb_fate_ops:store({var, ItV}, {stack, 0}),
+             to_scode(bind_loop(ContRef, BreakRef, ItV, Env1), Expr),
+             {jump, BreakRef}],
+    [{loop, InitS, It, ExprS, ContRef, BreakRef}];
+to_scode1(Env = #env{cont_ref = ContRef}, {continue, Expr}) ->
+    [to_scode1(notail(Env), Expr),
+     {jump, ContRef}];
+to_scode1(Env, {break, Expr}) ->
+    to_scode1(Env, Expr);
 to_scode1(Env, {switch, Case}) ->
     split_to_scode(Env, Case).
 
@@ -712,6 +730,8 @@ flatten(Code)    -> lists:map(fun flatten_s/1, lists:flatten(Code)).
 
 flatten_s({switch, Arg, Type, Alts, Catch}) ->
     {switch, Arg, Type, [flatten(Alt) || Alt <- Alts], flatten(Catch)};
+flatten_s({loop, Init, It, Body, BRef, CRef}) ->
+    {loop, flatten(Init), It, flatten(Body), BRef, CRef};
 flatten_s(I) -> I.
 
 -define(MAX_SIMPL_ITERATIONS, 10).
@@ -808,6 +828,11 @@ ann_live1(LiveTop, {switch, Arg, Type, Alts, Def}, LiveOut) ->
     {Def1,  LiveDef}  = ann_live(LiveTop, Def, LiveOut),
     LiveIn = ordsets:union([Read, LiveDef | LiveAlts]),
     {{switch, Arg, Type, Alts1, Def1}, LiveIn};
+ann_live1(LiveTop, {loop, Init, It, Body, BRef, CRef}, LiveOut) ->
+    {Init1, LiveInit} = ann_live(LiveTop, Init, LiveOut),
+    {Body1, LiveBody} = ann_live(LiveTop, Body, LiveOut),
+    LiveIn = ordsets:union([It, LiveInit, LiveBody]), % TODO not sure about this
+    {{loop, Init1, It, Body1, BRef, CRef}, LiveIn};
 ann_live1(_LiveTop, I, LiveOut) ->
     #{ read := Reads0, write := W } = attributes(I),
     Reads   = lists:filter(fun is_reg/1, Reads0),
@@ -834,6 +859,7 @@ attributes(I) ->
     case I of
         loop                                  -> Impure(pc, []);
         switch_body                           -> Pure(none, []);
+        {jump, _}                             -> Impure(pc, []);
         'RETURN'                              -> Impure(pc, []);
         {'RETURNR', A}                        -> Impure(pc, A);
         {'CALL', A}                           -> Impure(?a, [A]);
@@ -1023,6 +1049,7 @@ var_writes(I) ->
 -spec independent(sinstr_a(), sinstr_a()) -> boolean().
 %% independent({switch, _, _, _, _}, _) -> false;       %% Commented due to Dialyzer whinging
 independent(_, {switch, _, _, _, _}) -> false;
+independent(_, {loop, _, _, _, _, _}) -> false;
 independent({i, _, I}, {i, _, J}) ->
     #{ write := WI, read := RI, pure := PureI } = attributes(I),
     #{ write := WJ, read := RJ, pure := PureJ } = attributes(J),
@@ -1061,6 +1088,8 @@ live_in(R, {i, Ann, _}) -> live_in(R, Ann);
 live_in(R, [I = {i, _, _} | _]) -> live_in(R, I);
 live_in(R, [{switch, A, _, Alts, Def} | _]) ->
     R == A orelse lists:any(fun(Code) -> live_in(R, Code) end, [Def | Alts]);
+live_in(R, [{loop, Init, Var, Expr, _, _}]) ->
+    live_in(Var, Init) orelse (R /= Var andalso live_in(R, Expr));
 live_in(_, missing) -> false;
 live_in(_, []) -> false.
 
@@ -1076,6 +1105,8 @@ simplify([I | Code], Options) ->
 
 simpl_s({switch, Arg, Type, Alts, Def}, Options) ->
     {switch, Arg, Type, [simplify(A, Options) || A <- Alts], simplify(Def, Options)};
+simpl_s({loop, Init, Var, Expr, ContRef, BreakRef}, Options) ->
+    {loop, simplify(Init, Options), Var, simplify(Expr, Options), ContRef, BreakRef};
 simpl_s(I, _) -> I.
 
 %% Safe-guard against loops in the rewriting. Shouldn't happen so throw an
@@ -1378,6 +1409,8 @@ does_abort({i, _, {'EXIT', _}}) -> true;
 does_abort(missing) -> true;
 does_abort({switch, _, _, Alts, Def}) ->
     lists:all(fun does_abort/1, [Def | Alts]);
+does_abort({loop, Init, _, Expr, _, _}) ->
+    does_abort(Init) orelse does_abort(Expr);
 does_abort(_) -> false.
 
 %% STORE R A, SWITCH R --> SWITCH A
@@ -1505,6 +1538,8 @@ from_op_view(Op, R, As) -> list_to_tuple([Op, R | As]).
                 (missing)    -> missing.
 unannotate({switch, Arg, Type, Alts, Def}) ->
     [{switch, Arg, Type, [unannotate(A) || A <- Alts], unannotate(Def)}];
+unannotate({loop, Init, It, Body, BRef, CRef}) ->
+    [{loop, unannotate(Init), It, unannotate(Body), BRef, CRef}];
 unannotate(missing) -> missing;
 unannotate(Code) when is_list(Code) ->
     lists:flatmap(fun unannotate/1, Code);
@@ -1521,6 +1556,8 @@ desugar({'STORE', ?a, A})       -> [aeb_fate_ops:push(desugar_arg(A))];
 desugar({'STORE', R, ?a})       -> [aeb_fate_ops:pop(desugar_arg(R))];
 desugar({switch, Arg, Type, Alts, Def}) ->
     [{switch, desugar_arg(Arg), Type, [desugar(A) || A <- Alts], desugar(Def)}];
+desugar({loop, Init, Var, Expr, ContRef, BreakRef}) ->
+    [{loop, desugar(Init), Var, desugar(Expr), ContRef, BreakRef}];
 desugar(missing) -> missing;
 desugar(Code) when is_list(Code) ->
     lists:flatmap(fun desugar/1, Code);
@@ -1567,7 +1604,7 @@ bb(_Name, Code) ->
 -type bb()     :: {bbref(), bcode()}.
 -type bcode()  :: [binstr()].
 -type binstr() :: {jump, bbref()}
-                | {jumpif, bbref()}
+                | {jumpif, term(), bbref()}
                 | tuple().   %% FATE instruction
 
 -spec blocks(scode()) -> [bb()].
@@ -1581,25 +1618,29 @@ blocks([], Acc) ->
 blocks([Blk | Blocks], Acc) ->
     block(Blk, [], Blocks, Acc).
 
+fresh_block(C, Ca) ->
+    R = make_ref(),
+    {R, [#blk{ref = R, code = C, catchall = Ca}]}.
+
 -spec block(#blk{}, bcode(), [#blk{}], [bb()]) -> [bb()].
 block(#blk{ref = Ref, code = []}, CodeAcc, Blocks, BlockAcc) ->
     blocks(Blocks, [{Ref, lists:reverse(CodeAcc)} | BlockAcc]);
+block(Blk = #blk{code = [{loop, Init, _, Expr, ContRef, BreakRef} | Code], catchall = Catchall}, Acc, Blocks, BlockAcc) ->
+    LoopBlock = #blk{ref = ContRef, code = Expr, catchall = none},
+    BreakBlock = #blk{ref = BreakRef, code = Code, catchall = Catchall},
+    block(Blk#blk{code = Init}, Acc, [LoopBlock, BreakBlock | Blocks], BlockAcc);
 block(Blk = #blk{code = [switch_body | Code]}, Acc, Blocks, BlockAcc) ->
     %% Reached the body of a switch. Clear catchall ref.
     block(Blk#blk{code = Code, catchall = none}, Acc, Blocks, BlockAcc);
 block(Blk = #blk{code     = [{switch, Arg, Type, Alts, Default} | Code],
                  catchall = Catchall}, Acc, Blocks, BlockAcc) ->
-    FreshBlk = fun(C, Ca) ->
-                   R = make_ref(),
-                   {R, [#blk{ref = R, code = C, catchall = Ca}]}
-               end,
-    {RestRef, RestBlk} = FreshBlk(Code, Catchall),
+    {RestRef, RestBlk} = fresh_block(Code, Catchall),
     {DefRef, DefBlk} =
         case Default of
             missing when Catchall == none ->
-                FreshBlk([aeb_fate_ops:abort(?i(<<"Incomplete patterns">>))], none);
+                fresh_block([aeb_fate_ops:abort(?i(<<"Incomplete patterns">>))], none);
             missing -> {Catchall, []};
-            _       -> FreshBlk(Default ++ [{jump, RestRef}], Catchall)
+            _       -> fresh_block(Default ++ [{jump, RestRef}], Catchall)
                        %% ^ fall-through to the outer catchall
         end,
     %% If we don't generate a switch, we need to pop the argument if on the stack.
@@ -1611,7 +1652,7 @@ block(Blk = #blk{code     = [{switch, Arg, Type, Alts, Default} | Code],
                 {ThenRef, ThenBlk} =
                     case TrueCode of
                         missing -> {DefRef, []};
-                        _       -> FreshBlk(TrueCode ++ [{jump, RestRef}], DefRef)
+                        _       -> fresh_block(TrueCode ++ [{jump, RestRef}], DefRef)
                     end,
                 ElseCode =
                     case FalseCode of
@@ -1646,7 +1687,7 @@ block(Blk = #blk{code     = [{switch, Arg, Type, Alts, Default} | Code],
                     true  -> {Blk#blk{code = Pop ++ [{jump, DefRef}]}, [], []};
                     false ->
                         MkBlk = fun(missing) -> {DefRef, []};
-                                   (ACode)   -> FreshBlk(ACode ++ [{jump, RestRef}], DefRef)
+                                   (ACode)   -> fresh_block(ACode ++ [{jump, RestRef}], DefRef)
                                 end,
                         {AltRefs, AltBs} = lists:unzip(lists:map(MkBlk, Alts)),
                         {Blk#blk{code = []}, [{switch, Arg, AltRefs}], lists:append(AltBs)}
@@ -1662,7 +1703,7 @@ block(Blk = #blk{code = [I | Code]}, Acc, Blocks, BlockAcc) ->
 optimize_blocks(Blocks) ->
     %% We need to look at the last instruction a lot, so reverse all blocks.
     Rev       = fun(Bs) -> [ {Ref, lists:reverse(Code)} || {Ref, Code} <- Bs ] end,
-    RBlocks   = Rev(Blocks),
+    RBlocks   =  [{Ref, crop_jumps(Code)} || {Ref, Code} <- Blocks],
     RBlockMap = maps:from_list(RBlocks),
     RBlocks1  = reorder_blocks(RBlocks, []),
     RBlocks2  = [ {Ref, inline_block(RBlockMap, Ref, Code)} || {Ref, Code} <- RBlocks1 ],
@@ -1744,6 +1785,18 @@ tweak_returns(['RETURN' | Code = [{'EXIT', _} | _]])   -> Code;
 tweak_returns(['RETURN' | Code = [loop | _]])          -> Code;
 tweak_returns(Code) -> Code.
 
+%% -- Remove instructions that appear after jumps. Returns reversed code.
+%% This is useful for example when bb emitter adds continuation jumps
+%% for switch expressions, but some of the branches
+crop_jumps(Code) ->
+    crop_jumps(Code, []).
+crop_jumps([], Acc) ->
+    Acc;
+crop_jumps([I = {jump, _}|_], Acc) ->
+    [I|Acc];
+crop_jumps([I|Code], Acc) ->
+    crop_jumps(Code, [I|Acc]).
+
 %% -- Split basic blocks at CALL instructions --
 %%  Calls can only return to a new basic block. Also splits at JUMPIF instructions.
 

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

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)