`in-list` in comprehension forms type-checks with anything

[philnguyen]

What version of Racket are you using?

v7.0

What program did you run?

#lang typed/racket/base
(for ([n (in-list 53)])
  42)

What should have happened?

Program fails to type-check

If you got an error message, please include it here.

Program type-checks and fails at run-time:

; in-list: contract violation
;   expected: list?
;   given: 53

(in-list 53) used in an expression position fails to type-check as expected:

#lang typed/racket/base
(in-list 53)
; Type Checker: Polymorphic function `in-list' could not be applied to arguments:
; Argument 1:
;   Expected: (Listof a)
;   Given:    Positive-Byte
; 
; Result type:     (Sequenceof a)
; Expected result: AnyValues
; 
;   in: (in-list 53)

[samth]

This is basically the same as:

#lang typed/racket/base
(define x 53)
(when (list? x)
  (length x))

In both cases, Typed Racket proves that there's some dead code, and logs a warning. Maybe the warning could also say something about an unconditional error in your code, but the biggest issue is that warnings are hard to see in Racket.

[samth]

That isn't to say that this is a great situation -- as you saw, it can be quite confusing. But the assumption behind this behavior, that macros expanding into dead, type-incorrect, code should not be an error, is pretty fundamental in TR and I haven't yet found a better balance of the constraints here.

[gus-massa]

I think that a better version of the expansion is:

#lang typed/racket

(define x 53)
(unless (list? x)
  (error "not a list" x))

IIUC the problem is that for recognizes in-list and then it expands to a version that doesn't include in-list but it has a call to check the possible error, so TR is happy that the error will be properly handled.

[sorawee]

As I understand, the expanded code is an if expression where the then branch performs the actual loop and the else branch raises a runtime error. From what @samth said, it looks like the then branch is eliminated, leaving the else branch. However, that's still a run-time error, not compile-time error.

[racket-discourse-github-bot]

This issue has been mentioned on Racket Discussions. There might be relevant details there:

https://racket.discourse.group/t/no-static-type-checking-of-in-list-form-used-in-for/1548/2

[jbclements]

I ran into this again today, so I 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)

Is there something wrong with making this the definition of in-list in typed racket? I'm probably missing something.

[jbclements]

Oog... well, one small problem that turns up immediately is that using this is observed to cause TR to "collapse" certain types, e.g. (Listof (List String Integer)) into (Listof (Listof (U String Integer))). So I'm having to insert more annotations with this workaround.

[samth]

The right solution is for in-list to tell TR that the error case ought to be dead code. There may already be a syntax property that indicates that, in which case we should use it.

[sorawee]

One thought that I have is to create something like check-list that raises a run-time error when the input is not a list. Then, we export this check-list in a submodule that is not meant to be used publicly. TR would then give the type of (-> List Void) to this function in the base environment.

The method that @samth mentioned similarly requires editing the implementation of for, but I find that method less ideal since it explicitly mentions TR in a program that shouldn't need to concern with TR.

[gus-massa]

I think that TR shadows many of the racket primitives. Is it possible to shadow in-list too?