The (filter values ...) idiom should properly restrict type information

The following program does not typecheck under Racket 6.5:

#lang typed/racket

(define lst1 : (Listof (Option Integer))
  '(1 2 #f 4 5))

(define lst2 : (Listof Integer)
  (filter values lst1))

It produces the following type error:

Type Checker: Polymorphic function `filter' could not be applied to arguments:
Types: (-> a Any) (Listof a) -> (Listof a)
Arguments: (All (a b ...) (case-> (-> (values)) (-> a a) (-> a b ... b (values a b ... b)))) (Listof (U Integer False))
Expected result: (Listof Integer)
 in: (filter values lst1)

I’m not sure that there is any way to inst the call to filter in a way that will make lst2 typecheck, but this is a common idiom, and it would be nice if TR could cope with it.

It is not too hard to write a function of type (All [a] (Listof (Option a)) -> (Listof a)), but the Racket standard library does not currently provide one, so not supporting the (filter values ...) idiom would force a user to actually write such a function themselves to get this behavior. As far as I can tell, there isn’t a particularly good workaround.

Start with the typed/racket reproducer in the issue and inspect how filter and the values procedure are typed and analyzed by the type checker. Done means the example typechecks with lst2 inferred as (Listof Integer), with coverage for this behavior in the relevant tests.