[plt-scheme] Recognizing Listof in typed-scheme

Hi all,

I stumbled upon an issue that can be simplified into:
#lang typed-scheme

(require scheme/match)

(define-struct: foo
  ())

(define-struct: bar
  ())

(define-struct: foo1
  ())
(define-struct: bar1
  ())

(define-struct: foolist
  ((lst : (Listof foo))))

(define-struct: foolist1
  ((lst : (Listof foo1))))

(define-type-alias foobar (U foo bar))

(define-type-alias foobar1 (U foo1 bar1))

(: funct (foobar -> foobar1))
(define (funct f)
  (match f
    ((struct foo _)
     (make-foo1))
    ((struct bar _)
     (make-bar1))))

(: prob (foolist -> foolist1))
(define (prob fl)
  (let ([lst (map (lambda: ((f : foo)) (funct f))
                  (foolist-lst fl))])
    (make-foolist1 lst)))

I get:
typecheck: Wrong function argument type, expected (Listof foo1), got
(Listof foobar1) for argument 1 in: lst

I understand the problem... but I cannot find a workaround. I don't
want to change funct and it doesn't make sense to create another
function with just:
(define (funct1 f) (make-foo1)) with typing (: funct1 (foo -> foo1)).

I tried:
(: every (All (a) ((a -> Boolean) (Listof a) -> Boolean)))
(define (every p xs)
  (or (null? xs)
      (and (p (car xs))
           (every p (cdr xs)))))

(: prob (foolist -> foolist1))
(define (prob fl)
  (let ([lst (map (lambda: ((f : foo)) (funct f))
                  (foolist-lst fl))])
    (if (every foo1? lst)
        (make-foolist1 lst)
        (error 'buh ""))))

But I still get the error...
Then I remembered that I should let typed-scheme know that every is a
predicate for (Listof a), so I changed the typing to:
(: every (All (a) ((a -> Boolean) (Listof a) -> Boolean : (Listof a))))

But now I get an error in match:
match: no matching clause for Unknown Type: #(struct:Error 23 #f)

Have no idea what to do now... :( Any suggestions?

Cheers,

-- 
Paulo Jorge Matos - pocmatos at gmail.com
Webpage: http://www.personal.soton.ac.uk/pocm