diff --git a/test/aeso_compiler_tests.erl b/test/aeso_compiler_tests.erl
index d636bc9..bacc128 100644
--- a/test/aeso_compiler_tests.erl
+++ b/test/aeso_compiler_tests.erl
@@ -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)
diff --git a/test/contracts/polymorphism_variance_switching_custom_types.aes b/test/contracts/polymorphism_variance_switching_custom_types.aes
index 120e07d..a4c448b 100644
--- a/test/contracts/polymorphism_variance_switching_custom_types.aes
+++ b/test/contracts/polymorphism_variance_switching_custom_types.aes
@@ -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
 
         ()