occurrence typing fails on Listof vs List about typed-racket HOT 2 OPEN

I started taking a look at this yesterday, and part of the problem is what the actual type of cadr is in TR versus what you could reasonably expect. TR is currently taking the approach that type for cadr and friends only have logical information if there is no possibility of failure at runtime (i.e the pair structure is correct), but that it is also fine to apply it to a (Listof a). In your example r is not necessarily of the right structure because the inner (Listof (U String False)) could be null. Thus there is no logical information for the if to enhance the environment on. I believe this is easily fixable in some cases (which would cover this case).

The tricky cases are cadr applied to a value of the type (Pair A (Listof B)), which would currently return (U A B). So the question in these cases is what are the exact runtime failures that we allow to be not ruled out by the type? My thought is that it should be that if the runtime value that we need to be a cons-cell is null, then it should be allowed by the type.

The second issue is that inference doesn't take the object environment into account. So if we have x : (Listof (U False String)) and we know that car @ x has type String, then we still cannot infer type variables for car such that it returns a String in the expression (car x), but ((inst car String Any) x will work because typechecking does use the object environment.

from typed-racket.

I have an in-progress pull request that I think solves the first part (fixing the types for cadr etc) here: #15

But it doesn't currently pass the tests due to a type inference limitation. Also my PR probably doesn't the second issue you point out.

from typed-racket.