Add testing for custom types variance switching
This commit is contained in:
parent
dd259fbc96
commit
918346445f
@ -809,6 +809,7 @@ infer(Contracts, 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_variance, [set]),
|
ets_new(type_vars_variance, [set]),
|
||||||
|
ets_new(uvars_variance, [set]),
|
||||||
ets_new(warnings, [bag]),
|
ets_new(warnings, [bag]),
|
||||||
when_warning(warn_unused_functions, fun() -> create_unused_functions() end),
|
when_warning(warn_unused_functions, fun() -> create_unused_functions() end),
|
||||||
check_modifiers(Env, Contracts),
|
check_modifiers(Env, Contracts),
|
||||||
@ -1155,6 +1156,14 @@ infer_type_vars_variance(TypeParams, Cons) ->
|
|||||||
end, TypeParams).
|
end, TypeParams).
|
||||||
|
|
||||||
-spec infer_type_vars_variance(utype()) -> [{name(), variance()}].
|
-spec infer_type_vars_variance(utype()) -> [{name(), variance()}].
|
||||||
|
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(FT = {fun_t, _, [], [{app_t, _, Type, Args}], Res}) ->
|
infer_type_vars_variance(FT = {fun_t, _, [], [{app_t, _, Type, Args}], Res}) ->
|
||||||
Variances = case ets_lookup(type_vars_variance, qname(Type)) of
|
Variances = case ets_lookup(type_vars_variance, qname(Type)) of
|
||||||
[{_, Vs}] -> Vs;
|
[{_, Vs}] -> Vs;
|
||||||
@ -1777,6 +1786,17 @@ 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),
|
||||||
|
case FunType of
|
||||||
|
{fun_t, _, _, _, {app_t, _, QType, TArgs}} ->
|
||||||
|
case ets_lookup(type_vars_variance, qname(QType)) of
|
||||||
|
[{_, Vs}] ->
|
||||||
|
lists:foreach(fun({{uvar, _, URef}, Variance}) ->
|
||||||
|
ets_insert(uvars_variance, {URef, invariant})
|
||||||
|
end, lists:zip(TArgs, Vs));
|
||||||
|
_ -> ok
|
||||||
|
end;
|
||||||
|
_ -> 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(
|
||||||
@ -2681,7 +2701,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, Variance, When) ->
|
unify0(Env, A, B, Variance0, 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)}];
|
||||||
@ -2689,6 +2709,14 @@ unify0(Env, A, B, Variance, 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(uvars_variance, URef) of
|
||||||
|
[{_, V}] -> V;
|
||||||
|
_ -> 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) ->
|
||||||
|
@ -885,6 +885,116 @@ failing_contracts() ->
|
|||||||
"to arguments\n"
|
"to arguments\n"
|
||||||
" `x : (Cat) => Cat`">>
|
" `x : (Cat) => Cat`">>
|
||||||
])
|
])
|
||||||
|
, ?TYPE_ERROR(polymorphism_variance_switching_custom_types,
|
||||||
|
[<<?Pos(56,32)
|
||||||
|
"Cannot unify `Cat` and `Animal`\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"
|
||||||
|
"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"
|
||||||
|
"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"
|
||||||
|
"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"
|
||||||
|
"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"
|
||||||
|
"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"
|
||||||
|
"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"
|
||||||
|
"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"
|
||||||
|
"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"
|
||||||
|
"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"
|
||||||
|
"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"
|
||||||
|
"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"
|
||||||
|
"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"
|
||||||
|
"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"
|
||||||
|
"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"
|
||||||
|
"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"
|
||||||
|
"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"
|
||||||
|
"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"
|
||||||
|
"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"
|
||||||
|
"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"
|
||||||
|
"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"
|
||||||
|
"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"
|
||||||
|
"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"
|
||||||
|
"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"
|
||||||
|
"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"
|
||||||
|
"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"
|
||||||
|
"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"
|
||||||
|
"when checking the type of the expression `TK(f_a_to_c_to_u) : tk(Animal, Cat)` against the expected type `tk(Cat, Cat)`">>
|
||||||
|
])
|
||||||
].
|
].
|
||||||
|
|
||||||
-define(Path(File), "code_errors/" ??File).
|
-define(Path(File), "code_errors/" ??File).
|
||||||
|
132
test/contracts/polymorphism_variance_switching_custom_types.aes
Normal file
132
test/contracts/polymorphism_variance_switching_custom_types.aes
Normal file
@ -0,0 +1,132 @@
|
|||||||
|
contract interface Animal =
|
||||||
|
entrypoint sound : () => string
|
||||||
|
|
||||||
|
contract Cat : Animal =
|
||||||
|
entrypoint sound() = "meow"
|
||||||
|
|
||||||
|
main contract Main =
|
||||||
|
datatype ta('a) = TA('a => unit)
|
||||||
|
datatype tb('a) = TB(unit => 'a)
|
||||||
|
datatype tc('a) = TC('a => 'a)
|
||||||
|
datatype td('a) = TD(unit => unit)
|
||||||
|
datatype te('a) = TE1('a => unit) | TE2(unit => 'a)
|
||||||
|
datatype tf('a) = TF(ta('a) => unit)
|
||||||
|
datatype tg('a) = TG(tb('a) => unit)
|
||||||
|
datatype th('a) = TH(unit => ta('a))
|
||||||
|
datatype ti('a) = TI(unit => tb('a))
|
||||||
|
datatype tj('a) = TJ('a => unit => 'a)
|
||||||
|
datatype tk('a, 'b) = TK('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_ta_a_to_u(_ : ta(Animal)) : unit = ()
|
||||||
|
function f_ta_c_to_u(_ : ta(Cat)) : unit = ()
|
||||||
|
function f_tb_a_to_u(_ : tb(Animal)) : unit = ()
|
||||||
|
function f_tb_c_to_u(_ : tb(Cat)) : unit = ()
|
||||||
|
function f_u_to_ta_a(_ : unit) : ta(Animal) = TA(f_a_to_u)
|
||||||
|
function f_u_to_ta_c(_ : unit) : ta(Cat) = TA(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_a(_ : Animal) : (unit => Animal) = f_u_to_a
|
||||||
|
stateful function f_a_to_u_to_c(_ : Animal) : (unit => Cat) = f_u_to_c
|
||||||
|
stateful function f_c_to_u_to_a(_ : Cat) : (unit => Animal) = f_u_to_a
|
||||||
|
stateful function f_c_to_u_to_c(_ : Cat) : (unit => Cat) = f_u_to_c
|
||||||
|
|
||||||
|
stateful function f_u_to_tb_a(_ : unit) : tb(Animal) = TB(f_u_to_a)
|
||||||
|
stateful function f_u_to_tb_c(_ : unit) : tb(Cat) = TB(f_u_to_c)
|
||||||
|
|
||||||
|
stateful entrypoint init() =
|
||||||
|
let va1 : ta(Animal) = TA(f_a_to_u) // success
|
||||||
|
let va2 : ta(Animal) = TA(f_c_to_u) // fail
|
||||||
|
let va3 : ta(Cat) = TA(f_a_to_u) // success
|
||||||
|
let va4 : ta(Cat) = TA(f_c_to_u) // success
|
||||||
|
|
||||||
|
let vb1 : tb(Animal) = TB(f_u_to_a) // success
|
||||||
|
let vb2 : tb(Animal) = TB(f_u_to_c) // success
|
||||||
|
let vb3 : tb(Cat) = TB(f_u_to_a) // fail
|
||||||
|
let vb4 : tb(Cat) = TB(f_u_to_c) // success
|
||||||
|
|
||||||
|
let vc1 : tc(Animal) = TC(f_a_to_a) // success
|
||||||
|
let vc2 : tc(Animal) = TC(f_a_to_c) // fail
|
||||||
|
let vc3 : tc(Animal) = TC(f_c_to_a) // fail
|
||||||
|
let vc4 : tc(Animal) = TC(f_c_to_c) // fail
|
||||||
|
let vc5 : tc(Cat) = TC(f_a_to_a) // fail
|
||||||
|
let vc6 : tc(Cat) = TC(f_a_to_c) // fail
|
||||||
|
let vc7 : tc(Cat) = TC(f_c_to_a) // fail
|
||||||
|
let vc8 : tc(Cat) = TC(f_c_to_c) // success
|
||||||
|
|
||||||
|
let vd1 : td(Animal) = TD(f_u_to_u) // success
|
||||||
|
let vd2 : td(Cat) = TD(f_u_to_u) // success
|
||||||
|
|
||||||
|
let ve1 : te(Animal) = TE1(f_a_to_u) // success
|
||||||
|
let ve2 : te(Animal) = TE1(f_c_to_u) // fail
|
||||||
|
let ve3 : te(Animal) = TE2(f_u_to_a) // success
|
||||||
|
let ve4 : te(Animal) = TE2(f_u_to_c) // fail
|
||||||
|
let ve5 : te(Cat) = TE1(f_a_to_u) // fail
|
||||||
|
let ve6 : te(Cat) = TE1(f_c_to_u) // success
|
||||||
|
let ve7 : te(Cat) = TE2(f_u_to_a) // fail
|
||||||
|
let ve8 : te(Cat) = TE2(f_u_to_c) // success
|
||||||
|
|
||||||
|
let vf1 : tf(Animal) = TF(f_ta_a_to_u) // success
|
||||||
|
let vf2 : tf(Animal) = TF(f_ta_c_to_u) // success
|
||||||
|
let vf3 : tf(Cat) = TF(f_ta_a_to_u) // fail
|
||||||
|
let vf4 : tf(Cat) = TF(f_ta_c_to_u) // success
|
||||||
|
|
||||||
|
let vg1 : tg(Animal) = TG(f_tb_a_to_u) // success
|
||||||
|
let vg2 : tg(Animal) = TG(f_tb_c_to_u) // fail
|
||||||
|
let vg3 : tg(Cat) = TG(f_tb_a_to_u) // success
|
||||||
|
let vg4 : tg(Cat) = TG(f_tb_c_to_u) // success
|
||||||
|
|
||||||
|
let vh1 : th(Animal) = TH(f_u_to_ta_a) // success
|
||||||
|
let vh2 : th(Animal) = TH(f_u_to_ta_c) // fail
|
||||||
|
let vh3 : th(Cat) = TH(f_u_to_ta_a) // success
|
||||||
|
let vh4 : th(Cat) = TH(f_u_to_ta_c) // success
|
||||||
|
|
||||||
|
let vi1 : ti(Animal) = TI(f_u_to_tb_a) // success
|
||||||
|
let vi2 : ti(Animal) = TI(f_u_to_tb_c) // success
|
||||||
|
let vi3 : ti(Cat) = TI(f_u_to_tb_a) // fail
|
||||||
|
let vi4 : ti(Cat) = TI(f_u_to_tb_c) // success
|
||||||
|
|
||||||
|
let vj1 : tj(Animal) = TJ(f_a_to_u_to_a) // success
|
||||||
|
let vj2 : tj(Animal) = TJ(f_a_to_u_to_c) // fail
|
||||||
|
let vj3 : tj(Animal) = TJ(f_c_to_u_to_a) // fail (TODO)
|
||||||
|
let vj4 : tj(Animal) = TJ(f_c_to_u_to_c) // success
|
||||||
|
let vj5 : tj(Cat) = TJ(f_a_to_u_to_a) // fail
|
||||||
|
let vj6 : tj(Cat) = TJ(f_a_to_u_to_c) // fail
|
||||||
|
let vj7 : tj(Cat) = TJ(f_c_to_u_to_a) // fail (TODO)
|
||||||
|
let vj8 : tj(Cat) = TJ(f_c_to_u_to_c) // success
|
||||||
|
|
||||||
|
let vk01 : tk(Animal, Animal) = TK(f_a_to_a_to_u) // success
|
||||||
|
let vk02 : tk(Animal, Animal) = TK(f_a_to_c_to_u) // fail
|
||||||
|
let vk03 : tk(Animal, Animal) = TK(f_c_to_a_to_u) // success
|
||||||
|
let vk04 : tk(Animal, Animal) = TK(f_c_to_c_to_u) // fail
|
||||||
|
let vk05 : tk(Animal, Cat) = TK(f_a_to_a_to_u) // success
|
||||||
|
let vk06 : tk(Animal, Cat) = TK(f_a_to_c_to_u) // success
|
||||||
|
let vk07 : tk(Animal, Cat) = TK(f_c_to_a_to_u) // success
|
||||||
|
let vk08 : tk(Animal, Cat) = TK(f_c_to_c_to_u) // success
|
||||||
|
let vk09 : tk(Cat, Animal) = TK(f_a_to_a_to_u) // fail
|
||||||
|
let vk10 : tk(Cat, Animal) = TK(f_a_to_c_to_u) // fail
|
||||||
|
let vk11 : tk(Cat, Animal) = TK(f_c_to_a_to_u) // success
|
||||||
|
let vk12 : tk(Cat, Animal) = TK(f_c_to_c_to_u) // fail
|
||||||
|
let vk13 : tk(Cat, Cat) = TK(f_a_to_a_to_u) // fail
|
||||||
|
let vk14 : tk(Cat, Cat) = TK(f_a_to_c_to_u) // fail
|
||||||
|
let vk15 : tk(Cat, Cat) = TK(f_c_to_a_to_u) // success
|
||||||
|
let vk16 : tk(Cat, Cat) = TK(f_c_to_c_to_u) // success
|
||||||
|
|
||||||
|
()
|
Loading…
x
Reference in New Issue
Block a user