[racket] Typed Racket: can this recursive typing become polymorphic?

What if A is (Listof Integer)?
Generally a type variable naked in a union is just not going to do what you want. There's no way to keep it disjoint from the other types in the union.

-Ian

----- Original Message -----
From: "Matthew Butterick" <mb at mbtype.com>
To: "users" <users at racket-lang.org>
Sent: Tuesday, February 3, 2015 7:29:47 PM
Subject: [racket] Typed Racket: can this recursive typing become polymorphic?

I'm trying to create a polymorphic type for `flatten` that reflects its usual behavior. 

This monomorphic version works:

#lang typed/racket/base
(require/typed rackunit [check-equal? (Any Any . -> . Any)])
(require/typed racket/list [flatten (All (A) (Rec as (U Integer (Listof as))) -> (Listof Integer))])

(define flatten-integers (inst flatten Integer))
(check-equal? (flatten-integers 1) '(1))
(check-equal? (flatten-integers '(1)) '(1))
(check-equal? (flatten-integers '(1 (2 3) 4)) '(1 2 3 4))
(check-equal? (flatten-integers '(1 (2 3 (4 5)) 6)) '(1 2 3 4 5 6))


But when I try to substitute the polymorphic type `A` for `Integer`, it stops working:

#lang typed/racket/base
(require/typed rackunit [check-equal? (Any Any . -> . Any)])
(require/typed racket/list [flatten (All (A) (Rec as (U A (Listof as))) -> (Listof A))])

(define flatten-integers (inst flatten Integer))
(check-equal? (flatten-integers 1) '(1))
(check-equal? (flatten-integers '(1)) '(1))
(check-equal? (flatten-integers '(1 (2 3) 4)) '(1 2 3 4))
(check-equal? (flatten-integers '(1 (2 3 (4 5)) 6)) '(1 2 3 4 5 6))

> git/racket/racket/collects/racket/contract/private/blame.rkt:143:0: flatten: contract violation; none of the branches of the or/c matched



Is it possible? If so, what am I missing?
____________________
  Racket Users list:
  http://lists.racket-lang.org/users