[racket] confusion on Typed Racket, pairs, and lists

Carl Eastlund wrote at 12/22/2010 03:06 PM:
> So each time you apply cons, if you don't want a Listof type you have to "convince" it to build something else.  Do this by either annotating each step, or binding cons with a simpler type.
>   

Thanks for the explanation.  I found that annotating each step in the 
building of lists with "cons" works, but I was a surprised that was 
necessary.

More importantly, I don't understand why the following works without 
signaling an error...

 > (list 'a 'b)
- : (List 'a 'b)
(a b)
 > (ann (list 'a 'b) (Listof Symbol))
- : (Listof Symbol)
(a b)
 > (ann (ann (list 'a 'b) (Listof Symbol)) (List Symbol Symbol))
- : (Listof Symbol)
(a b)
 > (ann (list 'a 'b) (List Symbol Symbol))
- : (List Symbol Symbol)
(a b)

...yet the following does get errors when trying to do the same coercion 
from "(Listof Symbol)" to "(List Symbol Symbol)":

 > (cons 'a (cons 'b '()))
- : (Listof (U 'a 'b))
(a b)
 > (ann (cons 'a (cons 'b '())) (Listof Symbol))
- : (Listof Symbol)
(a b)
 > (ann (cons 'a (cons 'b '())) (List Symbol Symbol))
. . Type Checker: Polymorphic function cons could not be applied to 
arguments:
Types: a (Listof a) -> (Listof a)
       a b -> (Pairof a b)
Arguments: 'a (Listof 'b)
Expected result: (List Symbol Symbol)
 in: (cons (quote a) (cons (quote b) (quote ())))
 > (ann (ann (cons 'a (cons 'b '())) (Listof Symbol)) (List Symbol Symbol))
. . Type Checker: Polymorphic function cons could not be applied to 
arguments:
Types: a (Listof a) -> (Listof a)
       a b -> (Pairof a b)
Arguments: 'a (Listof 'b)
Expected result: (List Symbol Symbol)
 in: (cons (quote a) (cons (quote b) (quote ())))


-- 
http://www.neilvandyke.org/