[racket] typed racket and unions of vector types

This could be made to typecheck via a variety of methods:

- We could add something ad-hoc to `vector-ref`.
- We could add use-site variance to Typed Racket, so that it could
tell that `vector-ref` is covariant (while `vector-set!` would be
contra-variant).
- We could do something less ad-hoc that handled unions.

I'm reluctant to do the first, since it seems like not a big win for
the added complexity. The second would be a lot of work, but would add
expressiveness. The third might be the best idea, but I don't actually
know what the less-ad-hoc thing would be.

Sam

On Sun, Jul 20, 2014 at 2:08 PM, Alexander D. Knauth
<alexander at knauth.org> wrote:
> I ran into this when trying to do vector-ref on a value of type In-Indexes
> from math/array.
>
> If I do something like this:
>
> #lang typed/racket
>
> (: v : (U (Vectorof Index)
>           (Vectorof Integer)))
> (define v #(0))
>
> (ann (vector-ref v 0) Integer)
>
> Then it doesn't type check.  I understand that (Vectorof Index) isn’t a
> subtype of (Vectorof Integer), but still, why doesn’t this work?
>
> Is there any reason why the type checker doesn’t do something where it
> checks both components of a union type and if both work then the union type
> works?
>
>
>
> ____________________
>   Racket Users list:
>   http://lists.racket-lang.org/users
>