[racket-dev] Unfolding twice?

From: Sam Tobin-Hochstadt (samth at ccs.neu.edu)
Date: Fri Aug 10 12:41:11 EDT 2012

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

Posted on the dev mailing list.