Pre-proposal: Provide `unsafeForce :: forall (a :: Type) (b :: UnliftedType). a -> b` in Unsafe.Coerce
Consider
data Tree where
Leaf :: !Word -> Tree
Bin :: !Tree -> !Tree -> Tree
type Set = Tree
Imagine maintaining a container library where this is the main data structure for a Set
-like data type.
With 9.2, we might reasonably want to make use of -XUnliftedDatatypes to save tag checks in traversals over Tree
.
But all our clients still expect that Tree
is lifted! If we blindly switch to UnliftedType
, most existing use sites will break.
So instead we might define Tree
as
type Tree :: forall l. TYPE (BoxedRep l)
data Tree where
Leaf :: !Word -> Tree @l
Bin :: Tree @Unlifted -> Tree @Unlifted -> Tree @l
type Set = Tree @Lifted
But now we need an efficient way to convert a Tree @Lifted
to Tree @Unlifted
to call our internal worker functions without duplicating them. #21617 (comment 435216) shows that we are sorely lacking in that regard, making internal use of unlifted datatypes infeasible.
So I propose to add an efficient conversion function (working name force
) from Tree @Lifted
to Tree @Unlifted
which lowers to just \x -> case x of x' { __DEFAULT -> x'}
in STG/use of call-by-value in CoreToStg.
Since we drop all kinds of seq
s in Core if we can prove that x
will be evaluated later on anyway, it's important that Core doesn't see the definition.
(In a far future with #19530 I imagine that case x of x' { __DEFAULT -> x' }
will refine the type of x'
to its unlifted variant and then mindelessly dropping seqs would become a kind error. But we don't live in that future.)
Unfortunately, I'm having a hard time coming up with an accurately-typed definition of force
:
force :: forall (t :: forall l. TYPE (BoxedRep l)). t @Lifted -> t @Unlifted
But I don't think that works because Levity often is the first parameter of the levity polymorphic data type. Without type lambdas, use of force#
would be unbearable.
So instead I propose the following, (unsafe) variant of unsafeCoerce
:
unsafeForce :: forall (a :: Type) (b :: UnliftedType). a -> b
-- this would be a suitable implementation in Core if we can guarantee taggedness of a:
unsafeForce = unsafeCoerce (\(!a) -> lazy a)
We could either provide this library function if we deem its implementation safe and/or back it by a primop unsafeForce#
that we lower in CoreToStg.
What do you think? I wonder
- Whether the definition of
unsafeForce
is safe (provided thatunsafeForce
is used only to convert from Unlifted to Lifted of the same polymorphic data type). I think so, but I want to double-check. - Perhaps we can make the type of
force
work, then we don't need theunsafe
prefix. - Can you think of other more type-safe or more efficient designs?