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

I have just filed this as a bug report.  Typed Racket appears to
process nested annotations in the wrong order.

Welcome to Racket v5.0.99.5.
> (ann (ann 5 Real) Integer)
- : Real
5
> (ann (ann 5 Integer) Real)
stdin::37: Type Checker: Expected Integer, but got Real in: 5

Carl Eastlund

On Wed, Dec 22, 2010 at 3:42 PM, Carl Eastlund <cce at ccs.neu.edu> wrote:
> 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).  For instance:
>
>> (: f ((Listof Symbol) -> (List Symbol Symbol)))
>> (define (f x) x)
> stdin::124: Type Checker: Expected (List Symbol Symbol), but got
> (Listof Symbol) in: x
>
> Carl Eastlund
>
> On Wed, Dec 22, 2010 at 3:33 PM, Neil Van Dyke <neil at neilvandyke.org> wrote:
>> 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/