[racket] problem (?) with typed racket
From: Jose A. Ortega Ruiz (jao at gnu.org)
Date: Mon Jul 5 07:19:43 EDT 2010 

Hi,
The following (contrived) typed/racket program doesn't typecheck:
(definestruct: (E) Arrow
([arrow : (E > (Listof E))]))
(: composearrows (All (E) ((Arrow E) (Arrow E) > (Arrow E))))
(define (composearrows a b)
(Arrow (lambda (e) ((Arrowarrow a) (car ((Arrowarrow b) e))))))
The typechecker complains about `composearrows':
Type Checker: Expected E, but got Any in: e
(pointing to the lambda inside `composearrows' above). I can circumvent
the problem giving an explicit type to that lambda:
(define (composearrows a b)
(let: ([cmp : (All (E) ((Arrow E) (Arrow E) > (E > (Listof E))))
(lambda (a b)
(lambda (e) ((Arrowarrow a) (car ((Arrowarrow b) e)))))])
(Arrow (cmp a b))))
but this feels a bit verbose, compared to the original definition above.
(I've tried other combinations using `define:', but the problem is
always unifying all occurences of the type parameter 'E'.)
Is the failure to type check a genuine limitation of the type inference
engine, or is it me expecting too much from type inference in general?
And, is there a more compact way of indicating the type of that lambda?
TIA,
jao