[racket-dev] Unfolding twice?

On Fri, Aug 10, 2012 at 12:33 PM, Neil Toronto <neil.toronto at gmail.com> wrote:
> Using typed `flatten' takes too much manual instantiation. In the following
> program, the first three uses fail to typecheck; the last passes.

This looks like a bug ...

> 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.

But this diagnosis is not right.  Recursive types in TR are equal to
their unfoldings; there should never be a need to explicitly unfold
more than once, either in the typechecker or manually.  I'll look into
what's going on here.
-- 
sam th
samth at ccs.neu.edu