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

[SuzanneSoy]

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.

[SuzanneSoy]

Here are a couple more test cases for this:

#lang typed/racket
(: f (∀ (A ...)
        (-> (List A ... A)
            (List 'a ... A))))
(define (f xs)
  (map (const 'a) xs))

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

#lang typed/racket
(: f (∀ (A ...)
        (-> (List A ... A)
            (List (Pairof 'a A) ... A))))
(define (f xs)
  (map (λ #:∀ (X) ([x : X]) (cons 'a x)) xs))

(f (map (const 'x) (range 3)))
;; =>
;; - : (Listof 'x)
;; '((a . x) (a . x) (a . x))
;; Should be (Listof (Pairof 'a 'x))

These do not need f to return a function, and the bug is still occurring.