QPQ-AG/sophia
10
0
Fork 0
Code Issues 41 Pull Requests 5 Actions Packages Projects Releases 16 Wiki Activity

Fix variance inference

Browse Source
This commit is contained in:
Gaith Hallak 2022-05-27 15:45:26 +04:00
parent 24178f15d0
commit 113d699b01
3 changed files with 112 additions and 150 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

68
src/aeso_ast_infer_types.erl
View File

@ -809,7 +809,6 @@ infer(Contracts, Options) ->
create_options(Options), create_options(Options),
ets_new(defined_contracts, [bag]), ets_new(defined_contracts, [bag]),
ets_new(type_vars, [set]), ets_new(type_vars, [set]),
ets_new(type_vars_uvar, [set]),
ets_new(warnings, [bag]), ets_new(warnings, [bag]),
ets_new(type_vars_variance, [set]), ets_new(type_vars_variance, [set]),
%% Set the variance for builtin types %% Set the variance for builtin types
@ -1126,7 +1125,7 @@ infer_type_vars_variance(TypeParams, Cons) ->
% args from all type constructors % args from all type constructors
FlatArgs = lists:flatten([Args || {constr_t, _, _, Args} <- Cons]) ++ [Type || {field_t, _, _, Type} <- Cons], FlatArgs = lists:flatten([Args || {constr_t, _, _, Args} <- Cons]) ++ [Type || {field_t, _, _, Type} <- Cons],
Vs = lists:flatten([element(1, infer_type_vars_variance(Arg)) || Arg <- FlatArgs]), Vs = lists:flatten([infer_type_vars_variance(Arg) || Arg <- FlatArgs]),
lists:map(fun({tvar, _, TVar}) -> lists:map(fun({tvar, _, TVar}) ->
S = sets:from_list([Variance || {TV, Variance} <- Vs, TV == TVar]), S = sets:from_list([Variance || {TV, Variance} <- Vs, TV == TVar]),
IsCovariant = sets:is_element(covariant, S), IsCovariant = sets:is_element(covariant, S),
@ -1139,7 +1138,10 @@ infer_type_vars_variance(TypeParams, Cons) ->
end end
end, TypeParams). end, TypeParams).
-spec infer_type_vars_variance(utype()) -> {[{name(), variance()}], integer()}. -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}) -> infer_type_vars_variance({app_t, _, Type, Args}) ->
Variances = case ets_lookup(type_vars_variance, qname(Type)) of Variances = case ets_lookup(type_vars_variance, qname(Type)) of
[{_, Vs}] -> Vs; [{_, Vs}] -> Vs;
@ -1147,36 +1149,14 @@ infer_type_vars_variance({app_t, _, Type, Args}) ->
end, end,
TypeVarsVariance = [{TVar, Variance} TypeVarsVariance = [{TVar, Variance}
|| {{tvar, _, TVar}, Variance} <- lists:zip(Args, Variances)], || {{tvar, _, TVar}, Variance} <- lists:zip(Args, Variances)],
{TypeVarsVariance, 0}; TypeVarsVariance;
infer_type_vars_variance({fun_t, _, [], [{app_t, _, Type, Args}], Res}) -> infer_type_vars_variance({tvar, _, TVar}) -> [{TVar, covariant}];
Variances = case ets_lookup(type_vars_variance, qname(Type)) of infer_type_vars_variance({fun_t, _, [], Args, Res}) ->
[{_, Vs}] -> Vs; ArgsVariance = infer_type_vars_variance(Args),
_ -> lists:duplicate(length(Args), covariant) ResVariance = infer_type_vars_variance(Res),
end, FlippedArgsVariance = lists:map(fun({TVar, Variance}) -> {TVar, opposite_variance(Variance)} end, ArgsVariance),
TypeVarsVariance = [{TVar, Variance} FlippedArgsVariance ++ ResVariance;
|| {{tvar, _, TVar}, Variance} <- lists:zip(Args, Variances)], infer_type_vars_variance(_) -> [].
FlipVariance = fun({TVar, covariant}) -> {TVar, contravariant};
({TVar, contravariant}) -> {TVar, covariant}
end,
{TVVs, Depth} = infer_type_vars_variance(Res),
Cur = case (Depth + 1) rem 2 of
0 -> TypeVarsVariance;
1 -> lists:map(FlipVariance, TypeVarsVariance)
end,
{Cur ++ TVVs, Depth + 1};
infer_type_vars_variance({fun_t, _, [], [{tvar, _, TVar}], Res}) ->
{TVVs, Depth} = infer_type_vars_variance(Res),
Cur = case (Depth + 1) rem 2 of
0 -> {TVar, covariant};
1 -> {TVar, contravariant}
end,
{[Cur | TVVs], Depth + 1};
infer_type_vars_variance({fun_t, _, [], _, Res}) ->
{X, Depth} = infer_type_vars_variance(Res),
{X, Depth + 1};
infer_type_vars_variance({tvar, _, TVar}) ->
{[{TVar, covariant}], 0};
infer_type_vars_variance(_) -> {[], 0}.
opposite_variance(invariant) -> invariant; opposite_variance(invariant) -> invariant;
opposite_variance(covariant) -> contravariant; opposite_variance(covariant) -> contravariant;
@ -1773,16 +1753,6 @@ infer_expr(Env, {app, Ann, Fun, Args0} = App) ->
ResultType = fresh_uvar(Ann), ResultType = fresh_uvar(Ann),
when_warning(warn_unused_functions, when_warning(warn_unused_functions,
fun() -> register_function_call(Namespace ++ qname(CurrentFun), Name) end), fun() -> register_function_call(Namespace ++ qname(CurrentFun), Name) end),
% the uvars of tvars are stored so that no variance switching happens
% in between them (e.g. in TC('a => 'a), 'a should be a single type)
case FunType of
{fun_t, _, _, _, {app_t, _, _, TArgs}} ->
lists:foreach(fun({uvar, _, URef}) ->
ets_insert(type_vars_uvar, {URef});
(_) -> ok
end, TArgs);
_ -> ok
end,
unify(Env, FunType, {fun_t, [], NamedArgsVar, ArgTypes, GeneralResultType}, When), unify(Env, FunType, {fun_t, [], NamedArgsVar, ArgTypes, GeneralResultType}, When),
when_warning(warn_negative_spend, fun() -> warn_potential_negative_spend(Ann, NewFun1, NewArgs) end), when_warning(warn_negative_spend, fun() -> warn_potential_negative_spend(Ann, NewFun1, NewArgs) end),
add_constraint( add_constraint(
@ -2143,7 +2113,7 @@ next_count() ->
ets_tables() -> ets_tables() ->
[options, type_vars, constraints, freshen_tvars, type_errors, [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, type_vars_uvar]. type_vars_variance].
clean_up_ets() -> clean_up_ets() ->
[ catch ets_delete(Tab) || Tab <- ets_tables() ], [ catch ets_delete(Tab) || Tab <- ets_tables() ],
@ -2687,7 +2657,7 @@ unify(Env, A, B, When) -> unify0(Env, A, B, covariant, When).
unify0(_, {id, _, "_"}, _, _Variance, _When) -> true; unify0(_, {id, _, "_"}, _, _Variance, _When) -> true;
unify0(_, _, {id, _, "_"}, _Variance, _When) -> true; unify0(_, _, {id, _, "_"}, _Variance, _When) -> true;
unify0(Env, A, B, Variance0, When) -> unify0(Env, A, B, Variance, When) ->
Options = Options =
case When of %% Improve source location for map_in_map_key errors case When of %% Improve source location for map_in_map_key errors
{check_expr, E, _, _} -> [{ann, aeso_syntax:get_ann(E)}]; {check_expr, E, _, _} -> [{ann, aeso_syntax:get_ann(E)}];
@ -2695,14 +2665,6 @@ unify0(Env, A, B, Variance0, When) ->
end, end,
A1 = dereference(unfold_types_in_type(Env, A, Options)), A1 = dereference(unfold_types_in_type(Env, A, Options)),
B1 = dereference(unfold_types_in_type(Env, B, Options)), B1 = dereference(unfold_types_in_type(Env, B, Options)),
Variance = case A of
{uvar, _,URef} ->
case ets_lookup(type_vars_uvar, URef) of
[_] -> invariant;
_ -> Variance0
end;
_ -> Variance0
end,
unify1(Env, A1, B1, Variance, When). unify1(Env, A1, B1, Variance, When).
unify1(_Env, {uvar, _, R}, {uvar, _, R}, _Variance, _When) -> unify1(_Env, {uvar, _, R}, {uvar, _, R}, _Variance, _When) ->

131
test/aeso_compiler_tests.erl
View File

@ -884,114 +884,105 @@ failing_contracts() ->
"when checking the type of the expression `some_animal : Animal` against the expected type `Cat`">> "when checking the type of the expression `some_animal : Animal` against the expected type `Cat`">>
]) ])
, ?TYPE_ERROR(polymorphism_variance_switching_custom_types, , ?TYPE_ERROR(polymorphism_variance_switching_custom_types,
[<<?Pos(56,39) [<<?Pos(57,39)
"Cannot unify `Cat` and `Animal` in a contravariant context\n" "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)`">>, "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) <<?Pos(63,35)
"Cannot unify `Animal` and `Cat` in a covariant context\n" "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)`">>, "when checking the type of the expression `DT_CO(f_u_to_a) : dt_co(Animal)` against the expected type `dt_co(Cat)`">>,
<<?Pos(66,36)
"Cannot unify `Animal` and `Cat` in a invariant context\n"
"when checking the application of\n"
" `DT_INV : ((Animal) => Animal) => dt_inv(Animal)`\n"
"to arguments\n"
" `f_a_to_c : (Animal) => Cat`">>,
<<?Pos(67,36)
"Cannot unify `Cat` and `Animal` in a invariant context\n"
"when checking the application of\n"
" `DT_INV : ((Cat) => Cat) => dt_inv(Cat)`\n"
"to arguments\n"
" `f_c_to_a : (Cat) => Animal`">>,
<<?Pos(68,36) <<?Pos(68,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(69,36)
"Cannot unify `Cat` and `Animal` in a invariant context\n" "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)`">>, "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) <<?Pos(70,36)
"Cannot unify `Animal` and `Cat` in a invariant context\n" "Cannot unify `Animal` and `Cat` in a invariant context\n"
"when checking the application of\n" "when checking the type of the expression `DT_INV(f_a_to_a) : dt_inv(Animal)` against the expected type `dt_inv(Cat)`">>,
" `DT_INV : ((Animal) => Animal) => dt_inv(Animal)`\n"
"to arguments\n"
" `f_a_to_c : (Animal) => Cat`">>,
<<?Pos(71,36) <<?Pos(71,36)
"Cannot unify `Cat` and `Animal` in a invariant context\n" "Cannot unify `Animal` and `Cat` in a invariant context\n"
"when checking the application of\n" "when checking the type of the expression `DT_INV(f_a_to_c) : dt_inv(Animal)` against the expected type `dt_inv(Cat)`">>,
" `DT_INV : ((Cat) => Cat) => dt_inv(Cat)`\n" <<?Pos(72,36)
"to arguments\n" "Cannot unify `Cat` and `Animal` in a contravariant context\n"
" `f_c_to_a : (Cat) => Animal`">>, "when checking the application of\n `DT_INV : ((Cat) => Cat) => dt_inv(Cat)`\nto arguments\n `f_c_to_a : (Cat) => Animal`">>,
<<?Pos(78,40) <<?Pos(79,40)
"Cannot unify `Cat` and `Animal` in a invariant context\n" "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)`">>, "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(80,40) <<?Pos(81,40)
"Cannot unify `Cat` and `Animal` in a invariant context\n" "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)`">>, "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(81,40) <<?Pos(82,40)
"Cannot unify `Animal` and `Cat` in a invariant context\n" "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)`">>, "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(83,40) <<?Pos(84,40)
"Cannot unify `Animal` and `Cat` in a invariant context\n" "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)`">>, "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(88,42) <<?Pos(89,42)
"Cannot unify `Animal` and `Cat` in a covariant context\n" "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)`">>, "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(92,46) <<?Pos(93,46)
"Cannot unify `Cat` and `Animal` in a contravariant context\n" "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)`">>, "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(97,46) <<?Pos(98,46)
"Cannot unify `Cat` and `Animal` in a contravariant context\n" "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)`">>, "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(103,42) <<?Pos(104,42)
"Cannot unify `Animal` and `Cat` in a covariant context\n" "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)`">>, "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(107,41) <<?Pos(109,41)
"Cannot unify `Animal` and `Cat` in a invariant context\n" "Cannot unify `Cat` and `Animal` in a contravariant context\n"
"when checking the application of\n" "when checking the application of\n"
" `DT_CO_TWICE : ((Animal) => (unit) => Animal) => dt_co_twice(Animal)`\n" " `DT_CO_TWICE : (((Cat) => unit) => Cat) => dt_co_twice(Cat)`\n"
"to arguments\n" "to arguments\n"
" `f_a_to_u_to_c : (Animal) => (unit) => Cat`">>, " `f_c_to_u_to_a : ((Cat) => unit) => Animal`">>,
<<?Pos(108,41) <<?Pos(111,41)
"Cannot unify `Cat` and `Animal` in a invariant context\n"
"when checking the application of\n"
" `DT_CO_TWICE : ((Cat) => (unit) => Cat) => dt_co_twice(Cat)`\n"
"to arguments\n"
" `f_c_to_u_to_a : (Cat) => (unit) => Animal`">>,
<<?Pos(110,41)
"Cannot unify `Animal` and `Cat` in a covariant context\n" "Cannot unify `Animal` and `Cat` in a covariant context\n"
"when checking the type of the expression `DT_CO_TWICE(f_a_to_u_to_a) : dt_co_twice(Animal)` against the expected type `dt_co_twice(Cat)`">>, "when checking the type of the expression `DT_CO_TWICE(f_a_to_u_to_a) : dt_co_twice(Animal)` against the expected type `dt_co_twice(Cat)`">>,
<<?Pos(111,41)
"Cannot unify `Animal` and `Cat` in a invariant context\n"
"when checking the application of\n"
" `DT_CO_TWICE : ((Animal) => (unit) => Animal) => dt_co_twice(Animal)`\n"
"to arguments\n"
" `f_a_to_u_to_c : (Animal) => (unit) => Cat`">>,
<<?Pos(112,41) <<?Pos(112,41)
"Cannot unify `Cat` and `Animal` in a invariant context\n" "Cannot unify `Animal` and `Cat` in a covariant context\n"
"when checking the type of the expression `DT_CO_TWICE(f_a_to_u_to_c) : dt_co_twice(Animal)` against the expected type `dt_co_twice(Cat)`">>,
<<?Pos(113,41)
"Cannot unify `Cat` and `Animal` in a contravariant context\n"
"when checking the application of\n" "when checking the application of\n"
" `DT_CO_TWICE : ((Cat) => (unit) => Cat) => dt_co_twice(Cat)`\n" " `DT_CO_TWICE : (((Cat) => unit) => Cat) => dt_co_twice(Cat)`\n"
"to arguments\n" "to arguments\n"
" `f_c_to_u_to_a : (Cat) => (unit) => Animal`">>, " `f_c_to_u_to_a : ((Cat) => unit) => Animal`">>,
<<?Pos(116,55) <<?Pos(116,59)
"Cannot unify `Cat` and `Animal` in a contravariant context\n" "Cannot unify `Cat` and `Animal` in a contravariant context\n"
"when checking the type of the expression `DT_A_CO_B_CONTRA(f_a_to_c_to_u) : dt_a_co_b_contra(Animal, Cat)` against the expected type `dt_a_co_b_contra(Animal, Animal)`">>, "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(118,55) <<?Pos(117,59)
"Cannot unify `Cat` and `Animal` in a contravariant context\n" "Cannot unify `Cat` and `Animal` in a contravariant context\n"
"when checking the type of the expression `DT_A_CO_B_CONTRA(f_c_to_c_to_u) : dt_a_co_b_contra(Cat, Cat)` against the expected type `dt_a_co_b_contra(Animal, Animal)`">>, "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(123,55) <<?Pos(118,59)
"Cannot unify `Animal` and `Cat` in a covariant context\n"
"when checking the type of the expression `DT_A_CO_B_CONTRA(f_a_to_a_to_u) : dt_a_co_b_contra(Animal, Animal)` against the expected type `dt_a_co_b_contra(Cat, Animal)`">>,
<<?Pos(124,55)
"Cannot unify `Animal` and `Cat` in a covariant context\n"
"when checking the type of the expression `DT_A_CO_B_CONTRA(f_a_to_c_to_u) : dt_a_co_b_contra(Animal, Cat)` against the expected type `dt_a_co_b_contra(Cat, Animal)`">>,
<<?Pos(126,55)
"Cannot unify `Cat` and `Animal` in a contravariant context\n" "Cannot unify `Cat` and `Animal` in a contravariant context\n"
"when checking the type of the expression `DT_A_CO_B_CONTRA(f_c_to_c_to_u) : dt_a_co_b_contra(Cat, Cat)` against the expected type `dt_a_co_b_contra(Cat, Animal)`">>, "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(127,55) <<?Pos(121,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(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_c_to_c_to_u) : dt_a_contra_b_contra(Cat, Cat)` against the expected type `dt_a_contra_b_contra(Animal, Cat)`">>,
<<?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_a_to_c_to_u) : dt_a_contra_b_contra(Animal, Cat)` against the expected type `dt_a_contra_b_contra(Cat, Animal)`">>,
<<?Pos(126,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(133,45)
"Cannot unify `Animal` and `Cat` in a covariant context\n" "Cannot unify `Animal` and `Cat` in a covariant context\n"
"when checking the type of the expression `DT_A_CO_B_CONTRA(f_a_to_a_to_u) : dt_a_co_b_contra(Animal, Animal)` against the expected type `dt_a_co_b_contra(Cat, Cat)`">>, "when checking the application of\n `DT_CONTRA_TWICE : ((Animal) => (Animal) => unit) => dt_contra_twice(Animal)`\nto arguments\n `f_a_to_c_to_u : (Animal) => (Cat) => unit`">>,
<<?Pos(128,55) <<?Pos(134,45)
"Cannot unify `Cat` and `Animal` in a contravariant context\n"
"when checking the type of the expression `DT_CONTRA_TWICE(f_c_to_a_to_u) : dt_contra_twice(Cat)` against the expected type `dt_contra_twice(Animal)`">>,
<<?Pos(135,45)
"Cannot unify `Cat` and `Animal` in a contravariant context\n"
"when checking the type of the expression `DT_CONTRA_TWICE(f_c_to_c_to_u) : dt_contra_twice(Cat)` against the expected type `dt_contra_twice(Animal)`">>,
<<?Pos(137,45)
"Cannot unify `Animal` and `Cat` in a covariant context\n" "Cannot unify `Animal` and `Cat` in a covariant context\n"
"when checking the type of the expression `DT_A_CO_B_CONTRA(f_a_to_c_to_u) : dt_a_co_b_contra(Animal, Cat)` against the expected type `dt_a_co_b_contra(Cat, Cat)`">> "when checking the application of\n"
" `DT_CONTRA_TWICE : ((Animal) => (Animal) => unit) => dt_contra_twice(Animal)`\n"
"to arguments\n"
" `f_a_to_c_to_u : (Animal) => (Cat) => unit`">>
]) ])
, ?TYPE_ERROR(polymorphism_variance_switching_records, , ?TYPE_ERROR(polymorphism_variance_switching_records,
[<<?Pos(27,13) [<<?Pos(27,13)

63
test/contracts/polymorphism_variance_switching_custom_types.aes
View File

@ -14,8 +14,9 @@ main contract Main =
datatype dt_contra_nest_a('a) = DT_CONTRA_NEST_A(dt_co('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_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_nest_b('a) = DT_CO_NEST_B(unit => dt_co('a))
datatype dt_co_twice('a) = DT_CO_TWICE('a => unit => 'a) datatype dt_co_twice('a) = DT_CO_TWICE(('a => unit) => 'a)
datatype dt_a_co_b_contra('a, 'b) = DT_A_CO_B_CONTRA('a => 'b => unit) 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_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_a_to_c_to_u(_ : Animal) : (Cat => unit) = f_c_to_u
@ -43,10 +44,10 @@ main contract Main =
stateful function f_c_to_a(_ : Cat) : Animal = f_a() stateful function f_c_to_a(_ : Cat) : Animal = f_a()
stateful function f_c_to_c(_ : Cat) : Cat = f_c() stateful function f_c_to_c(_ : Cat) : Cat = f_c()
stateful function f_a_to_u_to_a(_ : Animal) : (unit => Animal) = f_u_to_a stateful function f_a_to_u_to_a(_ : (Animal => unit)) : Animal = f_a()
stateful function f_a_to_u_to_c(_ : Animal) : (unit => Cat) = f_u_to_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_u_to_a 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_u_to_c 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_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 function f_u_to_dt_co_c(_ : unit) : dt_co(Cat) = DT_CO(f_u_to_c)
@ -63,7 +64,7 @@ main contract Main =
let vb4 : dt_co(Cat) = DT_CO(f_u_to_c) // success 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 vc1 : dt_inv(Animal) = DT_INV(f_a_to_a) // success
let vc2 : dt_inv(Animal) = DT_INV(f_a_to_c) // fail 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 vc3 : dt_inv(Animal) = DT_INV(f_c_to_a) // fail
let vc4 : dt_inv(Animal) = DT_INV(f_c_to_c) // 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 vc5 : dt_inv(Cat) = DT_INV(f_a_to_a) // fail
@ -71,8 +72,8 @@ main contract Main =
let vc7 : dt_inv(Cat) = DT_INV(f_c_to_a) // 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 vc8 : dt_inv(Cat) = DT_INV(f_c_to_c) // success
let vd1 : dt_biv(Animal) = DT_BIV(f_u_to_u) // success let vd1 : dt_biv(Animal) = DT_BIV(f_u_to_u) : dt_biv(Cat) // success
let vd2 : dt_biv(Cat) = DT_BIV(f_u_to_u) // success let vd2 : dt_biv(Cat) = DT_BIV(f_u_to_u) : dt_biv(Animal) // success
let ve1 : dt_inv_sep(Animal) = DT_INV_SEP_A(f_a_to_u) // 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 ve2 : dt_inv_sep(Animal) = DT_INV_SEP_A(f_c_to_u) // fail
@ -104,29 +105,37 @@ main contract Main =
let vi4 : dt_co_nest_b(Cat) = DT_CO_NEST_B(f_u_to_dt_co_c) // success 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_a) // success let vj1 : dt_co_twice(Animal) = DT_CO_TWICE(f_a_to_u_to_a) // success
let vj2 : dt_co_twice(Animal) = DT_CO_TWICE(f_a_to_u_to_c) // fail let vj2 : dt_co_twice(Animal) = DT_CO_TWICE(f_a_to_u_to_c) // success
let vj3 : dt_co_twice(Animal) = DT_CO_TWICE(f_c_to_u_to_a) // fail let vj3 : dt_co_twice(Animal) = DT_CO_TWICE(f_c_to_u_to_a) // fail
let vj4 : dt_co_twice(Animal) = DT_CO_TWICE(f_c_to_u_to_c) // success let vj4 : dt_co_twice(Animal) = DT_CO_TWICE(f_c_to_u_to_c) // success
let vj5 : dt_co_twice(Cat) = DT_CO_TWICE(f_a_to_u_to_a) // fail let vj5 : dt_co_twice(Cat) = DT_CO_TWICE(f_a_to_u_to_a) // fail
let vj6 : dt_co_twice(Cat) = DT_CO_TWICE(f_a_to_u_to_c) // fail let vj6 : dt_co_twice(Cat) = DT_CO_TWICE(f_a_to_u_to_c) // fail
let vj7 : dt_co_twice(Cat) = DT_CO_TWICE(f_c_to_u_to_a) // fail let vj7 : dt_co_twice(Cat) = DT_CO_TWICE(f_c_to_u_to_a) // fail
let vj8 : dt_co_twice(Cat) = DT_CO_TWICE(f_c_to_u_to_c) // success
let vk01 : dt_a_co_b_contra(Animal, Animal) = DT_A_CO_B_CONTRA(f_a_to_a_to_u) // 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_co_b_contra(Animal, Animal) = DT_A_CO_B_CONTRA(f_a_to_c_to_u) // fail 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_co_b_contra(Animal, Animal) = DT_A_CO_B_CONTRA(f_c_to_a_to_u) // success 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_co_b_contra(Animal, Animal) = DT_A_CO_B_CONTRA(f_c_to_c_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_co_b_contra(Animal, Cat) = DT_A_CO_B_CONTRA(f_a_to_a_to_u) // success 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_co_b_contra(Animal, Cat) = DT_A_CO_B_CONTRA(f_a_to_c_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_co_b_contra(Animal, Cat) = DT_A_CO_B_CONTRA(f_c_to_a_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_co_b_contra(Animal, Cat) = DT_A_CO_B_CONTRA(f_c_to_c_to_u) // success 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_co_b_contra(Cat, Animal) = DT_A_CO_B_CONTRA(f_a_to_a_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_co_b_contra(Cat, Animal) = DT_A_CO_B_CONTRA(f_a_to_c_to_u) // fail 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_co_b_contra(Cat, Animal) = DT_A_CO_B_CONTRA(f_c_to_a_to_u) // success 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_co_b_contra(Cat, Animal) = DT_A_CO_B_CONTRA(f_c_to_c_to_u) // fail 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_co_b_contra(Cat, Cat) = DT_A_CO_B_CONTRA(f_a_to_a_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_co_b_contra(Cat, Cat) = DT_A_CO_B_CONTRA(f_a_to_c_to_u) // fail 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_co_b_contra(Cat, Cat) = DT_A_CO_B_CONTRA(f_c_to_a_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_co_b_contra(Cat, Cat) = DT_A_CO_B_CONTRA(f_c_to_c_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) // success
let vl2 : dt_contra_twice(Animal) = DT_CONTRA_TWICE(f_a_to_c_to_u) // fail
let vl3 : dt_contra_twice(Animal) = DT_CONTRA_TWICE(f_c_to_a_to_u) // fail
let vl4 : dt_contra_twice(Animal) = DT_CONTRA_TWICE(f_c_to_c_to_u) // fail
let vl5 : dt_contra_twice(Cat) = DT_CONTRA_TWICE(f_a_to_a_to_u) // success
let vl6 : dt_contra_twice(Cat) = DT_CONTRA_TWICE(f_a_to_c_to_u) // fail
let vl7 : dt_contra_twice(Cat) = DT_CONTRA_TWICE(f_c_to_a_to_u) // success
let vl8 : dt_contra_twice(Cat) = DT_CONTRA_TWICE(f_c_to_c_to_u) // success
() ()