Eliminate redundant tests

This commit is contained in:
Gaith Hallak 2022-05-31 00:25:53 +04:00
parent 113d699b01
commit 0237353ea7
2 changed files with 34 additions and 69 deletions

View File

@ -884,105 +884,78 @@ failing_contracts() ->
"when checking the type of the expression `some_animal : Animal` against the expected type `Cat`">> "when checking the type of the expression `some_animal : Animal` against the expected type `Cat`">>
]) ])
, ?TYPE_ERROR(polymorphism_variance_switching_custom_types, , ?TYPE_ERROR(polymorphism_variance_switching_custom_types,
[<<?Pos(57,39) [<<?Pos(56,39)
"Cannot unify `Cat` and `Animal` in a contravariant context\n" "Cannot unify `Cat` and `Animal` in a contravariant context\n"
"when checking the type of the expression `DT_CONTRA(f_c_to_u) : dt_contra(Cat)` against the expected type `dt_contra(Animal)`">>, "when checking the type of the expression `DT_CONTRA(f_c_to_u) : dt_contra(Cat)` against the expected type `dt_contra(Animal)`">>,
<<?Pos(63,35) <<?Pos(62,35)
"Cannot unify `Animal` and `Cat` in a covariant context\n" "Cannot unify `Animal` and `Cat` in a covariant context\n"
"when checking the type of the expression `DT_CO(f_u_to_a) : dt_co(Animal)` against the expected type `dt_co(Cat)`">>, "when checking the type of the expression `DT_CO(f_u_to_a) : dt_co(Animal)` against the expected type `dt_co(Cat)`">>,
<<?Pos(68,36) <<?Pos(67,36)
"Cannot unify `Cat` and `Animal` in a contravariant context\n" "Cannot unify `Cat` and `Animal` in a contravariant context\n"
"when checking the application of\n `DT_INV : ((Cat) => Cat) => dt_inv(Cat)`\nto arguments\n `f_c_to_a : (Cat) => Animal`">>, "when checking the application of\n `DT_INV : ((Cat) => Cat) => dt_inv(Cat)`\nto arguments\n `f_c_to_a : (Cat) => Animal`">>,
<<?Pos(69,36) <<?Pos(68,36)
"Cannot unify `Cat` and `Animal` in a invariant context\n" "Cannot unify `Cat` and `Animal` in a invariant context\n"
"when checking the type of the expression `DT_INV(f_c_to_c) : dt_inv(Cat)` against the expected type `dt_inv(Animal)`">>, "when checking the type of the expression `DT_INV(f_c_to_c) : dt_inv(Cat)` against the expected type `dt_inv(Animal)`">>,
<<?Pos(70,36) <<?Pos(69,36)
"Cannot unify `Animal` and `Cat` in a invariant context\n" "Cannot unify `Animal` and `Cat` in a invariant context\n"
"when checking the type of the expression `DT_INV(f_a_to_a) : dt_inv(Animal)` against the expected type `dt_inv(Cat)`">>, "when checking the type of the expression `DT_INV(f_a_to_a) : dt_inv(Animal)` against the expected type `dt_inv(Cat)`">>,
<<?Pos(71,36) <<?Pos(70,36)
"Cannot unify `Animal` and `Cat` in a invariant context\n" "Cannot unify `Animal` and `Cat` in a invariant context\n"
"when checking the type of the expression `DT_INV(f_a_to_c) : dt_inv(Animal)` against the expected type `dt_inv(Cat)`">>, "when checking the type of the expression `DT_INV(f_a_to_c) : dt_inv(Animal)` against the expected type `dt_inv(Cat)`">>,
<<?Pos(72,36) <<?Pos(71,36)
"Cannot unify `Cat` and `Animal` in a contravariant context\n" "Cannot unify `Cat` and `Animal` in a contravariant context\n"
"when checking the application of\n `DT_INV : ((Cat) => Cat) => dt_inv(Cat)`\nto arguments\n `f_c_to_a : (Cat) => Animal`">>, "when checking the application of\n `DT_INV : ((Cat) => Cat) => dt_inv(Cat)`\nto arguments\n `f_c_to_a : (Cat) => Animal`">>,
<<?Pos(79,40) <<?Pos(78,40)
"Cannot unify `Cat` and `Animal` in a invariant context\n" "Cannot unify `Cat` and `Animal` in a invariant context\n"
"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)`">>, "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(81,40) <<?Pos(80,40)
"Cannot unify `Cat` and `Animal` in a invariant context\n" "Cannot unify `Cat` and `Animal` in a invariant context\n"
"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)`">>, "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(82,40) <<?Pos(81,40)
"Cannot unify `Animal` and `Cat` in a invariant context\n" "Cannot unify `Animal` and `Cat` in a invariant context\n"
"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)`">>, "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(84,40) <<?Pos(83,40)
"Cannot unify `Animal` and `Cat` in a invariant context\n" "Cannot unify `Animal` and `Cat` in a invariant context\n"
"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)`">>, "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(89,42) <<?Pos(88,42)
"Cannot unify `Animal` and `Cat` in a covariant context\n" "Cannot unify `Animal` and `Cat` in a covariant context\n"
"when checking the type of the expression `DT_CO_NEST_A(f_dt_contra_a_to_u) : dt_co_nest_a(Animal)` against the expected type `dt_co_nest_a(Cat)`">>, "when checking the type of the expression `DT_CO_NEST_A(f_dt_contra_a_to_u) : dt_co_nest_a(Animal)` against the expected type `dt_co_nest_a(Cat)`">>,
<<?Pos(93,46) <<?Pos(92,46)
"Cannot unify `Cat` and `Animal` in a contravariant context\n" "Cannot unify `Cat` and `Animal` in a contravariant context\n"
"when checking the type of the expression `DT_CONTRA_NEST_A(f_dt_co_c_to_u) : dt_contra_nest_a(Cat)` against the expected type `dt_contra_nest_a(Animal)`">>, "when checking the type of the expression `DT_CONTRA_NEST_A(f_dt_co_c_to_u) : dt_contra_nest_a(Cat)` against the expected type `dt_contra_nest_a(Animal)`">>,
<<?Pos(98,46) <<?Pos(97,46)
"Cannot unify `Cat` and `Animal` in a contravariant context\n" "Cannot unify `Cat` and `Animal` in a contravariant context\n"
"when checking the type of the expression `DT_CONTRA_NEST_B(f_u_to_dt_contra_c) : dt_contra_nest_b(Cat)` against the expected type `dt_contra_nest_b(Animal)`">>, "when checking the type of the expression `DT_CONTRA_NEST_B(f_u_to_dt_contra_c) : dt_contra_nest_b(Cat)` against the expected type `dt_contra_nest_b(Animal)`">>,
<<?Pos(104,42) <<?Pos(103,42)
"Cannot unify `Animal` and `Cat` in a covariant context\n" "Cannot unify `Animal` and `Cat` in a covariant context\n"
"when checking the type of the expression `DT_CO_NEST_B(f_u_to_dt_co_a) : dt_co_nest_b(Animal)` against the expected type `dt_co_nest_b(Cat)`">>, "when checking the type of the expression `DT_CO_NEST_B(f_u_to_dt_co_a) : dt_co_nest_b(Animal)` against the expected type `dt_co_nest_b(Cat)`">>,
<<?Pos(109,41) <<?Pos(108,13)
"Cannot unify `Cat` and `Animal` in a contravariant context\n"
"when checking the application of\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(111,41)
"Cannot unify `Animal` and `Cat` in a covariant context\n" "Cannot unify `Animal` and `Cat` in a covariant context\n"
"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)`">>, "when checking the type of the pattern `vj3 : dt_co_twice(Cat)` against the expected type `dt_co_twice(Animal)`">>,
<<?Pos(112,41) <<?Pos(112,59)
"Cannot unify `Animal` and `Cat` in a covariant context\n"
"when checking the type of the expression `DT_CO_TWICE(f_a_to_u_to_c) : dt_co_twice(Animal)` against the expected type `dt_co_twice(Cat)`">>,
<<?Pos(113,41)
"Cannot unify `Cat` and `Animal` in a contravariant context\n"
"when checking the application of\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,59)
"Cannot unify `Cat` and `Animal` in a contravariant context\n" "Cannot unify `Cat` and `Animal` in a contravariant context\n"
"when checking the type of the expression `DT_A_CONTRA_B_CONTRA(f_a_to_c_to_u) : dt_a_contra_b_contra(Animal, Cat)` against the expected type `dt_a_contra_b_contra(Animal, Animal)`">>, "when checking the type of the expression `DT_A_CONTRA_B_CONTRA(f_a_to_c_to_u) : dt_a_contra_b_contra(Animal, Cat)` against the expected type `dt_a_contra_b_contra(Animal, Animal)`">>,
<<?Pos(117,59) <<?Pos(113,59)
"Cannot unify `Cat` and `Animal` in a contravariant context\n" "Cannot unify `Cat` and `Animal` in a contravariant context\n"
"when checking the type of the expression `DT_A_CONTRA_B_CONTRA(f_c_to_a_to_u) : dt_a_contra_b_contra(Cat, Animal)` against the expected type `dt_a_contra_b_contra(Animal, Animal)`">>, "when checking the type of the expression `DT_A_CONTRA_B_CONTRA(f_c_to_a_to_u) : dt_a_contra_b_contra(Cat, Animal)` against the expected type `dt_a_contra_b_contra(Animal, Animal)`">>,
<<?Pos(118,59) <<?Pos(114,59)
"Cannot unify `Cat` and `Animal` in a contravariant context\n" "Cannot unify `Cat` and `Animal` in a contravariant context\n"
"when checking the type of the expression `DT_A_CONTRA_B_CONTRA(f_c_to_c_to_u) : dt_a_contra_b_contra(Cat, Cat)` against the expected type `dt_a_contra_b_contra(Animal, Animal)`">>, "when checking the type of the expression `DT_A_CONTRA_B_CONTRA(f_c_to_c_to_u) : dt_a_contra_b_contra(Cat, Cat)` against the expected type `dt_a_contra_b_contra(Animal, Animal)`">>,
<<?Pos(121,59) <<?Pos(117,59)
"Cannot unify `Cat` and `Animal` in a contravariant context\n" "Cannot unify `Cat` and `Animal` in a contravariant context\n"
"when checking the type of the expression `DT_A_CONTRA_B_CONTRA(f_c_to_a_to_u) : dt_a_contra_b_contra(Cat, Animal)` against the expected type `dt_a_contra_b_contra(Animal, Cat)`">>, "when checking the type of the expression `DT_A_CONTRA_B_CONTRA(f_c_to_a_to_u) : dt_a_contra_b_contra(Cat, Animal)` against the expected type `dt_a_contra_b_contra(Animal, Cat)`">>,
<<?Pos(122,59) <<?Pos(118,59)
"Cannot unify `Cat` and `Animal` in a contravariant context\n" "Cannot unify `Cat` and `Animal` in a contravariant context\n"
"when checking the type of the expression `DT_A_CONTRA_B_CONTRA(f_c_to_c_to_u) : dt_a_contra_b_contra(Cat, Cat)` against the expected type `dt_a_contra_b_contra(Animal, Cat)`">>, "when checking the type of the expression `DT_A_CONTRA_B_CONTRA(f_c_to_c_to_u) : dt_a_contra_b_contra(Cat, Cat)` against the expected type `dt_a_contra_b_contra(Animal, Cat)`">>,
<<?Pos(124,59) <<?Pos(120,59)
"Cannot unify `Cat` and `Animal` in a contravariant context\n" "Cannot unify `Cat` and `Animal` in a contravariant context\n"
"when checking the type of the expression `DT_A_CONTRA_B_CONTRA(f_a_to_c_to_u) : dt_a_contra_b_contra(Animal, Cat)` against the expected type `dt_a_contra_b_contra(Cat, Animal)`">>, "when checking the type of the expression `DT_A_CONTRA_B_CONTRA(f_a_to_c_to_u) : dt_a_contra_b_contra(Animal, Cat)` against the expected type `dt_a_contra_b_contra(Cat, Animal)`">>,
<<?Pos(126,59) <<?Pos(122,59)
"Cannot unify `Cat` and `Animal` in a contravariant context\n" "Cannot unify `Cat` and `Animal` in a contravariant context\n"
"when checking the type of the expression `DT_A_CONTRA_B_CONTRA(f_c_to_c_to_u) : dt_a_contra_b_contra(Cat, Cat)` against the expected type `dt_a_contra_b_contra(Cat, Animal)`">>, "when checking the type of the expression `DT_A_CONTRA_B_CONTRA(f_c_to_c_to_u) : dt_a_contra_b_contra(Cat, Cat)` against the expected type `dt_a_contra_b_contra(Cat, Animal)`">>,
<<?Pos(133,45) <<?Pos(129,13)
"Cannot unify `Animal` and `Cat` in a covariant context\n"
"when checking the application of\n `DT_CONTRA_TWICE : ((Animal) => (Animal) => unit) => dt_contra_twice(Animal)`\nto arguments\n `f_a_to_c_to_u : (Animal) => (Cat) => unit`">>,
<<?Pos(134,45)
"Cannot unify `Cat` and `Animal` in a contravariant context\n" "Cannot unify `Cat` and `Animal` in a contravariant context\n"
"when checking the type of the expression `DT_CONTRA_TWICE(f_c_to_a_to_u) : dt_contra_twice(Cat)` against the expected type `dt_contra_twice(Animal)`">>, "when checking the type of the pattern `vl2 : dt_contra_twice(Animal)` against the expected type `dt_contra_twice(Cat)`">>
<<?Pos(135,45)
"Cannot unify `Cat` and `Animal` in a contravariant context\n"
"when checking the type of the expression `DT_CONTRA_TWICE(f_c_to_c_to_u) : dt_contra_twice(Cat)` against the expected type `dt_contra_twice(Animal)`">>,
<<?Pos(137,45)
"Cannot unify `Animal` and `Cat` in a covariant context\n"
"when checking the application of\n"
" `DT_CONTRA_TWICE : ((Animal) => (Animal) => unit) => dt_contra_twice(Animal)`\n"
"to arguments\n"
" `f_a_to_c_to_u : (Animal) => (Cat) => unit`">>
]) ])
, ?TYPE_ERROR(polymorphism_variance_switching_records, , ?TYPE_ERROR(polymorphism_variance_switching_records,
[<<?Pos(27,13) [<<?Pos(27,13)

View File

@ -44,7 +44,6 @@ main contract Main =
stateful function f_c_to_a(_ : Cat) : Animal = f_a() stateful function f_c_to_a(_ : Cat) : Animal = f_a()
stateful function f_c_to_c(_ : Cat) : Cat = f_c() stateful function f_c_to_c(_ : Cat) : Cat = f_c()
stateful function f_a_to_u_to_a(_ : (Animal => unit)) : Animal = f_a()
stateful function f_a_to_u_to_c(_ : (Animal => unit)) : Cat = f_c() stateful function f_a_to_u_to_c(_ : (Animal => unit)) : Cat = f_c()
stateful function f_c_to_u_to_a(_ : (Cat => unit)) : Animal = f_a() stateful function f_c_to_u_to_a(_ : (Cat => unit)) : Animal = f_a()
stateful function f_c_to_u_to_c(_ : (Cat => unit)) : Cat = f_c() stateful function f_c_to_u_to_c(_ : (Cat => unit)) : Cat = f_c()
@ -104,13 +103,10 @@ main contract Main =
let vi3 : dt_co_nest_b(Cat) = DT_CO_NEST_B(f_u_to_dt_co_a) // fail let vi3 : dt_co_nest_b(Cat) = DT_CO_NEST_B(f_u_to_dt_co_a) // fail
let vi4 : dt_co_nest_b(Cat) = DT_CO_NEST_B(f_u_to_dt_co_c) // success let vi4 : dt_co_nest_b(Cat) = DT_CO_NEST_B(f_u_to_dt_co_c) // success
let vj1 : dt_co_twice(Animal) = DT_CO_TWICE(f_a_to_u_to_a) // success let vj1 : dt_co_twice(Animal) = DT_CO_TWICE(f_a_to_u_to_c : (Animal => unit) => Animal) : dt_co_twice(Animal) // success
let vj2 : dt_co_twice(Animal) = DT_CO_TWICE(f_a_to_u_to_c) // success let vj2 : dt_co_twice(Animal) = DT_CO_TWICE(f_c_to_u_to_c : (Cat => unit) => Cat ) : dt_co_twice(Cat) // success
let vj3 : dt_co_twice(Animal) = DT_CO_TWICE(f_c_to_u_to_a) // fail let vj3 : dt_co_twice(Cat) = DT_CO_TWICE(f_c_to_u_to_a : (Animal => unit) => Animal) : dt_co_twice(Animal) // fail
let vj4 : dt_co_twice(Animal) = DT_CO_TWICE(f_c_to_u_to_c) // success let vj4 : dt_co_twice(Cat) = DT_CO_TWICE(f_c_to_u_to_c : (Cat => unit) => Cat ) : dt_co_twice(Cat) // 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 vk01 : dt_a_contra_b_contra(Animal, Animal) = DT_A_CONTRA_B_CONTRA(f_a_to_a_to_u) // success let vk01 : dt_a_contra_b_contra(Animal, Animal) = DT_A_CONTRA_B_CONTRA(f_a_to_a_to_u) // success
let vk02 : dt_a_contra_b_contra(Animal, Animal) = DT_A_CONTRA_B_CONTRA(f_a_to_c_to_u) // fail let vk02 : dt_a_contra_b_contra(Animal, Animal) = DT_A_CONTRA_B_CONTRA(f_a_to_c_to_u) // fail
@ -129,13 +125,9 @@ main contract Main =
let vk15 : dt_a_contra_b_contra(Cat, Cat) = DT_A_CONTRA_B_CONTRA(f_c_to_a_to_u) // success let vk15 : dt_a_contra_b_contra(Cat, Cat) = DT_A_CONTRA_B_CONTRA(f_c_to_a_to_u) // success
let vk16 : dt_a_contra_b_contra(Cat, Cat) = DT_A_CONTRA_B_CONTRA(f_c_to_c_to_u) // success let vk16 : dt_a_contra_b_contra(Cat, Cat) = DT_A_CONTRA_B_CONTRA(f_c_to_c_to_u) // success
let vl1 : dt_contra_twice(Animal) = DT_CONTRA_TWICE(f_a_to_a_to_u) // success let vl1 : dt_contra_twice(Animal) = DT_CONTRA_TWICE(f_a_to_a_to_u : Animal => Animal => unit) : dt_contra_twice(Animal) // success
let vl2 : dt_contra_twice(Animal) = DT_CONTRA_TWICE(f_a_to_c_to_u) // fail let vl2 : dt_contra_twice(Animal) = DT_CONTRA_TWICE(f_a_to_c_to_u : Cat => Cat => unit) : dt_contra_twice(Cat) // fail
let vl3 : dt_contra_twice(Animal) = DT_CONTRA_TWICE(f_c_to_a_to_u) // fail let vl3 : dt_contra_twice(Cat) = DT_CONTRA_TWICE(f_a_to_a_to_u : Animal => Animal => unit) : dt_contra_twice(Animal) // success
let vl4 : dt_contra_twice(Animal) = DT_CONTRA_TWICE(f_c_to_c_to_u) // fail let vl4 : dt_contra_twice(Cat) = DT_CONTRA_TWICE(f_c_to_a_to_u : Cat => Cat => unit) : dt_contra_twice(Cat) // success
let vl5 : dt_contra_twice(Cat) = DT_CONTRA_TWICE(f_a_to_a_to_u) // success
let vl6 : dt_contra_twice(Cat) = DT_CONTRA_TWICE(f_a_to_c_to_u) // fail
let vl7 : dt_contra_twice(Cat) = DT_CONTRA_TWICE(f_c_to_a_to_u) // success
let vl8 : dt_contra_twice(Cat) = DT_CONTRA_TWICE(f_c_to_c_to_u) // success
() ()