diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,5 +1,12 @@
 # Revision history for data-elevator
 
+## 0.2 -- 2024-09-16
+
+* Fix issue #4, which makes `toStrict#` and `fromLazy#` NOINLINE.
+  We now have rewrite rules to cancel away, e.g., `fromStrict# . toStrict# = id`.
+  This is expected to be a bit more brittle performance-wise compared to the
+  0.1.*, but it fixes a major soundness bug (#4).
+
 ## 0.1.0.2 -- 2024-08-02
 
 * Added support for GHC versions 9.6, 9.8, and 9.10
diff --git a/data-elevator.cabal b/data-elevator.cabal
--- a/data-elevator.cabal
+++ b/data-elevator.cabal
@@ -1,6 +1,6 @@
 cabal-version:      2.4
 name:               data-elevator
-version:            0.1.0.2
+version:            0.2
 
 tested-with: GHC ==9.2.8 || ==9.4.8 || ==9.6.6 || ==9.8.2 || ==9.10.1
 
@@ -24,10 +24,8 @@
 -- An email address to which users can send suggestions, bug reports, and patches.
 maintainer: sgraf1337@gmail.com
 
--- A copyright notice.
-copyright: 2022
 category: Data
-extra-source-files: CHANGELOG.md
+extra-doc-files: CHANGELOG.md
 
 bug-reports: https://github.com/sgraf812/data-elevator/issues
 
@@ -56,6 +54,9 @@
     -- hs-source-dirs:
     main-is:          Main.hs
     hs-source-dirs:   test
+    other-modules:    Issue4
     build-depends:    base >=4.16 && <4.21
                     , data-elevator
+                    , primitive
                     , hspec
+                    , inspection-testing
diff --git a/src/Data/Elevator/Internal.hs b/src/Data/Elevator/Internal.hs
--- a/src/Data/Elevator/Internal.hs
+++ b/src/Data/Elevator/Internal.hs
@@ -49,9 +49,13 @@
 
 toStrict# :: a -> Strict a
 toStrict# = unsafeCoerce id
+{-# NOINLINE toStrict# #-} -- See Note [NOINLINE toStrict#/fromLazy#]
+{-# RULES "fromStrict#.toStrict#" forall x. fromStrict# (toStrict# x) = x #-}
+{-# RULES "toLazy#.toStrict#" forall x. toLazy# (toStrict# x) = unsafeCoerce id x #-}
 
 fromStrict# :: Strict a -> a
 fromStrict# = unsafeCoerce id
+{-# INLINE[0] fromStrict# #-} -- See Note [NOINLINE toStrict#/fromLazy#]
 
 pattern Strict :: a -> Strict a
 pattern Strict x <- (fromStrict# -> x) where
@@ -75,9 +79,13 @@
 
 toLazy# :: a -> Lazy a
 toLazy# = unsafeCoerce id
+{-# INLINE[0] toLazy# #-} -- See Note [NOINLINE toStrict#/fromLazy#]
 
 fromLazy# :: Lazy a -> a
 fromLazy# = unsafeCoerce id
+{-# NOINLINE fromLazy# #-} -- See Note [NOINLINE toStrict#/fromLazy#]
+{-# RULES "toLazy#.fromLazy#" forall x. toLazy# (fromLazy# x) = x #-}
+{-# RULES "fromStrict#.fromLazy#" forall x. fromStrict# (fromLazy# x) = unsafeCoerce id x #-}
 
 pattern Lazy :: a -> Lazy a
 pattern Lazy x <- (fromLazy# -> x) where
@@ -217,3 +225,38 @@
   -- Specification:
   -- > levCoerce# f x = levCoerce# (f (levCoerce# x :: a1))
   levCoerce# f x = unsafeCoerce# f x
+
+{- Note [NOINLINE toStrict#/fromLazy#]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+It is important GHC does not regard the expression `Strict x` as trivial.
+This is because CorePrep will not case-bind `Strict x` in `f (Strict x)` when it
+is trivial, in which case we do not get proper call-by-value for the call to `f`.
+
+However, if we inline the Strict and the toStrict#, what we get is
+`f (x |> co)`, and `x |> co` is trivial.
+So, sadly we need to mark `toStrict#` as NOINLINE; in which case we get
+`f (toStrict# x)`, where `toStrict# x` is non-trivial and thus properly
+case-bound by CorePrep: `case toStrict# x of x' { __DEFAULT -> f x' }`.
+
+But this means that expressions such as `toLazy# (toStrict# x)` are no longer
+optimised to `x`. We fix that by introducing the rewrite rules
+
+  forall x. fromStrict# (toStrict# x) = x
+  forall x. toLazy# (toStrict# x) = unsafeCoerce id x -- will desugar to x |> co
+
+Thus we keep the zero-cost promise.
+
+This applies to `fromLazy#` as well. Note the following desugaring
+
+  case x of Lazy y -> f y
+  ==> {INLINE, including `fromLazy#`, CorePrep}
+  f (x |> co)
+
+Note the absence of a seq on `x`. If we do not inline `fromLazy#`, we get
+
+  f (fromLazy# x)
+  ==> {CorePrep}
+  case fromLazy# x of y { __DEFAULT -> f y }
+
+Much better. We need similar rewrite rules, however.
+-}
diff --git a/test/Issue4.hs b/test/Issue4.hs
new file mode 100644
--- /dev/null
+++ b/test/Issue4.hs
@@ -0,0 +1,59 @@
+{-# OPTIONS_GHC -O2              #-}
+{-# LANGUAGE MagicHash           #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications    #-}
+{-# LANGUAGE UnboxedTuples       #-}
+module Issue4 (
+    StrictArray,
+    primArrayToStrictArray,
+    indexStrictArray,
+    sizeofStrictArray,
+) where
+
+import           Data.Elevator (Strict (Strict))
+import qualified Data.Primitive as P
+import qualified GHC.Exts as GHC
+import           GHC.Exts ((+#))
+import           GHC.ST (ST(ST), runST)
+
+data StrictArray a = StrictArray !(GHC.Array# (Strict a))
+
+primArrayToStrictArray :: forall a. P.Array a -> StrictArray a
+primArrayToStrictArray (P.Array a) =
+    runST $ ST $ \s0 ->
+    case GHC.newArray# (GHC.sizeofArray# a) (Strict (P.indexArray (P.Array a) 0)) s0 of
+      (# s1, a#  #) ->
+        case go a# 0# s1 of
+          s2 -> case GHC.unsafeFreezeArray# a# s2 of
+                  (# s3, a'# #) -> (# s3, StrictArray a'# #)
+  where
+    go :: forall s.
+          GHC.MutableArray# s (Strict a)
+       -> GHC.Int#
+       -> GHC.State# s
+       -> GHC.State# s
+    go a# i# s =
+      case i# GHC.<# GHC.sizeofArray# a of
+        1# ->
+          case GHC.indexArray# a i# of
+            (# x #) ->
+              -- We have to use seq# here to force the array element to WHNF
+              -- before putting it into the strict array. This should not be
+              -- necessary. https://github.com/sgraf812/data-elevator/issues/4
+{-              case GHC.seq# x s of
+                (# s', x' #) ->
+-}
+                  case GHC.writeArray# a# i# (Strict x) s of
+                    s' -> go a# (i# +# 1#) s'
+        _  -> s
+
+{-# INLINE indexStrictArray #-}
+indexStrictArray :: StrictArray a -> Int -> a
+indexStrictArray (StrictArray a#) (GHC.I# i#) =
+    case GHC.indexArray# a# i# of
+      (# Strict x #) -> x
+
+{-# INLINE sizeofStrictArray #-}
+sizeofStrictArray :: StrictArray a -> Int
+sizeofStrictArray (StrictArray a#) =
+    GHC.I# (GHC.sizeofArray# a#)
diff --git a/test/Main.hs b/test/Main.hs
--- a/test/Main.hs
+++ b/test/Main.hs
@@ -1,12 +1,21 @@
+{-# OPTIONS_GHC -fplugin=Test.Inspection.Plugin #-}
+
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE MagicHash        #-}
+{-# LANGUAGE UnboxedTuples    #-}
+{-# LANGUAGE TemplateHaskell  #-}
 
 module Main where
 
 import Data.Elevator.Internal
 import Test.Hspec
+import Test.Inspection
 import Control.Exception (evaluate, SomeException (SomeException))
 import GHC.Exts
+import GHC.IO
+import Data.IORef
+import qualified Data.Primitive as P
+import qualified Issue4
 
 main :: IO ()
 main = hspec $ do
@@ -40,3 +49,26 @@
         levCoerce @(Int -> Strict Int) @(Strict Int -> Int) (\x -> Strict (x+1)) (Strict 42) `shouldBe` (43 :: Int)
       it "rank2 co: (Int -> Int) -> Int ~ (Strict Int -> Int) -> Int" $ do
         levCoerce @((Strict Int -> Int) -> Int) @((Int -> Strict Int) -> Int) (\f -> f (Strict 42)) (\x -> Strict x) `shouldBe` (42 :: Int)
+
+  describe "Issue 4" $ do
+    it "should not crash" $ do
+      let arr = P.createArray 5 (even (sum [0..1000]) :: Bool) (\_arr -> return ())
+      let sarr = Issue4.primArrayToStrictArray arr
+      Issue4.indexStrictArray sarr 3 `shouldBe` True
+
+from_to_strict :: Bool -> Bool
+from_to_strict x = fromStrict# (toStrict# x)
+
+from_to_strict2 :: Bool -> Bool
+from_to_strict2 x = case Strict x of Strict x -> x
+
+to_from_lazy :: Lazy a -> Lazy a
+to_from_lazy x = toLazy# (fromLazy# x)
+
+to_from_lazy2 :: Lazy a -> Lazy a
+to_from_lazy2 (Lazy x) = Lazy x
+
+inspect $ 'from_to_strict `doesNotUse` 'toStrict#
+inspect $ ('from_to_strict2 `doesNotUse` 'toStrict#) { expectFail = True } -- https://gitlab.haskell.org/ghc/ghc/-/issues/25261
+inspect $ 'to_from_lazy `doesNotUse` 'fromLazy#
+inspect $ ('to_from_lazy2 `doesNotUse` 'fromLazy#) { expectFail = True } -- https://gitlab.haskell.org/ghc/ghc/-/issues/25261