# [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