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

Rename datatypes in custom types variance switching test for readability

Browse Source
This commit is contained in:
Gaith Hallak 2022-05-25 17:28:30 +04:00
parent 025e0f7b8f
commit ef3b0dece9
2 changed files with 141 additions and 141 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

112
test/aeso_compiler_tests.erl
View File

@ -881,114 +881,114 @@ failing_contracts() ->
"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)
[<<?Pos(56,39)
"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)
"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 `TB(f_u_to_a) : tb(Animal)` against the expected type `tb(Cat)`">>,
<<?Pos(66,32)
"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"
" `TC : ((Animal) => Animal) => tc(Animal)`\n"
" `DT_INV : ((Animal) => Animal) => dt_inv(Animal)`\n"
"to arguments\n"
" `f_a_to_c : (Animal) => Cat`">>,
<<?Pos(67,32)
<<?Pos(67,36)
"Cannot unify `Cat` and `Animal` in a invariant context\n"
"when checking the application of\n"
" `TC : ((Cat) => Cat) => tc(Cat)`\n"
" `DT_INV : ((Cat) => Cat) => dt_inv(Cat)`\n"
"to arguments\n"
" `f_c_to_a : (Cat) => Animal`">>,
<<?Pos(68,32)
<<?Pos(68,36)
"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)
"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 `TC(f_a_to_a) : tc(Animal)` against the expected type `tc(Cat)`">>,
<<?Pos(70,32)
"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 application of\n"
" `TC : ((Animal) => Animal) => tc(Animal)`\n"
" `DT_INV : ((Animal) => Animal) => dt_inv(Animal)`\n"
"to arguments\n"
" `f_a_to_c : (Animal) => Cat`">>,
<<?Pos(71,32)
<<?Pos(71,36)
"Cannot unify `Cat` and `Animal` in a invariant context\n"
"when checking the application of\n"
" `TC : ((Cat) => Cat) => tc(Cat)`\n"
" `DT_INV : ((Cat) => Cat) => dt_inv(Cat)`\n"
"to arguments\n"
" `f_c_to_a : (Cat) => Animal`">>,
<<?Pos(78,32)
<<?Pos(78,40)
"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)
"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)
"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)
"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)
"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)
"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)
"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)
"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)
"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)
"when checking the type of the expression `DT_CO_NEST_A(f_ta_a_to_u) : dt_co_nest_a(Animal)` against the expected type `dt_co_nest_a(Cat)`">>,
<<?Pos(92,46)
"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)
"when checking the type of the expression `DT_CONTRA_NEST_A(f_tb_c_to_u) : dt_contra_nest_a(Cat)` against the expected type `dt_contra_nest_a(Animal)`">>,
<<?Pos(97,46)
"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)
"when checking the type of the expression `DT_CONTRA_NEST_B(f_u_to_ta_c) : dt_contra_nest_b(Cat)` against the expected type `dt_contra_nest_b(Animal)`">>,
<<?Pos(103,42)
"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)
"when checking the type of the expression `DT_CO_NEST_B(f_u_to_tb_a) : dt_co_nest_b(Animal)` against the expected type `dt_co_nest_b(Cat)`">>,
<<?Pos(107,41)
"Cannot unify `Animal` and `Cat` in a invariant context\n"
"when checking the application of\n"
" `TJ : ((Animal) => (unit) => Animal) => tj(Animal)`\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(108,32)
<<?Pos(108,41)
"Cannot unify `Cat` and `Animal` in a invariant context\n"
"when checking the application of\n"
" `TJ : ((Cat) => (unit) => Cat) => tj(Cat)`\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,32)
<<?Pos(110,41)
"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)
"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"
" `TJ : ((Animal) => (unit) => Animal) => tj(Animal)`\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,32)
<<?Pos(112,41)
"Cannot unify `Cat` and `Animal` in a invariant context\n"
"when checking the application of\n"
" `TJ : ((Cat) => (unit) => Cat) => tj(Cat)`\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(116,41)
<<?Pos(116,55)
"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)
"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)`">>,
<<?Pos(118,55)
"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)
"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)`">>,
<<?Pos(123,55)
"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)
"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 `TK(f_a_to_c_to_u) : tk(Animal, Cat)` against the expected type `tk(Cat, Animal)`">>,
<<?Pos(126,41)
"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"
"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)
"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)`">>,
<<?Pos(127,55)
"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)
"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)`">>,
<<?Pos(128,55)
"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)`">>
"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)`">>
])
, ?TYPE_ERROR(polymorphism_variance_switching_records,
[<<?Pos(27,13)

170
test/contracts/polymorphism_variance_switching_custom_types.aes
View File

@ -5,17 +5,17 @@ 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)
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_a_co_b_contra('a, 'b) = DT_A_CO_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
@ -26,12 +26,12 @@ main contract Main =
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)
function f_ta_a_to_u(_ : dt_contra(Animal)) : unit = ()
function f_ta_c_to_u(_ : dt_contra(Cat)) : unit = ()
function f_tb_a_to_u(_ : dt_co(Animal)) : unit = ()
function f_tb_c_to_u(_ : dt_co(Cat)) : unit = ()
function f_u_to_ta_a(_ : unit) : dt_contra(Animal) = DT_CONTRA(f_a_to_u)
function f_u_to_ta_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()
@ -48,85 +48,85 @@ main contract Main =
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 function f_u_to_tb_a(_ : unit) : dt_co(Animal) = DT_CO(f_u_to_a)
stateful function f_u_to_tb_c(_ : unit) : dt_co(Cat) = DT_CO(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 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 : 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 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 : 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 vc1 : dt_inv(Animal) = DT_INV(f_a_to_a) // success
let vc2 : dt_inv(Animal) = DT_INV(f_a_to_c) // 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 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 : td(Animal) = TD(f_u_to_u) // success
let vd2 : td(Cat) = TD(f_u_to_u) // success
let vd1 : dt_biv(Animal) = DT_BIV(f_u_to_u) // success
let vd2 : dt_biv(Cat) = DT_BIV(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 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 : 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 vf1 : dt_co_nest_a(Animal) = DT_CO_NEST_A(f_ta_a_to_u) // success
let vf2 : dt_co_nest_a(Animal) = DT_CO_NEST_A(f_ta_c_to_u) // success
let vf3 : dt_co_nest_a(Cat) = DT_CO_NEST_A(f_ta_a_to_u) // fail
let vf4 : dt_co_nest_a(Cat) = DT_CO_NEST_A(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 vg1 : dt_contra_nest_a(Animal) = DT_CONTRA_NEST_A(f_tb_a_to_u) // success
let vg2 : dt_contra_nest_a(Animal) = DT_CONTRA_NEST_A(f_tb_c_to_u) // fail
let vg3 : dt_contra_nest_a(Cat) = DT_CONTRA_NEST_A(f_tb_a_to_u) // success
let vg4 : dt_contra_nest_a(Cat) = DT_CONTRA_NEST_A(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 vh1 : dt_contra_nest_b(Animal) = DT_CONTRA_NEST_B(f_u_to_ta_a) // success
let vh2 : dt_contra_nest_b(Animal) = DT_CONTRA_NEST_B(f_u_to_ta_c) // fail
let vh3 : dt_contra_nest_b(Cat) = DT_CONTRA_NEST_B(f_u_to_ta_a) // success
let vh4 : dt_contra_nest_b(Cat) = DT_CONTRA_NEST_B(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 vi1 : dt_co_nest_b(Animal) = DT_CO_NEST_B(f_u_to_tb_a) // success
let vi2 : dt_co_nest_b(Animal) = DT_CO_NEST_B(f_u_to_tb_c) // success
let vi3 : dt_co_nest_b(Cat) = DT_CO_NEST_B(f_u_to_tb_a) // fail
let vi4 : dt_co_nest_b(Cat) = DT_CO_NEST_B(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
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
let vj8 : tj(Cat) = TJ(f_c_to_u_to_c) // 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 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 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 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 : 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
let vk01 : dt_a_co_b_contra(Animal, Animal) = DT_A_CO_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 vk03 : dt_a_co_b_contra(Animal, Animal) = DT_A_CO_B_CONTRA(f_c_to_a_to_u) // success
let vk04 : dt_a_co_b_contra(Animal, Animal) = DT_A_CO_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 vk06 : dt_a_co_b_contra(Animal, Cat) = DT_A_CO_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 vk08 : dt_a_co_b_contra(Animal, Cat) = DT_A_CO_B_CONTRA(f_c_to_c_to_u) // success
let vk09 : dt_a_co_b_contra(Cat, Animal) = DT_A_CO_B_CONTRA(f_a_to_a_to_u) // fail
let vk10 : dt_a_co_b_contra(Cat, Animal) = DT_A_CO_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 vk12 : dt_a_co_b_contra(Cat, Animal) = DT_A_CO_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 vk14 : dt_a_co_b_contra(Cat, Cat) = DT_A_CO_B_CONTRA(f_a_to_c_to_u) // fail
let vk15 : dt_a_co_b_contra(Cat, Cat) = DT_A_CO_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
()