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

Add the context to unification error

Browse Source
This commit is contained in:
Gaith Hallak 2022-05-24 15:11:43 +04:00
parent 983e7165b0
commit 08d0c7034f
2 changed files with 68 additions and 58 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

24
src/aeso_ast_infer_types.erl
View File

@ -2711,7 +2711,7 @@ unify1(Env, {uvar, A, R}, T, _Variance, When) ->
true ->
if
Env#env.unify_throws ->
cannot_unify({uvar, A, R}, T, When);
cannot_unify({uvar, A, R}, T, none, When);
true ->
ok
end,
@ -2737,7 +2737,13 @@ unify1(Env, A = {con, _, NameA}, B = {con, _, NameB}, Variance, When) ->
false ->
if
Env#env.unify_throws ->
cannot_unify(A, B, When);
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,
@ -2790,7 +2796,7 @@ unify1(Env, A, {app_t, _, T, []}, Variance, When) ->
unify1(Env, A, B, _Variance, When) ->
if
Env#env.unify_throws ->
cannot_unify(A, B, When);
cannot_unify(A, B, none, When);
true ->
ok
end,
@ -3102,8 +3108,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).
@ -3172,8 +3178,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);

102
test/aeso_compiler_tests.erl
View File

@ -862,192 +862,192 @@ failing_contracts() ->
])
, ?TYPE_ERROR(polymorphism_variance_switching,
[<<?Pos(39,49)
"Cannot unify `Cat` and `Animal`\n"
"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(42,43)
"Cannot unify `Animal` and `Cat`\n"
"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(51,55)
"Cannot unify `Animal` and `Cat`\n"
"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(55, 44)
"Cannot unify `Animal` and `Cat`\n"
"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)`">>
])
, ?TYPE_ERROR(polymorphism_variance_switching_custom_types,
[<<?Pos(56,32)
"Cannot unify `Cat` and `Animal`\n"
"Cannot unify `Cat` and `Animal` in a contravariant context\n"
"when checking the type of the expression `TA(f_c_to_u) : ta(Cat)` against the expected type `ta(Animal)`">>,
<<?Pos(62,32)
"Cannot unify `Animal` and `Cat`\n"
"Cannot unify `Animal` and `Cat` in a covariant context\n"
"when checking the type of the expression `TB(f_u_to_a) : tb(Animal)` against the expected type `tb(Cat)`">>,
<<?Pos(66,32)
"Cannot unify `Animal` and `Cat`\n"
"Cannot unify `Animal` and `Cat` in a invariant context\n"
"when checking the application of\n"
" `TC : ((Animal) => Animal) => tc(Animal)`\n"
"to arguments\n"
" `f_a_to_c : (Animal) => Cat`">>,
<<?Pos(67,32)
"Cannot unify `Cat` and `Animal`\n"
"Cannot unify `Cat` and `Animal` in a invariant context\n"
"when checking the application of\n"
" `TC : ((Cat) => Cat) => tc(Cat)`\n"
"to arguments\n"
" `f_c_to_a : (Cat) => Animal`">>,
<<?Pos(68,32)
"Cannot unify `Cat` and `Animal`\n"
"Cannot unify `Cat` and `Animal` in a invariant context\n"
"when checking the type of the expression `TC(f_c_to_c) : tc(Cat)` against the expected type `tc(Animal)`">>,
<<?Pos(69,32)
"Cannot unify `Animal` and `Cat`\n"
"Cannot unify `Animal` and `Cat` in a invariant context\n"
"when checking the type of the expression `TC(f_a_to_a) : tc(Animal)` against the expected type `tc(Cat)`">>,
<<?Pos(70,32)
"Cannot unify `Animal` and `Cat`\n"
"Cannot unify `Animal` and `Cat` in a invariant context\n"
"when checking the application of\n"
" `TC : ((Animal) => Animal) => tc(Animal)`\n"
"to arguments\n"
" `f_a_to_c : (Animal) => Cat`">>,
<<?Pos(71,32)
"Cannot unify `Cat` and `Animal`\n"
"Cannot unify `Cat` and `Animal` in a invariant context\n"
"when checking the application of\n"
" `TC : ((Cat) => Cat) => tc(Cat)`\n"
"to arguments\n"
" `f_c_to_a : (Cat) => Animal`">>,
<<?Pos(78,32)
"Cannot unify `Cat` and `Animal`\n"
"Cannot unify `Cat` and `Animal` in a invariant context\n"
"when checking the type of the expression `TE1(f_c_to_u) : te(Cat)` against the expected type `te(Animal)`">>,
<<?Pos(80,32)
"Cannot unify `Cat` and `Animal`\n"
"Cannot unify `Cat` and `Animal` in a invariant context\n"
"when checking the type of the expression `TE2(f_u_to_c) : te(Cat)` against the expected type `te(Animal)`">>,
<<?Pos(81,32)
"Cannot unify `Animal` and `Cat`\n"
"Cannot unify `Animal` and `Cat` in a invariant context\n"
"when checking the type of the expression `TE1(f_a_to_u) : te(Animal)` against the expected type `te(Cat)`">>,
<<?Pos(83,32)
"Cannot unify `Animal` and `Cat`\n"
"Cannot unify `Animal` and `Cat` in a invariant context\n"
"when checking the type of the expression `TE2(f_u_to_a) : te(Animal)` against the expected type `te(Cat)`">>,
<<?Pos(88,32)
"Cannot unify `Animal` and `Cat`\n"
"Cannot unify `Animal` and `Cat` in a covariant context\n"
"when checking the type of the expression `TF(f_ta_a_to_u) : tf(Animal)` against the expected type `tf(Cat)`">>,
<<?Pos(92,32)
"Cannot unify `Cat` and `Animal`\n"
"Cannot unify `Cat` and `Animal` in a contravariant context\n"
"when checking the type of the expression `TG(f_tb_c_to_u) : tg(Cat)` against the expected type `tg(Animal)`">>,
<<?Pos(97,32)
"Cannot unify `Cat` and `Animal`\n"
"Cannot unify `Cat` and `Animal` in a contravariant context\n"
"when checking the type of the expression `TH(f_u_to_ta_c) : th(Cat)` against the expected type `th(Animal)`">>,
<<?Pos(103,32)
"Cannot unify `Animal` and `Cat`\n"
"Cannot unify `Animal` and `Cat` in a covariant context\n"
"when checking the type of the expression `TI(f_u_to_tb_a) : ti(Animal)` against the expected type `ti(Cat)`">>,
<<?Pos(107,32)
"Cannot unify `Animal` and `Cat`\n"
"Cannot unify `Animal` and `Cat` in a invariant context\n"
"when checking the application of\n"
" `TJ : ((Animal) => (unit) => Animal) => tj(Animal)`\n"
"to arguments\n"
" `f_a_to_u_to_c : (Animal) => (unit) => Cat`">>,
<<?Pos(108,32)
"Cannot unify `Cat` and `Animal`\n"
"Cannot unify `Cat` and `Animal` in a invariant context\n"
"when checking the application of\n"
" `TJ : ((Cat) => (unit) => Cat) => tj(Cat)`\n"
"to arguments\n"
" `f_c_to_u_to_a : (Cat) => (unit) => Animal`">>,
<<?Pos(110,32)
"Cannot unify `Animal` and `Cat`\n"
"Cannot unify `Animal` and `Cat` in a covariant context\n"
"when checking the type of the expression `TJ(f_a_to_u_to_a) : tj(Animal)` against the expected type `tj(Cat)`">>,
<<?Pos(111,32)
"Cannot unify `Animal` and `Cat`\n"
"Cannot unify `Animal` and `Cat` in a invariant context\n"
"when checking the application of\n"
" `TJ : ((Animal) => (unit) => Animal) => tj(Animal)`\n"
"to arguments\n"
" `f_a_to_u_to_c : (Animal) => (unit) => Cat`">>,
<<?Pos(112,32)
"Cannot unify `Cat` and `Animal`\n"
"Cannot unify `Cat` and `Animal` in a invariant context\n"
"when checking the application of\n"
" `TJ : ((Cat) => (unit) => Cat) => tj(Cat)`\n"
"to arguments\n"
" `f_c_to_u_to_a : (Cat) => (unit) => Animal`">>,
<<?Pos(116,41)
"Cannot unify `Cat` and `Animal`\n"
"Cannot unify `Cat` and `Animal` in a contravariant context\n"
"when checking the type of the expression `TK(f_a_to_c_to_u) : tk(Animal, Cat)` against the expected type `tk(Animal, Animal)`">>,
<<?Pos(118,41)
"Cannot unify `Cat` and `Animal`\n"
"Cannot unify `Cat` and `Animal` in a contravariant context\n"
"when checking the type of the expression `TK(f_c_to_c_to_u) : tk(Cat, Cat)` against the expected type `tk(Animal, Animal)`">>,
<<?Pos(123,41)
"Cannot unify `Animal` and `Cat`\n"
"Cannot unify `Animal` and `Cat` in a covariant context\n"
"when checking the type of the expression `TK(f_a_to_a_to_u) : tk(Animal, Animal)` against the expected type `tk(Cat, Animal)`">>,
<<?Pos(124,41)
"Cannot unify `Animal` and `Cat`\n"
"Cannot unify `Animal` and `Cat` in a covariant context\n"
"when checking the type of the expression `TK(f_a_to_c_to_u) : tk(Animal, Cat)` against the expected type `tk(Cat, Animal)`">>,
<<?Pos(126,41)
"Cannot unify `Cat` and `Animal`\n"
"Cannot unify `Cat` and `Animal` in a contravariant context\n"
"when checking the type of the expression `TK(f_c_to_c_to_u) : tk(Cat, Cat)` against the expected type `tk(Cat, Animal)`">>,
<<?Pos(127,41)
"Cannot unify `Animal` and `Cat`\n"
"Cannot unify `Animal` and `Cat` in a covariant context\n"
"when checking the type of the expression `TK(f_a_to_a_to_u) : tk(Animal, Animal)` against the expected type `tk(Cat, Cat)`">>,
<<?Pos(128,41)
"Cannot unify `Animal` and `Cat`\n"
"Cannot unify `Animal` and `Cat` in a covariant context\n"
"when checking the type of the expression `TK(f_a_to_c_to_u) : tk(Animal, Cat)` against the expected type `tk(Cat, Cat)`">>
])
, ?TYPE_ERROR(polymorphism_variance_switching_records,
[<<?Pos(26,13)
"Cannot unify `Animal` and `Cat`\n"
"Cannot unify `Animal` and `Cat` in a covariant context\n"
"when checking the type of the pattern `r03 : rec_a(Cat)` against the expected type `Main.rec_a(Animal)`">>,
<<?Pos(32,13)
"Cannot unify `Cat` and `Animal`\n"
"Cannot unify `Cat` and `Animal` in a contravariant context\n"
"when checking the type of the pattern `r06 : rec_b(Animal)` against the expected type `Main.rec_b(Cat)`">>,
<<?Pos(40,13)
"Cannot unify `Animal` and `Cat`\n"
"Cannot unify `Animal` and `Cat` in a covariant context\n"
"when checking the type of the pattern `r11 : rec_c(Cat)` against the expected type `Main.rec_c(Animal)`">>,
<<?Pos(46,13)
"Cannot unify `Cat` and `Animal`\n"
"Cannot unify `Cat` and `Animal` in a invariant context\n"
"when checking the type of the pattern `r16 : rec_d(Animal)` against the expected type `Main.rec_d(Cat)`">>,
<<?Pos(47,13)
"Cannot unify `Animal` and `Cat`\n"
"Cannot unify `Animal` and `Cat` in a invariant context\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"
"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`\n"
"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`\n"
"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`\n"
"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`\n"
"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`\n"
"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`\n"
"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(31,13)
"Cannot unify `Cat` and `Animal`\n"
"Cannot unify `Cat` and `Animal` in a contravariant context\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"
"Cannot unify `Cat` and `Animal` in a contravariant context\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"
"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`\n"
"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(41,13)
"Cannot unify `Cat` and `Animal`\n"
"Cannot unify `Cat` and `Animal` in a contravariant context\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"
"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`\n"
"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)`">>])
].