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

Handle builtin types type variables separately

Browse Source
This commit is contained in:
Gaith Hallak 2022-05-20 18:24:02 +04:00
parent 136035b952
commit 7d5ea6a39e
2 changed files with 56 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

15
src/aeso_ast_infer_types.erl
View File

@ -808,9 +808,15 @@ infer(Contracts, Options) ->
create_options(Options),
ets_new(defined_contracts, [bag]),
ets_new(type_vars, [set]),
ets_new(type_vars_variance, [set]),
ets_new(type_vars_uvar, [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, {"oracle", [contravariant, covariant]}),
ets_insert(type_vars_variance, {"oracle_query", [covariant, contravariant]}),
when_warning(warn_unused_functions, fun() -> create_unused_functions() end),
check_modifiers(Env, Contracts),
create_type_errors(),
@ -2775,7 +2781,12 @@ unify1(Env, {fun_t, _, Named1, Args1, Result1}, {fun_t, _, Named2, Args2, Result
unify1(Env, {app_t, _, {Tag, _, F}, Args1}, {app_t, _, {Tag, _, F}, Args2}, Variance, When)
when length(Args1) == length(Args2), Tag == id orelse Tag == qid ->
Variances = case ets_lookup(type_vars_variance, F) of
[{_, Vs}] -> Vs;
[{_, Vs}] ->
case Variance of
contravariant -> lists:map(fun opposite_variance/1, Vs);
invariant -> invariant;
_ -> Vs
end;
_ -> Variance
end,
unify1(Env, Args1, Args2, Variances, When);

43
test/aeso_compiler_tests.erl
View File

@ -1006,6 +1006,49 @@ failing_contracts() ->
<<?Pos(47,13)
"Cannot unify `Animal` and `Cat`\n"
"when checking the type of the pattern `r17 : rec_d(Cat)` against the expected type `Main.rec_d(Animal)`">>])
, ?TYPE_ERROR(polymorphism_variance_switching_oracles,
[<<?Pos(15,13)
"Cannot unify `Cat` and `Animal`\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`\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`\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`\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`\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`\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`\n"
"when checking the type of the pattern `o15 : oracle(Cat, Cat)` against the expected type `oracle(Cat, Animal)`">>,
<<?Pos(31,13)
"Cannot unify `Cat` and `Animal`\n"
"when checking the type of the pattern `q02 : oracle_query(Animal, Animal)` against the expected type `oracle_query(Animal, Cat)`">>,
<<?Pos(33,13)
"Cannot unify `Cat` and `Animal`\n"
"when checking the type of the pattern `q04 : oracle_query(Animal, Animal)` against the expected type `oracle_query(Cat, Cat)`">>,
<<?Pos(38,13)
"Cannot unify `Animal` and `Cat`\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`\n"
"when checking the type of the pattern `q10 : oracle_query(Cat, Animal)` against the expected type `oracle_query(Animal, Cat)`">>,
<<?Pos(41,13)
"Cannot unify `Cat` and `Animal`\n"
"when checking the type of the pattern `q12 : oracle_query(Cat, Animal)` against the expected type `oracle_query(Cat, Cat)`">>,
<<?Pos(42,13)
"Cannot unify `Animal` and `Cat`\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`\n"
"when checking the type of the pattern `q14 : oracle_query(Cat, Cat)` against the expected type `oracle_query(Animal, Cat)`">>])
].
-define(Path(File), "code_errors/" ??File).