Skip to content

Unsafely coercing between Any and unlifted boxed types

The documentation for the Any type family reads:

The type constructor 'Any' is type to which you can unsafely coerce any lifted type, and back. More concretely, for a lifted type @t@ and value @x :: t@, -- @unsafeCoerce (unsafeCoerce x :: Any) :: t@ is equivalent to @x@.

I think the use of the word "lifted" here was accurate correct several years ago but is now implies something stronger than what is true. If I have some x where x :: ByteArray#, I can do this:

let y0 = unsafeCoerce# x :: (Any :: TYPE ('BoxedRep 'Lifted))
    y1 = unsafeCoerce# y0 :: ByteArray#
 in ...

And this ought to be fine. I suggest rewriting the whole thing like to look like this (using code blocks as well to improve the presentation the examples):

The type constructor 'Any' is type to which you can unsafely coerce any boxed type (either lifted or unlifted), and back. More concretely, for a lifted type @t@ and value @x :: t@:

unsafeCoerce (unsafeCoerce x :: Any) :: t
===
x

To cast a boxed unlifted type to Any, type annotations are recommended to make sure that Any has the correct kind. (Coercion between lifted and unlifted types is unsound.) For example, for some @b :: ByteArray#@:

unsafeCoerce# b :: (Any :: TYPE ('BoxedRep 'Unlifted))
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information