Skip to content

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

  1. Whether the definition of unsafeForce is safe (provided that unsafeForce is used only to convert from Unlifted to Lifted of the same polymorphic data type). I think so, but I want to double-check.
  2. Perhaps we can make the type of force work, then we don't need the unsafe prefix.
  3. Can you think of other more type-safe or more efficient designs?
Edited by Ben Gamari
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information