[racket] typed/racket: type of sequence-filter

There's a bug in the type. I have a fix, which I'll push soon.

Details below.

At Fri, 11 Apr 2014 14:17:24 +0100,
Tim Brown wrote:
> A :print-types of sequence-filter shows:
>   > (:print-type sequence-filter)
>   (All (a b)
>   (case->
>    (-> (-> a Any) (Sequenceof a) (Sequenceof b))
>    (-> (-> a Any) (Listof a) (Sequenceof a))))
> 
> Should the type of sequence-filter not be "(a -> Any) (Sequenceof a) ->
> (Sequenceof a)" since the type (and data) of the successful elements of
> the sequence are identical.
> 
> Is there any reason for this particular type declaration of
> sequence-filter?

The type has additional information that is not displayed. Specifically,
the predicate has type `(-> a Any)' with filters that say "if this
function returns a non-false value, then its argument is a `b'". That's
where the `b' comes from.

This makes it possible to do things like:

    (sequence-filter integer? <sequence-of-Any>) -> <sequence-of-Integer>

There has been discussion about displaying filters in types, which would
have made the type less confusing.


> [sequence-filter
>   (-poly (a b)
>   (cl->*
>     ((asym-pred a Univ (-FS (-filter b 0) -top))
>      (-seq a)
>      . -> .
>      (-seq a))
>     ((a . -> . Univ) (-lst a) . -> . (-seq a))))]
>
> [...]
> 
> Lets it behave correctly. Unfortunately, I don't comprehend the description
> of the (asym-pred ...) clause, what it does and how it breaks my typing. So
> could someone look at what's happening here?

The `asym-pred' part adds the filter I mentioned above.

The actual bug is that the seconf clause should be:

  ((a . -> . Univ) (-seq a) . -> . (-seq a))

That is, when the function gets a predicate without filters, it should
accept any kind of sequences, not just lists.

Thanks for the report!

Vincent