Bad optimization with (if (pair? rest) …) on polymorphic rest argument (unsound)

[SuzanneSoy]

What version of Racket are you using?

6.6.0.1

What program did you run?

#lang typed/racket
((λ #:∀ (A ...) [rest : A ... A]
   (if (pair? rest)
       #t
       #f))
 1)
; => #f

What should have happened?

The result should be #t, but the program outputs #f. When typing this expression at the REPL, we can see racket incorrectly inferred the return type is False.

Without the (if … #t #f), the program outputs #t as expected:

#lang typed/racket
((λ #:∀ (A ...) [rest : A ... A]
   (pair? rest))
 1)
; => #t

Also, when using a regular Any * rest argument instead of the polymorphic A ... A, the result is correct:

#lang typed/racket
((λ [rest : Any *]
   (if (pair? rest)
       #t
       #f))
 1)
; => #t

I couldn't find a way to turn this into unsafe behaviour, so the problem is "just" incorrect results.

[SuzanneSoy]

I managed to construct an unsound example based on this:

#lang typed/racket

(define v ((λ #:∀ (A ...) [rest : A ... A]
             (let ([p (pair? rest)])
               (if p p p)))
           1))

(ann v #f) ; => #t

And for extra fun, we can cause a run-time error:

#lang typed/racket

(define v ((λ #:∀ (A ...) [rest : A ... A]
             (let ([p (pair? rest)])
               (if p p p)))
           1))

(: fn (case→ (→ #f Integer)
               (→ #t String)))
(define (fn b)
  (if b "oops" 1))
(+ (fn v) 2)
; => +: contract violation
;      expected: number?
;      given: "oops"

[stamourv]

FWIW, the bad optimization is just a symptom. The underlying cause is highly likely to be a bug in TR's unreachable code detection, which has historically been pretty brittle.

[racket-discourse-github-bot]

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

https://racket.discourse.group/t/predicate-inconsistency-in-with-list-listof-in-polymorphic-functions/3187/4