Why does `filter` work with higher-order occurrence typing?

Question

On the homepage for Racket, they show this example:

#lang typed/racket
;; Using higher-order occurrence typing
(define-type SrN (U String Number))
(: tog ((Listof SrN) -> String))
(define (tog l)
  (apply string-append (filter string? l)))
(tog (list 5 "hello " 1/2 "world" (sqrt -1)))

I know that with occurrence typing, an expression like (if (string? v) ...) will mark v as having type String in the true branch. This is because the type of string? has a filter on it:

> string?
- : (Any -> Boolean : String)
#<procedure:string?>

So, for "higher-order occurrence typing" to work with the filter function, I would expect the type of filter to say that a filter on the predicate's type gets propagated to the result type. But when I check the type of filter in the REPL, this doesn't show up:

> filter
- : (All (a b) (case-> ((a -> Any) (Listof a) -> (Listof b)) ((a -> Any) (Listof a) -> (Listof a))))
#<procedure:filter>

But this can't be the real type of filter, because there's no constraint on b! I expected something like

(All (a b) (a -> Any : b) (Listof a) -> (Listof b))

tldr: Why does filter appear have an unconstrained type variable in its return type?

EDIT: I am using Racket v6.0

Answer 1

In the Typed Racket Reference it is said:

In some cases, asymmetric type information is useful in filters. For example, the filter function’s first argument is specified with only a positive filter. Example:

> filter
- : (All (a b)
      (case->
       (-> (-> a Any : #:+ b) (Listof a) (Listof b))
       (-> (-> a Any) (Listof a) (Listof a))))
#<procedure:filter>

The use of #:+ indicates that when the function applied to a variable evaluates to a true value, the given type can be assumed for the variable. However, the type-checker gains no information in branches in which the result is #f.

In other words, if you have the following example:

> (filter string? '(symbol 1 2 3 "string"))
- : (Listof String)
'("string")

the system can says that an element of the list '(symbol 1 2 3 "string") is of type String only when string? returns true on it. Only in this case the type of the filter's predicate is propagated.