[racket] Typed Racket can't filter non-false yet?

I want to write this piece of code:

(: only-non-false (All (T) ((Listof (U T False)) -> (Listof T))))
(define (only-non-false l)
  (filter (ann (lambda (x) x)
               ((U T False) -> Any : T))
          l))

... but Typed Racket says:

Type Checker: Expected result with filter ((T @ x) | (! T @ x)), got filter ((! False @ x) | (False @ x)) in: x

I'm guessing that Typed Racket isn't clever enough to figure out that when the input is (U T False), that a filter on not-false is the same as a filter on T.

I gave up on the general case and focused in on the specific one I want, and ran into another problem where I want subtyping.

Specifically, consider this code:

#lang typed/racket

(: a (Listof (U False (Listof Number))))
(define a '((34) #f (9 22) #f))

(ann (filter pair? a)
     (Listof (Listof Number)))

I know that the result is a list of numbers, but that information gets lost... I suppose the abstraction that I need here would be something like a case on the right-hand-side of a filter type... oog, no, I think that still wouldn't help. 

I can solve this by refining the predicate so that it matches the (Listof Number) type exactly, but that seems a bit cumbersome.  

Am I missing something obvious in either of these?

Alas, things like this are why TR is *still* in the bin of "things-I-tackle-when-I'm-not-pressured-for-time".

Thanks!

John

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 4624 bytes
Desc: not available
URL: <http://lists.racket-lang.org/users/archive/attachments/20120130/c272e327/attachment.p7s>