Incorrect expansion of pair? assertion in polymorphic function operating on a List A ...

[EricKalkman]

Related to (or maybe the same as?) to #412

What version of Racket are you using?

v8.14 [cs]

What program did you run?

#lang typed/racket/base

(: ttest-homo (All (A) (-> (Listof A) (Listof A))))
(define (ttest-homo lst)
  (display (format "pair? ~a; list? ~a~%" (pair? lst) (list? lst)))
  (unless (pair? lst)  ; or (assert lst pair?)
    (error 'wat))
  lst)

(: ttest-hetero (All (A  ...) (-> (List A ... A) (List A ... A))))
(define (ttest-hetero lst)
  (display (format "pair? ~a; list? ~a~%" (pair? lst) (list? lst)))
  (unless (pair? lst)  ; or (assert lst pair?)
    (error 'wat))
  lst)

(define inp (ann '(1 2 3) (List Natural Natural Natural)))

(ttest-homo inp)
;pair? #t; list? #t
;'(1 2 3)

(ttest-hetero inp)
;pair? #t; list? #t
;error: wat

What should have happened?

The program consists of two polymorphic functions with identical bodies that return the argument after asserting that it is a pair with pair?. The functions are typed on homogeneous and heterogeneous lists, respectively (ttest-homo and ttest-hetero, respectively). Neither function should produce an error when passed a non-empty list.

However, ttest-hetero fails the pair? assertion when passed '(1 2 3) despite print debugging suggesting that the check should succeed. In contrast, its twin ttest-homo correctly returns without erroring.

The program typechecks successfully.

EmEf on Racket Discourse suggested stepping through the TR macros, revealing a problematic expansion of the predicate in the unless block to always return #f in ttest-hetero:

(define-values:125 (ttest-hetero)
  (lambda:126 (lst)
    (#%app:128 display (#%app:129 format (quote "pair? ~a; list? ~a~%")
                                  (#%app:130 pair? lst) (#%app:131 list? lst)))
    (if (begin (#%app:132 pair? lst) (quote #f))  ;;; <<< ERRONEOUS (quote #f)
        (#%app:133 void:133)
        (let-values:134 () (#%app:135 error 'wat)))
    lst))

; expansion of ttest-homo, which executes correctly, for comparison
(define-values:112 (ttest-homo)
  (lambda:113 (lst)
    (#%app:115 display (#%app:116 format (quote "pair? ~a; list? ~a~%")
                                  (#%app:117 pair? lst)
                                  (#%app:118 list? lst)))
    (if (#%app:119 pair? lst)
        (#%app:120 void:120)
        (let-values:121 () (#%app:122 error 'wat)))
    lst))

The (if (begin ... (quote #f)) ... ...) always goes to its else branch, leading to the error. ttest-homo does not add the extra (quote #f) to the predicate and thus behaves normally.

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

error: wat (lol)

If I replace the (unless ...) with(assert lst pair?), the error is Assertion #<procedure:pair?> failed on '(1 2 3)

[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