[racket] TR: Really? I have to put an annotation *there*?

Here's a simpler version of the code, which typechecks:

#lang typed/racket

(define sounds
  (for/list : (Listof String) ([i : Index (ann 7 Index)])
    "abc"))

But yes, in general, recursive functions need more annotations, and it
can be hard to figure out where to put them when said recursive
function is generated by a macro. It might be that `for/list` can put
more annotations in more places, but I think the only real fix is a
more sophisticated form of type inference.

Sam

On Tue, Apr 8, 2014 at 1:54 PM, John Clements <clements at brinckerhoff.org> wrote:
> I feel like I must be missing something, or my TR intuition is seriously broken.  This piece of code:
>
> #lang typed/racket
>
> (define sounds
>   (for/list : (Listof String) ([i : Index (in-range (ann 7 Index))])
>     "abc”))
>
> … fails to type-check with this error:
>
> Type Checker: type mismatch
>   expected: Index
>   given: Integer in: (for/list : (Listof String) ((i : Index (in-range (ann 7 Index)))) "abc”)
>
> … and unfortunately, the whole ‘for’ is highlighted.
>
> I checked the type of “in-range”, and it suggests that if you give it an an Index, it can return a (Sequenceof Index).  Finally, in a fit of desperation, I manually annotated the call to “in-range” with the (Sequenceof Index) type … and it worked.
>
> Does it make sense that this kind of annotation should be required, or is this a bug?
>
> John
>
> P.S.: this is a simplification of code whose body does in fact require that i be of type Index….
> ____________________
>   Racket Users list:
>   http://lists.racket-lang.org/users