List filters override list element filters

[bennn]

(I'm pretty sure this is a bug)

Applying a filter to a list seems to remove any filters we previously applied to the list's elements.

#lang typed/racket/base

(: test (-> (Listof (U (List Natural) Boolean)) Boolean))
(define (test expr)
  (if (list? (car expr))
    (if (not (null? expr))
      (= 1 (car (car expr)))
      #f)
    #f))

;; test.rkt:7:11: Type Checker: Polymorphic function `car' could not be applied to arguments:
;; Domains: (Listof a)
;;          (Pairof a b)
;; Arguments: (U Boolean (List Nonnegative-Integer))

Changing the order of the if tests makes the problem go away.

(Credit to the original SO post: http://stackoverflow.com/questions/33475581/how-to-fix-the-return-value-in-this-typed-racket-code/33489459#33489459)

[samth]

I think this is a bug in restrict.

[rfindler]

This looks like the right output to me, but perhaps I'm confused. When I run this program:

#lang racket/base

;(: test (-> (Listof (U (List Natural) Boolean)) Boolean))
(define (test expr)
  (if (list? (car expr))
      (if (not (null? expr))
          (= 1 (car (car expr)))
          #f)
      #f))

(test '())

I get a runtime error about (car '()) and when I reverse the if arguments:

#lang racket/base

;(: test (-> (Listof (U (List Natural) Boolean)) Boolean))
(define (test expr)
  (if (not (null? expr))
      (if (list? (car expr))
          (= 1 (car (car expr)))
          #f)
      #f))

(test '())

then I get no error.

I think TR is correctly detecting that error.

[samth]

fortunately or not, typed racket doesn't try to prevent that particular runtime error (car of null), so that's not what's happening here.

[bennn]

Also interesting, I expected this program without the null? check to work, but it fails (works fine for a List though). Same as before, the type of expr isn't refined in the "then" branch.

(: test (-> (Listof (U (Listof Natural) Boolean)) Boolean))
(define (test expr)
  (if (list? (car expr))
    (= 1 (car (car expr)))
    #f))

(test '((1)))
;; Type Checker: Polymorphic function `car' could not be applied to arguments:
;; Domains: (Listof a)
;;          (Pairof a b)
;; Arguments: (U Boolean (Listof Nonnegative-Integer))