Passing Listof to a (List 'x ... A) can cause unsound results

What version of Racket are you using?

6.8.0.1

What program did you run?

#lang typed/racket

(: f (∀ (A ...)
        (-> (List 'x ... A)
            (-> (List 'a ... A)))))
(define ((f xs))
  (map (λ (x) 'a) xs))

((f (map (const 'x) (range 3))))
;; =>
;; - : (Listof Nothing)
;; '(a a a)

What should have happened?

The ((f (map (const 'x) (range 3)))) expression should produce a (Listof 'a), not a (Listof Nothing). The current result type is unsound, and allows 'a to be "cast" as Number:

(car (ann ((f (map (const 'x) (range 3))))
          (Listof Number)))
;; =>
;; - : Number
;; 'a

Note that this does not happen if f directly returns the (List 'a ... A), there has to be a nested function type, otherwise the argument is simply rejected (which at least is not unsound).

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

Start by running the supplied #lang typed/racket reproducer and compare its inferred type with the expected (Listof 'a). Investigate the nested polymorphic function case involving (List 'x ... A) and verify that the ann expression can no longer treat 'a as Number; the issue names no source file or test path.