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

Work around this with explicit let or other intermediate bindings:

Welcome to Racket v5.0.99.5.
> (let: ([x : Integer 5]) (ann x Real))
- : Real
5
> (let: ([x : Real 5]) (ann x Integer))
stdin::64: Type Checker: Expected Integer, but got Real in: x

Carl Eastlund

On Wed, Dec 22, 2010 at 3:54 PM, Carl Eastlund <cce at ccs.neu.edu> wrote:
> 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/