[racket-dev] Unfolding twice?

Using typed `flatten' takes too much manual instantiation. In the 
following program, the first three uses fail to typecheck; the last passes.

#lang typed/racket

(define-type (Treeof A) (Rec T (U A (Listof T))))

(: flatten (All (A) ((Treeof A) (Any -> Boolean : A) -> (Listof A))))
(define (flatten lst pred?)
   (error 'unimplemented))

(define ws (flatten (sequence->list (in-range -1.4 1.400001 0.2))
                     flonum?))
(define xs ((inst flatten Float)
             (sequence->list (in-range -1.4 1.400001 0.2))
             flonum?))
(define ys (flatten ((inst sequence->list Float)
                      (in-range -1.4 1.400001 0.2))
             flonum?))
(define zs ((inst flatten Float)
             ((inst sequence->list Float)
              (in-range -1.4 1.400001 0.2))
             flonum?))


I think the problem is that TR only unfolds the type of (Treeof A) once. 
If I manually unfold it once; i.e., I change it to this:

   (define-type (Treeof A) (U A (Listof (Rec T (U A (Listof T))))))

then the program passes, because TR now unfolds it twice.

Would it be feasible to have TR, when something with recursive types 
fails to typecheck, calculate an upper bound on the number of unfolds, 
unfold that many times, and try again?

Neil ⊥