[racket] Tricky case of occurrence typing in Typed Racket

Hi everyone,

I am trying to convince Typed Racket that after a run-time check on
some list, its elements are all of a given type. This is just like
occurrence typing based on a predicate, except that my predicate
is more complicated.

My first attempt was this:


   #lang typed/racket

   (struct: foo ())
   (struct: bar ())
   (define-type FooOrBar (U foo bar))

   (: f-bar (-> (Listof bar) Void))
   (define (f-bar xs)
     (void))

   (: f-mixed (-> (Listof FooOrBar) Void))
   (define (f-mixed xs)
     (void))

   (: f (-> (Listof FooOrBar) Void))
   (define (f xs)
     (if (for/and : Boolean ([x xs]) (bar? x))
         (f-bar xs) ; contains only bars
         (f-mixed xs) ; may contain foos as well
         ))

This yields a type error:

   ; /Users/hinsen/projects/racket/foobar.rkt:18:13: Type Checker: type mismatch
   ;   expected: (Listof bar)
   ;   given: (Listof FooOrBar)
   ;   in: xs

After reading section 5 of the Typed Racket Guide, in particular section
5.2 entitled "Filters and Predicates", I thought I could simply define my
own predicate with a type annotation:

   #lang typed/racket

   (struct: foo ())
   (struct: bar ())
   (define-type FooOrBar (U foo bar))

   (: f-bar (-> (Listof bar) Void))
   (define (f-bar xs)
     (void))

   (: f-mixed (-> (Listof FooOrBar) Void))
   (define (f-mixed xs)
     (void))

   (: pure-bars? (-> (Listof FooOrBar) Boolean : (Listof bar)))
   (define (pure-bars? xs)
     (for/and : Boolean ([x xs]) (bar? x)))

   (: f (-> (Listof FooOrBar) Void))
   (define (f xs)
     (if (pure-bars? xs)
         (f-bar xs) ; contains only bars
         (f-mixed xs) ; may contain foos as well
         ))

But this got me only into more trouble - now I don't even understand the
error message any more:

   ; /Users/hinsen/projects/racket/foobar.rkt:17:2: Type Checker: type mismatch;
   ;  mismatch in filter
   ;   expected: (((Listof bar) @ xs) | (! (Listof bar) @ xs))
   ;   given: (Top | Top)
   ;   in: (for/and : Boolean ((x xs)) (bar? x))

Is there a way to do this kind of test?

Konrad.