No static type checking of 'in-list' form used in 'for'?

Questions & Answers
1

I was surprised by this program's type-checking behavior:

#lang typed/racket

(define definitely-not-a-list string-length)

;; this doesn't type-check:
#;(in-list definitely-not-a-list)

;; and neither does this
#;(for/list : (Listof Real)
  ([i (in-range 4 10)]
   [b definitely-not-a-list])
  i)


;; but this does!
(for/list : (Listof Real)
  ([i (in-range 4 10)]
   [b (in-list definitely-not-a-list)])
  i)

After thinking about it some more, I'm guessing that the 'in-list' is expanded in the context of the 'for' into something that TR has a hard time analyzing, so it just inserts a contract check. I'm guessing that the expansion of for could be enriched to allow TR to check this, but ... maybe it's not worth it?

If my suppositions here are right, it gives me a moment's pause, because it suggests weirdly that I should avoid using in-list in TR code to get better checking.

Am I missing something obvious?

1 Like
2

Old relevant discussion `in-list` in comprehension forms type-checks with anything · Issue #781 · racket/typed-racket · GitHub

2 Likes
3

Ran into this again, came up with this simple workaround.

#lang typed/racket

(define definitely-not-a-list string-length)

(: listy (All (T) ((Listof T) -> (Listof T))))
(define (listy l) l)

(define-syntax (in-list/ck stx)
  (syntax-case stx ()
    [(_ a) #'(in-list (listy a))]))

(for/list : (Listof Real)
  ([i (in-range 4 10)]
   [b (in-list/ck definitely-not-a-list)])
  i)

I'll add this comment to the issue as well.

1 Like