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

From: John Clements (clements at brinckerhoff.org)
Date: Tue Apr 8 13:54:27 EDT 2014

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….

Posted on the users mailing list.