Test variance switching for bivariant records

This commit is contained in:
Gaith Hallak 2022-05-24 22:16:34 +04:00
parent 08d0c7034f
commit e5c6efc8ae
2 changed files with 13 additions and 5 deletions

View File

@ -991,19 +991,19 @@ failing_contracts() ->
"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 `TK(f_a_to_c_to_u) : tk(Animal, Cat)` against the expected type `tk(Cat, Cat)`">>
]) ])
, ?TYPE_ERROR(polymorphism_variance_switching_records, , ?TYPE_ERROR(polymorphism_variance_switching_records,
[<<?Pos(26,13) [<<?Pos(27,13)
"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 pattern `r03 : rec_a(Cat)` against the expected type `Main.rec_a(Animal)`">>, "when checking the type of the pattern `r03 : rec_a(Cat)` against the expected type `Main.rec_a(Animal)`">>,
<<?Pos(32,13) <<?Pos(33,13)
"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 pattern `r06 : rec_b(Animal)` against the expected type `Main.rec_b(Cat)`">>, "when checking the type of the pattern `r06 : rec_b(Animal)` against the expected type `Main.rec_b(Cat)`">>,
<<?Pos(40,13) <<?Pos(41,13)
"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 pattern `r11 : rec_c(Cat)` against the expected type `Main.rec_c(Animal)`">>, "when checking the type of the pattern `r11 : rec_c(Cat)` against the expected type `Main.rec_c(Animal)`">>,
<<?Pos(46,13) <<?Pos(47,13)
"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 pattern `r16 : rec_d(Animal)` against the expected type `Main.rec_d(Cat)`">>, "when checking the type of the pattern `r16 : rec_d(Animal)` against the expected type `Main.rec_d(Cat)`">>,
<<?Pos(47,13) <<?Pos(48,13)
"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 pattern `r17 : rec_d(Cat)` against the expected type `Main.rec_d(Animal)`">>]) "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, , ?TYPE_ERROR(polymorphism_variance_switching_oracles,

View File

@ -10,6 +10,7 @@ main contract Main =
record rec_c('a) = { x : () => 'a} record rec_c('a) = { x : () => 'a}
record rec_d('a) = { x : 'a => unit, record rec_d('a) = { x : 'a => unit,
y : () => 'a } y : () => 'a }
record rec_e('a) = { x : int }
stateful entrypoint new_cat() : Cat = Chain.create() stateful entrypoint new_cat() : Cat = Chain.create()
stateful entrypoint new_animal() : Animal = new_cat() stateful entrypoint new_animal() : Animal = new_cat()
@ -47,4 +48,11 @@ main contract Main =
let r17 : rec_d(Cat) = rxaya // fail let r17 : rec_d(Cat) = rxaya // fail
let r20 : rec_d(Cat) = rxcyc // success let r20 : rec_d(Cat) = rxcyc // success
let rba : rec_e(Animal) = { x = 1 }
let rbc : rec_e(Cat) = { x = 1 }
let r21 : rec_e(Animal) = rba // success
let r21 : rec_e(Animal) = rbc // success
let r22 : rec_e(Cat) = rba // success
let r22 : rec_e(Cat) = rbc // success
() ()