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

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/