I’ve just published the `data-elevator`

package on hackage: data-elevator: Coerce between unlifted boxed and lifted types.

It’s the result of a joint brainstorming session at ZuriHac with Andreas Klebinger, Krzysztof Gogolewski and Matthew Craven (remotely). See this thread for details: Pre-proposal: Provide `unsafeForce :: forall (a :: Type) (b :: UnliftedType). a -> b` in Unsafe.Coerce (#21693) · Issues · Glasgow Haskell Compiler / GHC · GitLab

You can use its `Strict :: LiftedType -> UnliftedType`

and `Lazy :: LiftedType -> UnliftedType`

newtypes (!) to turn any lifted type into an unlifted (boxed) type like `Array#`

and vice versa.

Example:

```
let f :: (a :: UnliftedType) -> Int
f _ = 42
in f (Strict (error "boom" :: Int))
```

This will error out with `"boom"`

. While the following

```
let f :: a -> Int
f _ = 42
in f (Lazy (error "boom" :: Array# Int))
```

will *not* error and return 42 instead. (Do note though that unlifted primitives like `Array#`

currently don’t have enter code and any eval of `Lazy`

will crash, Make everything BoxedRep have enter code (#21792) · Issues · Glasgow Haskell Compiler / GHC · GitLab).

I added a `Coercible`

-like type, `LevitySubsumption`

that allows to coerce some functions along the subkinding relationship `Unlifted <: Lifted`

lifted over `BoxedRep`

, `TYPE`

and then `(->)`

. The only axioms are `Strict a <: a`

and `a <: Lazy a`

. With that in place, I can do call-by-value on any existing lazy function:

```
even :: Int -> Bool
strictEven :: Strict Int -> Bool
strictEven = levCoerce @(Int -> Bool) @(Strict Int -> Bool) even
even 42
strictEven (Strict 42)
```

See also Data.Elevator. It’s pretty interesting; constructing a coercion like that is very much what I would like GHC to do by itself one day, without any visible trace of `levCoerce`

if possible (inferrable).