Unlifted data types

[Edward Z. Yang]

Yes, I think you are right.  I've restructured the spec so that 'Box'
is an optional extension.

Excerpts from Dan Doel's message of 2015-09-06 13:56:35 -0700:
> On Sat, Sep 5, 2015 at 1:35 PM, Dan Doel <dan.doel at gmail.com> wrote:
> > Also, the constructor isn't exactly relevant, so much as whether the
> > unlifted error occurs inside the definition of a lifted thing.
> 
> So, in light of this, `Box` is not necessary to define `suspend`. We
> can simply write:
> 
>     suspend :: Force a -> a
>     suspend (Force x) = x
> 
> and the fact that `a` has kind * means that `suspend undefined` only
> throws an exception if you inspect it.
> 
> `Box` as currently defined (not the previous GADT definition) is novel
> in that it allows you to suspend unlifted types that weren't derived
> from `Force`. And it would probably be useful to have coercions
> between `Box (Force a)` and `a`, and `Force (Box u)` and `u`. But (I
> think) it is not necessary for mediating between `Force a` and `a`.
> 
> -- Dan