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

Thanks, I'm relieved if that's a bug.  Although, if it is a bug, it's a 
showstopper for me until fixed, as problems like this exhibit throughout 
some list-processing-intensive code I'm trying to convert to Typed Racket.

Carl Eastlund wrote at 12/22/2010 03:42 PM:
> I believe your intermediate expression there, the one with two
> "ann"otations in it, is a Typed Racket bug.  You should definitely not
> be able to take something with the type (Listof Symbol) and coerce it
> to (List Symbol Symbol).

>> ...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/