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 thatAny
has the correct kind. (Coercion between lifted and unlifted types is unsound.) For example, for some @b :: ByteArray#@:unsafeCoerce# b :: (Any :: TYPE ('BoxedRep 'Unlifted))