diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,5 @@
+# Revision history for data-elevator
+
+## 0.1.0.0 -- 2022-07-31
+
+* First version
diff --git a/data-elevator.cabal b/data-elevator.cabal
new file mode 100644
--- /dev/null
+++ b/data-elevator.cabal
@@ -0,0 +1,61 @@
+cabal-version:      2.4
+name:               data-elevator
+version:            0.1.0.0
+
+tested-with: GHC ==9.2.3 || ==9.4.1
+
+-- A short (one-line) description of the package.
+synopsis: Coerce between unlifted boxed and lifted types.
+
+-- A longer description of the package.
+description: Near zero-cost coercions between unlifted boxed and lifted types.
+             There are 3 main ingredients to this library:
+             (1) a newtype @Strict :: LiftedType -> UnliftedType@,
+             (2) a newtype @Lazy :: UnliftedType -> LiftedType@, and
+             (3) a coercion function @levCoerce@ to coerce existing functions
+                 into accepting @Strict@ wrapper.
+
+-- The license under which the package is released.
+license: MIT
+
+-- The package author(s).
+author: Sebastian Graf
+
+-- 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
+
+bug-reports: https://github.com/sgraf812/data-elevator/issues
+
+source-repository head
+  type: git
+  location: https://github.com/sgraf812/data-elevator
+
+library
+    exposed-modules:  Data.Elevator
+                      Data.Elevator.Internal
+
+    -- Modules included in this library but not exported.
+    -- other-modules:
+
+    -- LANGUAGE extensions used by modules in this package.
+    -- other-extensions:
+    build-depends:    base ^>=4.16
+    hs-source-dirs:   src
+    default-language: Haskell2010
+
+test-suite data-elevator-test
+    default-language: Haskell2010
+    type:             exitcode-stdio-1.0
+
+    -- Directories containing source files.
+    -- hs-source-dirs:
+    main-is:          Main.hs
+    hs-source-dirs:   test
+    build-depends:    base ^>=4.16
+                    , data-elevator
+                    , hspec
diff --git a/src/Data/Elevator.hs b/src/Data/Elevator.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Elevator.hs
@@ -0,0 +1,20 @@
+-- | Near zero-cost coercions between lifted and boxed unlifted types.
+--
+-- Turn any lifted type into an unlifted boxed type with 'Strict', eagerly
+-- forcing any wrapped computation in the syntactic binding context.
+--
+-- Turn any unlifted boxed type into a lifted type with 'Lazy', suspending any
+-- wrapped computation until the 'Lazy' is matched upon.
+--
+-- Re-use existing code by coercing functions that can be generalised according
+-- to the levity polymorphism subkinding law @Unlifted <: Lifted@ with
+-- 'levCoerce'.
+
+module Data.Elevator
+  ( UnliftedType, LiftedType
+  , Strict(Strict), Lazy(Lazy)
+  , levCoerce, LevitySubsumption(..)
+  ) where
+
+import Data.Elevator.Internal
+import GHC.Exts
diff --git a/src/Data/Elevator/Internal.hs b/src/Data/Elevator/Internal.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Elevator/Internal.hs
@@ -0,0 +1,217 @@
+{-# LANGUAGE BangPatterns          #-}
+{-# LANGUAGE DataKinds             #-}
+{-# LANGUAGE PolyKinds             #-}
+{-# LANGUAGE KindSignatures        #-}
+{-# LANGUAGE TypeApplications      #-}
+{-# LANGUAGE RoleAnnotations       #-}
+{-# LANGUAGE MagicHash             #-}
+{-# LANGUAGE PatternSynonyms       #-}
+{-# LANGUAGE ViewPatterns          #-}
+{-# LANGUAGE GADTs                 #-}
+{-# LANGUAGE UnliftedNewtypes      #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE ExplicitForAll        #-}
+{-# LANGUAGE ScopedTypeVariables   #-}
+{-# LANGUAGE InstanceSigs          #-}
+
+-- | This module doesn't respect the PVP!
+-- Breaking changes may happen at any minor version (^>= *.*.m.*)
+
+module Data.Elevator.Internal where
+
+import GHC.Exts
+import Data.Kind
+import Unsafe.Coerce
+
+-- | The kind of boxed, lifted types, for example @[Int]@ or any other
+-- user-defined data type.
+type LiftedType = Type
+
+type U = UnliftedType
+type L = LiftedType
+
+type role Strict representational
+
+-- | Turn a lifted data type into an unlifted one.
+-- Unlifted data types enjoy a call-by-value calling convention. E.g.,
+--
+-- > let f :: (a :: UnliftedType) -> Int
+-- >     f _ = 42
+-- > in f (Strict (error "boom" :: Int))
+--
+-- Will error out with @"boom"@.
+--
+-- Note however that most function definitions don't take argument types of kind
+-- 'UnliftedType'. Use 'levCoerce' to work around that.
+newtype Strict (a :: LiftedType) where
+  Strict_ :: Any @UnliftedType -> Strict a
+
+toStrict# :: a -> Strict a
+toStrict# = unsafeCoerce id
+
+fromStrict# :: Strict a -> a
+fromStrict# = unsafeCoerce id
+
+pattern Strict :: a -> Strict a
+pattern Strict x <- (fromStrict# -> x) where
+  Strict x = toStrict# x
+{-# INLINE Strict #-}
+
+
+type role Lazy representational
+
+-- | Turn an unlifted boxed type into a lifted one.
+-- @Lazy a@ then enjoys a call-by-name calling convention. E.g.,
+--
+-- > let f :: a -> Int
+-- >     f _ = 42
+-- > in f (Lazy (error "boom" :: Array# Int))
+--
+-- Will evaluate to @42@ and not error.
+newtype Lazy (a :: UnliftedType) where
+  Lazy_ :: Any @LiftedType -> Lazy a
+
+toLazy# :: a -> Lazy a
+toLazy# = unsafeCoerce id
+
+fromLazy# :: Lazy a -> a
+fromLazy# = unsafeCoerce id
+
+pattern Lazy :: a -> Lazy a
+pattern Lazy x <- (fromLazy# -> x) where
+  Lazy x = toLazy# x
+{-# INLINE Lazy #-}
+
+
+-- | Re-use existing code taking arguments lazily to take arguments 'Strict'ly
+-- by coercing with 'levCoerce'.Example: 'even' can be
+-- re-used on @Strict Int@:
+--
+-- >>> levCoerce @(Int -> Bool) @(Strict Int -> Bool) even (Strict 42)
+-- True
+--
+-- More generally, any type of kind 'UnliftedType' can act as a (\"is-a\") type
+-- of kind 'LiftedType'. This levity polymorphism subkinding axiom
+-- @Unlifted <: Lifted@ is encoded in 'LevitySubsumption' and is lifted to
+-- useful instances for 'Strict', 'Lazy' and '(->)'. Example with covariance in
+-- the result type:
+--
+-- >>> levCoerce @(Int -> Strict Bool) @(Strict Int -> Bool) (\x -> Strict (even x)) (Strict 42)
+-- True
+--
+-- A function from @Int@ to @Strict Bool@ can be called on a @Strict Int@ (e.g.,
+-- the precondition strengthened) and the result can be coerced to @Bool@ (e.g.,
+-- the postcondition weakened).
+--
+-- You can also keep on coercing in negative position of the function arrow,
+-- with the variance following polarity:
+--
+-- > levCoerce @((Strict Int -> Int) -> Int)
+-- >           @((Int -> Strict Int) -> Int)
+-- >           (\f -> f (Strict 42))
+-- >           (\x -> Strict x)
+--
+levCoerce :: LevitySubsumption a b => a -> b
+levCoerce = levCoerce#
+
+-- | Similar to 'Coercible', this type class models a subkinding relationship
+-- between two types. The instances lift the @Unlifted <: Lifted@ sub-kinding
+-- relationship to 'TYPE', 'Strict', 'Lazy' and then over function types.
+--
+-- Like for 'Coercible', the instances of this type class should ultimately be
+-- compiler-generated.
+class LevitySubsumption (a :: TYPE (BoxedRep l)) (b :: TYPE (BoxedRep r)) where
+  levCoerce# :: a -> b
+
+instance {-# OVERLAPPABLE #-} LevitySubsumption (a::LiftedType) a where
+  levCoerce# x = x
+
+instance {-# OVERLAPPABLE #-} LevitySubsumption (a::UnliftedType) a where
+  levCoerce# x = x
+
+instance {-# OVERLAPPING #-} LevitySubsumption (Strict a) a where
+  levCoerce# (Strict a) = a
+
+instance {-# OVERLAPPING #-} LevitySubsumption a (Lazy a) where
+  levCoerce# a = Lazy a
+
+instance {-# OVERLAPPING #-} (LevitySubsumption a2 a1, LevitySubsumption b1 b2) => LevitySubsumption ((a1::L) -> (b1::L)) ((a2::L) -> (b2::L)) where
+  -- Specification:
+  -- > levCoerce# f x = levCoerce# (f (levCoerce# x :: a1))
+  levCoerce# f x = unsafeCoerce# f x
+
+instance {-# OVERLAPPING #-} (LevitySubsumption a2 a1, LevitySubsumption b1 b2) => LevitySubsumption ((a1::L) -> (b1::L)) ((a2::L) -> (b2::U)) where
+  -- Specification:
+  -- > levCoerce# f x = levCoerce# (f (levCoerce# x :: a1))
+  levCoerce# f x = unsafeCoerce# f x
+
+instance {-# OVERLAPPING #-} (LevitySubsumption a2 a1, LevitySubsumption b1 b2) => LevitySubsumption ((a1::L) -> (b1::L)) ((a2::U) -> (b2::L)) where
+  -- Specification:
+  -- > levCoerce# f x = levCoerce# (f (levCoerce# x :: a1))
+  levCoerce# f x = unsafeCoerce# f x
+
+instance {-# OVERLAPPING #-} (LevitySubsumption a2 a1, LevitySubsumption b1 b2) => LevitySubsumption ((a1::L) -> (b1::L)) ((a2::U) -> (b2::U)) where
+  -- Specification:
+  -- > levCoerce# f x = levCoerce# (f (levCoerce# x :: a1))
+  levCoerce# f x = unsafeCoerce# f x
+
+instance {-# OVERLAPPING #-} (LevitySubsumption a2 a1, LevitySubsumption b1 b2) => LevitySubsumption ((a1::L) -> (b1::U)) ((a2::L) -> (b2::L)) where
+  -- Specification:
+  -- > levCoerce# f x = levCoerce# (f (levCoerce# x :: a1))
+  levCoerce# f x = unsafeCoerce# f x
+
+instance {-# OVERLAPPING #-} (LevitySubsumption a2 a1, LevitySubsumption b1 b2) => LevitySubsumption ((a1::L) -> (b1::U)) ((a2::L) -> (b2::U)) where
+  -- Specification:
+  -- > levCoerce# f x = levCoerce# (f (levCoerce# x :: a1))
+  levCoerce# f x = unsafeCoerce# f x
+
+instance {-# OVERLAPPING #-} (LevitySubsumption a2 a1, LevitySubsumption b1 b2) => LevitySubsumption ((a1::L) -> (b1::U)) ((a2::U) -> (b2::L)) where
+  -- Specification:
+  -- > levCoerce# f x = levCoerce# (f (levCoerce# x :: a1))
+  levCoerce# f x = unsafeCoerce# f x
+
+instance {-# OVERLAPPING #-} (LevitySubsumption a2 a1, LevitySubsumption b1 b2) => LevitySubsumption ((a1::L) -> (b1::U)) ((a2::U) -> (b2::U)) where
+  -- Specification:
+  -- > levCoerce# f x = levCoerce# (f (levCoerce# x :: a1))
+  levCoerce# f x = unsafeCoerce# f x
+
+instance {-# OVERLAPPING #-} (LevitySubsumption a2 a1, LevitySubsumption b1 b2) => LevitySubsumption ((a1::U) -> (b1::L)) ((a2::L) -> (b2::L)) where
+  -- Specification:
+  -- > levCoerce# f x = levCoerce# (f (levCoerce# x :: a1))
+  levCoerce# f x = unsafeCoerce# f x
+
+instance {-# OVERLAPPING #-} (LevitySubsumption a2 a1, LevitySubsumption b1 b2) => LevitySubsumption ((a1::U) -> (b1::L)) ((a2::L) -> (b2::U)) where
+  -- Specification:
+  -- > levCoerce# f x = levCoerce# (f (levCoerce# x :: a1))
+  levCoerce# f x = unsafeCoerce# f x
+
+instance {-# OVERLAPPING #-} (LevitySubsumption a2 a1, LevitySubsumption b1 b2) => LevitySubsumption ((a1::U) -> (b1::L)) ((a2::U) -> (b2::L)) where
+  -- Specification:
+  -- > levCoerce# f x = levCoerce# (f (levCoerce# x :: a1))
+  levCoerce# f x = unsafeCoerce# f x
+
+instance {-# OVERLAPPING #-} (LevitySubsumption a2 a1, LevitySubsumption b1 b2) => LevitySubsumption ((a1::U) -> (b1::L)) ((a2::U) -> (b2::U)) where
+  -- Specification:
+  -- > levCoerce# f x = levCoerce# (f (levCoerce# x :: a1))
+  levCoerce# f x = unsafeCoerce# f x
+
+instance {-# OVERLAPPING #-} (LevitySubsumption a2 a1, LevitySubsumption b1 b2) => LevitySubsumption ((a1::U) -> (b1::U)) ((a2::L) -> (b2::L)) where
+  -- Specification:
+  -- > levCoerce# f x = levCoerce# (f (levCoerce# x :: a1))
+  levCoerce# f x = unsafeCoerce# f x
+
+instance {-# OVERLAPPING #-} (LevitySubsumption a2 a1, LevitySubsumption b1 b2) => LevitySubsumption ((a1::U) -> (b1::U)) ((a2::L) -> (b2::U)) where
+  -- Specification:
+  -- > levCoerce# f x = levCoerce# (f (levCoerce# x :: a1))
+  levCoerce# f x = unsafeCoerce# f x
+
+instance {-# OVERLAPPING #-} (LevitySubsumption a2 a1, LevitySubsumption b1 b2) => LevitySubsumption ((a1::U) -> (b1::U)) ((a2::U) -> (b2::L)) where
+  -- Specification:
+  -- > levCoerce# f x = levCoerce# (f (levCoerce# x :: a1))
+  levCoerce# f x = unsafeCoerce# f x
+
+instance {-# OVERLAPPING #-} (LevitySubsumption a2 a1, LevitySubsumption b1 b2) => LevitySubsumption ((a1::U) -> (b1::U)) ((a2::U) -> (b2::U)) where
+  -- Specification:
+  -- > levCoerce# f x = levCoerce# (f (levCoerce# x :: a1))
+  levCoerce# f x = unsafeCoerce# f x
diff --git a/test/Main.hs b/test/Main.hs
new file mode 100644
--- /dev/null
+++ b/test/Main.hs
@@ -0,0 +1,42 @@
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE MagicHash        #-}
+
+module Main where
+
+import Data.Elevator.Internal
+import Test.Hspec
+import Control.Exception (evaluate, SomeException (SomeException))
+import GHC.Exts
+
+main :: IO ()
+main = hspec $ do
+  describe "Strict" $ do
+    it "strict" $ do
+      evaluate
+        (let a = Strict (error "boom" :: Int)
+             konst :: a -> Strict b -> a
+             konst x y = x
+        in konst 42 a)
+        `shouldThrow` \(SomeException e) -> True
+
+  describe "Lazy" $ do
+    it "lazy" $ do
+      (let a = Lazy (error "boom" :: Array# Int)
+           konst :: a -> Lazy b -> a
+           konst x y = x
+       in konst 42 a)
+      `shouldBe` 42
+
+  describe "levCoerce" $ do
+    describe "Refl" $ do
+      it "Int ~ Int" $ do
+        levCoerce @Int @Int 42 `shouldBe` (42 :: Int)
+      it "Strict Int ~ Strict Int" $ do
+        case levCoerce# @_ @_ @(Strict Int) @(Strict Int) (Strict 42) of Strict x -> x  `shouldBe` (42 :: Int)
+    describe "->" $ do
+      it "even" $ do
+        levCoerce @(Int -> Bool) @(Strict Int -> Bool) even (Strict 42) `shouldBe` True
+      it "co,contra: Int -> Strict Int ~ Int -> Strict Int" $ do
+        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)