missing cast, unsound

[bennn]

Retic with blame (commit 7adef84) and the current master (5cd2d10) don't insert some casts (=>) shown in the paper.

Example program:

def main(xs:Dyn)->str:
    return xs[0]

main([1])

Since xs has type Dyn, there should be a cast from Dyn to List(Dyn) just before the dereference. (Figure 4 in POPL'17.) But this cast is missing:

(commit 7adef84)

$ retic --mgd-transient --print file.py
from retic.runtime import *
from retic.mgd_transient import *
from retic.typing import *
gensym5 = Dyn
gensym3 = String
gensym0 = Dyn
gensym2 = Dyn
gensym1 = Function(NamedParameters([('xs', Dyn)]), String)
gensym4 = List(Int)

def main(xs):
    return mgd_cast_type_string(xs[0], gensym2, '2', gensym3)
mgd_check_type_string(main(mgd_cast_type_dyn([1], gensym4, '4', gensym5)), main, 2)

And Retic can't blame xs for not being a list of strings.

Retic also gives a Python error when xs is not a list --- again because of the missing cast:

(commit 5cd2d10)

def main(xs:Dyn)->str:
    s = xs[0]
    return s

main(1)

# $ retic --transient file.py
# TypeError: 'int' object is not subscriptable