[plt-scheme] Typed-Scheme and car

Hi all,

Just trying this example I got two unexpected error:
#lang typed-scheme

(: x (Listof (Pair Symbol Integer)))
(define x '((one . 1) (two . 2) (three . 3)))

(: y (Listof Symbol))
(define y (map car x))

. typecheck: Expected (Listof (Pair Symbol Integer)), but got (List
Any Any Any) in: (quote ((one . 1) (two . 2) (three . 3)))
. typecheck: Polymorphic function map could not be applied to arguments:
Domain: (a b ... b -> c) (Listof a) (Listof b) ... b
Arguments: (All (a b) (case-lambda ((Pair a b) -> a) ((Listof a) ->
a))) (Listof (Pair Symbol Integer))
Result type: (Listof c)
Expected result: (Listof Symbol)
 in: (map car x)

if I replace x define with:
(define x (list (cons 'one 1) (cons 'two 2) (cons 'three 3)))

the first error disappears but the second remains. The second error
goes away with:
(define y (map (lambda: ((p : (Pair Symbol Integer))) (car p)) x))

But this is MUCH more annoying to write and the program gets much more
verbose and I have to say that after rewriting a couple of 'big'
modules in typed-scheme, the scheme simplicity and elegance starts to
fade. Making typed-scheme support things such as a (map car x) is for
me a big requirement. Currently my code is full of lambda: in maps,
filters, etc for no good reason. I hope that there is work to improve
this in the future. I guess it is possible to make the type inference
mechanism to detect this.

Still, cheers and kudos to Sam and other for the current state of
typed-scheme. It is a very nice language to program in even though its
current state still has some quirks.


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