[racket] TR disappearing types?

On Wed, Feb 22, 2012 at 3:51 PM, Neil Toronto <neil.toronto at gmail.com> wrote:
> The following program types without trouble:
>
>
> #lang typed/racket
>
> (struct: (a) Foo ())
>
> (: make-foo (All (a) (a -> (Foo a))))
> (define (make-foo x)
>  (Foo))
>
> (ann (make-foo 1) : (Foo String))
>
> It doesn't seem like it should, though. If this is the right behavior, is
> there a way to get a `Foo' parameterized on type `a' without actually
> storing the value? I'm trying to use TR to check programs that can't
> actually be run (i.e. written in a lambda calculus extended with uncountable
> sets).

What you're seeing is that TR currently implements type instantiation
with substitution, and so encodings like 'phantom types' don't work.
This isn't a soundness hole, but it's something that I'm willing to
change if there are programs you'd like to write that you can't.  Can
you give a more complete example?
-- 
sam th
samth at ccs.neu.edu