Re: Unlifted data types

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