[racket] typed racket and unions of vector types

On 07/20/2014 02:08 PM, Alexander D. Knauth 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?

Great question. Sam?

TR's behavior here hasn't caused problems for `math/array` because it

1. Converts array shapes to (Vectorof Index) immediately by copying them 
while ensuring the dimensions are indexes.

2. Checks array indexes against array shapes, also by making a copy 
while checking elements' ranges.

The latter is convenient: checking an Integer to make sure it's 
nonnegative and smaller than a known Index proves to TR that the integer 
is really an Index.

The two functions that do it are in `math/private/array/utils`, and have 
these types:

   check-array-shape : (-> In-Indexes (-> Nothing) Indexes)
   check-array-indexes : (-> Symbol Indexes In-Indexes Indexes)

In `check-array-shape`, the (-> Nothing) argument is a failure thunk. In 
`check-array-indexes`, the Symbol is the name of a function reported in 
the out-of-bounds error. Both return a copy of the In-Indexes argument.

Neil ⊥