diff --git a/.gitignore b/.gitignore
index 2a3fcfb..f3ea3d0 100644
--- a/.gitignore
+++ b/.gitignore
@@ -6,3 +6,10 @@
 dist/
 dist-newstyle/
 .ghc.environment.*
+
+# direnv
+.envrc
+.direnv
+
+# nix 
+result*
diff --git a/cabal.project b/cabal.project
index 737754c..3b30511 100644
--- a/cabal.project
+++ b/cabal.project
@@ -1 +1,7 @@
 packages: sop-core/ generics-sop/
+
+repository hackage.haskell.org
+  url: http://hackage.haskell.org/packages/archive
+
+index-state:
+  , hackage.haskell.org 2023-03-21T09:55:23Z
diff --git a/generics-sop/src/Generics/SOP.hs b/generics-sop/src/Generics/SOP.hs
index 9b13241..6dd1eb9 100644
--- a/generics-sop/src/Generics/SOP.hs
+++ b/generics-sop/src/Generics/SOP.hs
@@ -242,6 +242,7 @@ module Generics.SOP (
   , NS(..)
   , SOP(..)
   , unSOP
+  , unUSOP
   , POP(..)
   , unPOP
     -- * Metadata
diff --git a/generics-sop/src/Generics/SOP/GGP.hs b/generics-sop/src/Generics/SOP/GGP.hs
index 7b3e6ff..a8b0192 100644
--- a/generics-sop/src/Generics/SOP/GGP.hs
+++ b/generics-sop/src/Generics/SOP/GGP.hs
@@ -1,5 +1,6 @@
 {-# LANGUAGE EmptyCase, PolyKinds, UndecidableInstances #-}
 {-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
 -- | Derive @generics-sop@ boilerplate instances from GHC's 'GHC.Generic'.
 --
 -- The technique being used here is described in the following paper:
@@ -17,16 +18,19 @@ module Generics.SOP.GGP
   , gfrom
   , gto
   , gdatatypeInfo
+  , DeferMkLifted
   ) where
 
 import Data.Proxy (Proxy (..))
-import Data.Kind (Type)
+import Data.Kind (Type, Constraint)
 import GHC.Generics as GHC
 import Generics.SOP.NP as SOP
 import Generics.SOP.NS as SOP
 import Generics.SOP.BasicFunctors as SOP
 import qualified Generics.SOP.Type.Metadata as SOP.T
 import Generics.SOP.Metadata as SOP
+import GHC.Exts (Levity(Lifted))
+import GHC.TypeLits (TypeError, ErrorMessage (Text, ShowType, (:<>:), (:$$:)))
 
 type family ToSingleCode (a :: Type -> Type) :: Type
 type instance ToSingleCode (K1 _i a) = a
@@ -121,7 +125,7 @@ class GSingleTo (a :: Type -> Type) where
   gSingleTo :: ToSingleCode a -> a x
 
 instance GSingleTo (K1 i a) where
-  gSingleTo a = K1 a
+  gSingleTo = K1
 
 class GProductTo (a :: Type -> Type) where
   gProductTo :: NP I (ToProductCode a xs) -> (a x -> NP I xs -> r) -> r
@@ -175,7 +179,20 @@ instance (GProductTo a) => GSumTo (M1 C c a) where
   gSumTo (SOP (S xs)) _ k = k (SOP xs)
 
 instance (GSumTo a) => GSumTo (M1 D c a) where
-  gSumTo xss s k = gSumTo xss (s . M1) k
+  gSumTo xss s = gSumTo xss (s . M1)
+
+type MkTUnliftedError :: ErrorMessage -> k -> l
+type family MkTUnliftedError tfName ty where
+  MkTUnliftedError tfName ty = TypeError
+    (tfName :<>: 'Text " only supports Lifted Types"
+      :$$: 'Text "but " :<>: 'ShowType ty :<>: 'Text " is unlifted"
+    )
+
+type DeferMkLifted :: (Type -> Constraint) -> BoxedType levity -> Constraint
+type family DeferMkLifted c ty where
+  DeferMkLifted @'Lifted c ty = c ty
+  DeferMkLifted c ty = MkTUnliftedError ('ShowType c) ty
+ 
 
 -- | Compute the SOP code of a datatype.
 --
@@ -185,13 +202,22 @@ instance (GSumTo a) => GSumTo (M1 D c a) where
 -- This is the default definition for 'Generics.SOP.Code'.
 -- For more info, see 'Generics.SOP.Generic'.
 --
-type GCode (a :: Type) = ToSumCode (GHC.Rep a) '[]
+type GCode :: BoxedType levity -> [[BoxedType levity]]
+type family GCode a where
+  GCode @'Lifted a = ToSumCode (GHC.Rep a) '[]
+  GCode a = MkTUnliftedError ('Text "GCode") a
 
 -- | Constraint for the class that computes 'gfrom'.
-type GFrom a = GSumFrom (GHC.Rep a)
+type GFrom :: BoxedType levity -> Constraint
+type family GFrom a where
+  GFrom @'Lifted a = GSumFrom (GHC.Rep a)
+  GFrom a = MkTUnliftedError ('Text "GFrom") a
 
 -- | Constraint for the class that computes 'gto'.
-type GTo a = GSumTo (GHC.Rep a)
+type GTo :: BoxedType levity -> Constraint
+type family GTo a where
+  GTo @'Lifted a = GSumTo (GHC.Rep a)
+  GTo a = MkTUnliftedError ('Text "GTo") a
 
 -- | Constraint for the class that computes 'gdatatypeInfo'.
 type GDatatypeInfo a = SOP.T.DemoteDatatypeInfo (GDatatypeInfoOf a) (GCode a)
diff --git a/generics-sop/src/Generics/SOP/Instances.hs b/generics-sop/src/Generics/SOP/Instances.hs
index 40db2c6..aa8cb0b 100644
--- a/generics-sop/src/Generics/SOP/Instances.hs
+++ b/generics-sop/src/Generics/SOP/Instances.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE EmptyCase #-}
+{-# LANGUAGE EmptyCase, UnliftedDatatypes #-}
 {-# LANGUAGE TemplateHaskell #-}
 {-# OPTIONS_GHC -fno-warn-orphans #-}
 {-# OPTIONS_GHC -freduction-depth=100 #-}
@@ -73,9 +73,9 @@ import Generics.SOP.TH
 
 -- Types from Generics.SOP:
 
-deriveGeneric ''I
-deriveGeneric ''K
-deriveGeneric ''(:.:)
+deriveGeneric 'I
+deriveGeneric 'K
+deriveGeneric 'Comp
 deriveGeneric ''(-.->) -- new
 
 -- Cannot derive instances for Sing
diff --git a/generics-sop/src/Generics/SOP/TH.hs b/generics-sop/src/Generics/SOP/TH.hs
index da2638f..c9cf3ca 100644
--- a/generics-sop/src/Generics/SOP/TH.hs
+++ b/generics-sop/src/Generics/SOP/TH.hs
@@ -10,7 +10,7 @@ module Generics.SOP.TH
   , deriveMetadataType
   ) where
 
-import Control.Monad (join, replicateM, unless)
+import Control.Monad (replicateM, unless)
 import Data.List (foldl')
 import Data.Maybe (fromMaybe)
 import Data.Proxy
@@ -26,6 +26,7 @@ import qualified Generics.SOP.Type.Metadata as SOP.T
 import Generics.SOP.NP
 import Generics.SOP.NS
 import Generics.SOP.Universe
+import GHC.Exts (UnliftedType)
 
 -- | Generate @generics-sop@ boilerplate for the given datatype.
 --
@@ -87,7 +88,7 @@ deriveGenericOnly n =
 deriveGenericSubst :: Name -> (Name -> Q Type) -> Q [Dec]
 deriveGenericSubst n f = do
   dec <- reifyDatatype n
-  ds1 <- withDataDec dec (deriveGenericForDataDec  f)
+  ds1 <- withDataDec dec . deriveGenericForDataDec f =<< isLiftedKind n
   ds2 <- withDataDec dec (deriveMetadataForDataDec f)
   return (ds1 ++ ds2)
 
@@ -98,7 +99,7 @@ deriveGenericSubst n f = do
 deriveGenericOnlySubst :: Name -> (Name -> Q Type) -> Q [Dec]
 deriveGenericOnlySubst n f = do
   dec <- reifyDatatype n
-  withDataDec dec (deriveGenericForDataDec f)
+  withDataDec dec . deriveGenericForDataDec f =<< isLiftedKind n
 
 -- | Like 'deriveGenericOnly', but don't derive class instance, only functions.
 --
@@ -127,6 +128,7 @@ deriveGenericFunctions n codeName fromName toName = do
   let fromName' = mkName fromName
   let toName'   = mkName toName
   dec <- reifyDatatype n
+  isLifted <- isLiftedKind n
   withDataDec dec $ \_variant _cxt name bndrs instTys cons -> do
     let codeType = codeFor varT cons                     -- '[ '[Int], '[Tree, Tree] ]
     let origType = appTysSubst varT name instTys         -- Tree
@@ -134,9 +136,9 @@ deriveGenericFunctions n codeName fromName toName = do
     sequence
       [ tySynD codeName' bndrs codeType                 -- type TreeCode = '[ '[Int], '[Tree, Tree] ]
       , sigD fromName' [t| $origType -> $repType |]     -- fromTree :: Tree -> SOP I TreeCode
-      , embedding fromName' cons                        -- fromTree ... =
+      , embedding fromName' isLifted cons                        -- fromTree ... =
       , sigD toName' [t| $repType -> $origType |]       -- toTree :: SOP I TreeCode -> Tree
-      , projection toName' cons                         -- toTree ... =
+      , projection toName' isLifted cons                         -- toTree ... =
       ]
 
 -- | Derive @DatatypeInfo@ value for the type.
@@ -189,18 +191,18 @@ deriveMetadataType n datatypeInfoName = do
       [ tySynD datatypeInfoName' [] (metadataType' variant name cons) ]
 
 deriveGenericForDataDec ::
-  (Name -> Q Type) -> DatatypeVariant -> Cxt -> Name -> [TyVarBndrUnit] -> [Type] -> [TH.ConstructorInfo] -> Q [Dec]
-deriveGenericForDataDec f _variant _cxt name _bndrs instTys cons = do
+  (Name -> Q Type) -> Bool -> DatatypeVariant -> Cxt -> Name -> [TyVarBndrUnit] -> [Type] -> [TH.ConstructorInfo] -> Q [Dec]
+deriveGenericForDataDec f isLifted _variant _cxt name _bndrs instTys cons = do
   let typ = appTysSubst f name instTys
-  deriveGenericForDataType f typ cons
+  deriveGenericForDataType f isLifted typ cons
 
-deriveGenericForDataType :: (Name -> Q Type) -> Q Type -> [TH.ConstructorInfo] -> Q [Dec]
-deriveGenericForDataType f typ cons = do
+deriveGenericForDataType :: (Name -> Q Type) -> Bool -> Q Type -> [TH.ConstructorInfo] -> Q [Dec]
+deriveGenericForDataType f isLifted typ cons = do
   let codeSyn = tySynInstDCompat ''Generics.SOP.Universe.Code Nothing [typ] (codeFor f cons)
   inst <- instanceD
             (cxt [])
             [t| Generic $typ |]
-            [codeSyn, embedding 'from cons, projection 'to cons]
+            [codeSyn, embedding 'from isLifted cons , projection 'to isLifted cons ]
   return [inst]
 
 deriveMetadataForDataDec ::
@@ -238,8 +240,8 @@ codeFor f = promotedTypeList . map go
   Computing the embedding/projection pair
 -------------------------------------------------------------------------------}
 
-embedding :: Name -> [TH.ConstructorInfo] -> Q Dec
-embedding fromName = funD fromName . go' (\e -> [| Z $e |])
+embedding :: Name -> Bool -> [TH.ConstructorInfo] -> Q Dec
+embedding fromName isLifted = funD fromName . go' (appProperCon isLifted 'Z 'UZ)
   where
     go' :: (Q Exp -> Q Exp) -> [TH.ConstructorInfo] -> [Q Clause]
     go' _ [] = (:[]) $ do
@@ -249,18 +251,18 @@ embedding fromName = funD fromName . go' (\e -> [| Z $e |])
 
     go :: (Q Exp -> Q Exp) -> [TH.ConstructorInfo] -> [Q Clause]
     go _  []     = []
-    go br (c:cs) = mkClause br c : go (\e -> [| S $(br e) |]) cs
+    go br (c:cs) = mkClause br c : go (appProperCon isLifted 'S 'US . br) cs
 
     mkClause :: (Q Exp -> Q Exp) -> TH.ConstructorInfo -> Q Clause
     mkClause br c = do
       (n, ts) <- conInfo c
       vars    <- replicateM (length ts) (newName "x")
       clause [conP n (map varP vars)]
-             (normalB [| SOP $(br . npE . map (appE (conE 'I) . varE) $ vars) |])
+             (normalB ( appProperCon isLifted 'SOP 'USOP . br . npE isLifted . map (appProperCon isLifted 'I 'UI . varE) $ vars))
              []
 
-projection :: Name -> [TH.ConstructorInfo] -> Q Dec
-projection toName = funD toName . go'
+projection :: Name -> Bool -> [TH.ConstructorInfo] -> Q Dec
+projection toName isLifted = funD toName . go'
   where
     go' :: [TH.ConstructorInfo] -> [Q Clause]
     go' [] = (:[]) $ do
@@ -270,7 +272,7 @@ projection toName = funD toName . go'
 
     go :: (Q Pat -> Q Pat) -> [TH.ConstructorInfo] -> [Q Clause]
     go br [] = [mkUnreachableClause br]
-    go br (c:cs) = mkClause br c : go (\p -> conP 'S [br p]) cs
+    go br (c:cs) = mkClause br c : go (\p -> patProperCon isLifted 'S 'US [br p]) cs
 
     -- Generates a final clause of the form:
     --
@@ -283,18 +285,21 @@ projection toName = funD toName . go'
     -- This, however, would require clients to enable the EmptyCase extension
     -- in their own code, which is something which we have not previously
     -- required. Therefore, we do not generate this code at the moment.
+    --
+    -- for the unlifted case, we don't have to seq the argument because we can
+    -- be sure that the argument is already evaluated
     mkUnreachableClause :: (Q Pat -> Q Pat) -> Q Clause
     mkUnreachableClause br = do
       var <- newName "x"
-      clause [conP 'SOP [br (varP var)]]
-             (normalB [| $(varE var) `seq` error "inaccessible" |])
+      clause [patProperCon isLifted 'SOP 'USOP [br (varP var)]]
+             (normalB $ if isLifted then [| $(varE var) `seq` error "inaccessible (lifted case)" |] else [| error "inaccessible (unlifted case)" |])
              []
 
     mkClause :: (Q Pat -> Q Pat) -> TH.ConstructorInfo -> Q Clause
     mkClause br c = do
       (n, ts) <- conInfo c
       vars    <- replicateM (length ts) (newName "x")
-      clause [conP 'SOP [br . conP 'Z . (:[]) . npP . map (\v -> conP 'I [varP v]) $ vars]]
+      clause [patProperCon isLifted 'SOP 'USOP [br . patProperCon isLifted 'Z 'UZ. (:[]) . npP isLifted . map (\v -> patProperCon isLifted 'I 'UI [varP v]) $ vars]]
              (normalB . appsE $ conE n : map varE vars)
              []
 
@@ -308,20 +313,22 @@ metadataType typ variant typeName cs =
 
 -- | Derive term-level metadata.
 metadata' :: DatatypeVariant -> Name -> [TH.ConstructorInfo] -> Q Exp
-metadata' dataVariant typeName cs = md
+metadata' dataVariant typeName cs =
+  -- FIXME: may be wrong
+  isLiftedKind typeName >>= md
   where
-    md :: Q Exp
-    md | isNewtypeVariant dataVariant
+    md :: Bool -> Q Exp
+    md isLifted | isNewtypeVariant dataVariant
        = [| SOP.Newtype $(stringE (nameModule' typeName))
                         $(stringE (nameBase typeName))
-                        $(mdCon (head cs))
+                        $(mdCon isLifted (head cs))
           |]
 
        | otherwise
        = [| SOP.ADT     $(stringE (nameModule' typeName))
                         $(stringE (nameBase typeName))
-                        $(npE $ map mdCon cs)
-                        $(popE $ map mdStrictness cs)
+                        $(npE isLifted $ map (mdCon isLifted) cs)
+                        $(popE isLifted $ map mdStrictness cs)
           |]
 
     mdStrictness :: TH.ConstructorInfo -> Q [Q Exp]
@@ -339,14 +346,14 @@ metadata' dataVariant typeName cs = md
           $(mdDecidedStrictness  ds)
         |]) bs dss)
 
-    mdCon :: TH.ConstructorInfo -> Q Exp
-    mdCon ci@(ConstructorInfo { constructorName    = n
+    mdCon :: Bool -> TH.ConstructorInfo -> Q Exp
+    mdCon isLifted ci@(ConstructorInfo { constructorName    = n
                               , constructorVariant = conVariant }) =
       checkForGADTs ci $
       case conVariant of
         NormalConstructor    -> [| SOP.Constructor $(stringE (nameBase n)) |]
         RecordConstructor ts -> [| SOP.Record      $(stringE (nameBase n))
-                                                   $(npE (map mdField ts))
+                                                   $(npE isLifted (map mdField ts))
                                  |]
         InfixConstructor     -> do
           fixity <- reifyFixity n
@@ -467,19 +474,18 @@ nameModule' = fromMaybe "" . nameModule
 -- Construct
 --
 -- > a :* b :* c :* Nil
-npE :: [Q Exp] -> Q Exp
-npE []     = [| Nil |]
-npE (e:es) = [| $e :* $(npE es) |]
+npE :: Bool -> [Q Exp] -> Q Exp
+npE isLifted = foldr (\e es -> if isLifted then [| $e :* $es |] else [| $e ::* $es |]) (if isLifted then [| Nil |] else [| UNil |])
 
 -- Construct a POP.
-popE :: [Q [Q Exp]] -> Q Exp
-popE ess =
-  [| POP $(npE (map (join . fmap npE) ess)) |]
+popE :: Bool -> [Q [Q Exp]] -> Q Exp
+popE isLifted ess =
+  [| POP $(npE isLifted (map (npE  isLifted =<<) ess)) |]
 
 -- Like npE, but construct a pattern instead
-npP :: [Q Pat] -> Q Pat
-npP []     = conP 'Nil []
-npP (p:ps) = conP '(:*) [p, npP ps]
+npP :: Bool -> [Q Pat] -> Q Pat
+npP isLifted []     = conP (if isLifted then 'Nil else 'UNil) []
+npP isLifted (p:ps) = conP (if isLifted then '(:*) else '(::*)) [p, npP isLifted ps]
 
 {-------------------------------------------------------------------------------
   Some auxiliary definitions for working with TH
@@ -502,7 +508,7 @@ promotedTypeList (t:ts) = [t| $promotedConsT $t $(promotedTypeList ts) |]
 
 promotedTypeListOfList :: [Q [Q Type]] -> Q Type
 promotedTypeListOfList =
-  promotedTypeList . map (join . fmap promotedTypeList)
+  promotedTypeList . map (promotedTypeList =<<)
 
 promotedTypeListSubst :: (Name -> Q Type) -> [Q Type] -> Q Type
 promotedTypeListSubst _ []     = promotedNilT
@@ -539,6 +545,21 @@ substType f = go
       -- in the benchmarking suite. So we can fall back on identity in all
       -- but the cases we need for the benchmarking suite.
 
+-- FIXME: probably doesn't work for data families with unlifted members
+isLiftedKind :: Name -> Q Bool
+isLiftedKind = fmap (/= ConT ''UnliftedType) . reifyType
+
+appProperCon :: Bool -> Name -> Name -> Q Exp -> Q Exp
+appProperCon isLifted liftedCon unliftedCon = if isLifted
+                           then appE $ conE liftedCon
+                           else appE $ conE unliftedCon
+
+patProperCon :: Quote m => Bool -> Name -> Name -> [m Pat] -> m Pat
+patProperCon isLifted liftedCon unliftedCon =
+  if isLifted
+    then conP liftedCon
+    else conP unliftedCon
+
 -- Process a DatatypeInfo using continuation-passing style.
 withDataDec :: TH.DatatypeInfo
             -> (DatatypeVariant
diff --git a/generics-sop/src/Generics/SOP/Universe.hs b/generics-sop/src/Generics/SOP/Universe.hs
index 4b67a48..175cad0 100644
--- a/generics-sop/src/Generics/SOP/Universe.hs
+++ b/generics-sop/src/Generics/SOP/Universe.hs
@@ -1,5 +1,9 @@
 {-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE UndecidableSuperClasses #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE TypeApplications #-}
+{-# OPTIONS_GHC -fprint-explicit-kinds #-}
 -- | Codes and interpretations
 module Generics.SOP.Universe where
 
@@ -15,6 +19,7 @@ import Generics.SOP.NS
 import Generics.SOP.GGP
 import Generics.SOP.Metadata
 import qualified Generics.SOP.Type.Metadata as T
+import GHC.Exts (Levity (Lifted))
 
 -- | The (generic) representation of a datatype.
 --
@@ -22,7 +27,10 @@ import qualified Generics.SOP.Type.Metadata as T
 -- The isomorphism is witnessed by 'from' and 'to' from the
 -- 'Generic' class.
 --
-type Rep a = SOP I (Code a)
+
+type Rep :: forall levin levout. BoxedType levin -> BoxedType levout
+type family Rep a where
+  Rep @levin @levout a = SOP (I ::  BoxedType levin -> BoxedType levout) (Code a)
 
 -- | The class of representable datatypes.
 --
@@ -94,7 +102,7 @@ type Rep a = SOP I (Code a)
 --
 -- still holds.
 --
-class (All SListI (Code a)) => Generic (a :: Type) where
+class (All SListI (Code a)) => Generic (a :: BoxedType levity) where
   -- | The code of a datatype.
   --
   -- This is a list of lists of its components. The outer list contains
@@ -112,22 +120,43 @@ class (All SListI (Code a)) => Generic (a :: Type) where
   -- >    , '[ Tree, Tree ]
   -- >    ]
   --
-  type Code a :: [[Type]]
-  type Code a = GCode a
+  type Code a :: [[BoxedType levity]]
+  type Code (a :: BoxedType levity) = GCode a
+
+  -- | The output levity of the representation
+  --
+  --   This is the levity the representation of the type 'a' will have
+  --   by default it's the same levity as the levity of the incoming type
+  --   if we have a lifted type, the out levity cannot be unlifted anyway so we monomorphise
+  --   that happens
+  type OutLev a :: Levity
+  type OutLev (a :: BoxedType lev) = lev
 
   -- | Converts from a value to its structural representation.
-  from         :: a -> Rep a
-  default from :: (GFrom a, GHC.Generic a, Rep a ~ SOP I (GCode a))
-               => a -> Rep a
+  from         :: a -> Rep @levity @(CompOutLev a) a
+  default from :: (levity ~ 'Lifted, CompOutLev a ~ 'Lifted, GFrom a, DeferMkLifted GHC.Generic a, Rep a ~ SOP I (GCode a))
+               => a -> Rep @levity @(CompOutLev a) a
   from = gfrom
 
   -- | Converts from a structural representation back to the
   -- original value.
-  to         :: Rep a -> a
-  default to :: (GTo a, GHC.Generic a, Rep a ~ SOP I (GCode a))
-             => Rep a -> a
+  to         :: Rep @levity @(CompOutLev a) a -> a
+  default to :: (levity ~ 'Lifted, CompOutLev a ~ 'Lifted, GTo a, DeferMkLifted GHC.Generic a, Rep a ~ SOP I (GCode a))
+             => Rep @levity @(CompOutLev a) a -> a
   to = gto
 
+type KindOf :: k -> Type
+type family KindOf t where
+  KindOf (t :: k) = k
+
+type DefaultOutLevWhenLifted :: Levity -> Type -> Levity
+type family DefaultOutLevWhenLifted col il where
+  DefaultOutLevWhenLifted col Type = 'Lifted
+  DefaultOutLevWhenLifted col _ = col
+
+type CompOutLev :: BoxedType levity -> Levity
+type CompOutLev a = DefaultOutLevWhenLifted (OutLev a) (KindOf a)
+
 -- | A class of datatypes that have associated metadata.
 --
 -- It is possible to use the sum-of-products approach to generic programming
diff --git a/generics-sop/test/Example.hs b/generics-sop/test/Example.hs
index f10c3d8..9e803c3 100644
--- a/generics-sop/test/Example.hs
+++ b/generics-sop/test/Example.hs
@@ -3,11 +3,16 @@
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DefaultSignatures #-}
 {-# LANGUAGE GADTs #-}
-{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE UnliftedDatatypes #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE ViewPatterns #-}
 {-# OPTIONS_GHC -fno-warn-deprecations #-}
 module Main (main, toTreeC, toDataFamC) where
 
@@ -17,6 +22,8 @@ import Generics.SOP.TH
 import qualified Generics.SOP.Type.Metadata as T
 
 import HTransExample
+import GHC.Exts (UnliftedType, Levity (Unlifted))
+import Data.Kind (Constraint)
 
 -- Generic show, kind of
 gshow :: (Generic a, All2 Show (Code a)) => a -> String
@@ -28,7 +35,7 @@ gshowS (SOP (S xss)) = gshowS (SOP xss)
 
 gshowP :: (All Show xs) => NP I xs -> String
 gshowP Nil         = ""
-gshowP (I x :* xs) = show x ++ (gshowP xs)
+gshowP (I x :* xs) = show x ++ gshowP xs
 
 -- Generic enum, kind of
 class Enumerable a where
@@ -40,8 +47,7 @@ genum =
 
 genumS :: (All SListI xss, All2 Enumerable xss) => [SOP I xss]
 genumS =
-  concat (fmap apInjs_POP
-    (hsequence (hcpure (Proxy :: Proxy Enumerable) enum)))
+  concatMap apInjs_POP (hsequence (hcpure (Proxy :: Proxy Enumerable) enum))
 
 -- GHC.Generics
 data Tree = Leaf Int | Node Tree Tree
@@ -206,30 +212,62 @@ instance Enumerable ABCC where
 instance Enumerable VoidC where
   enum = fmap toVoidC genumS
 
+type UT :: UnliftedType
+data UT = UL | UN UT UT
+
+deriveGenericOnly ''UT
+
+type UEq :: UnliftedType -> Constraint
+class UEq a where
+  ueq :: a -> a -> Bool
+  default ueq :: (Generic a, All2 UEq (Code a), OutLev a ~ 'Unlifted) => a -> a -> Bool
+  ueq = gueq
+
+infix 4 `ueq`
+
+gueq :: forall (a :: UnliftedType). (Generic a, All2 UEq (Code a), OutLev a ~ 'Unlifted) => a -> a -> Bool
+gueq x y =
+  let repx :: Rep @'Unlifted @'Unlifted a
+      repx = from x
+      repy :: Rep @'Unlifted @'Unlifted a
+      repy = from y
+   in constrsSame (unUSOP repx) (unUSOP repy)
+  where
+    constrsSame :: forall (xss :: [[UnliftedType]]). (All2 UEq xss) => NS (NP (I @'Unlifted @'Unlifted)) xss -> NS (NP (I @'Unlifted @'Unlifted)) xss -> Bool
+    constrsSame (US x') (US y') = constrsSame x' y'
+    constrsSame (UZ x') (UZ y') = fieldsSame x' y'
+    constrsSame _ _ = False
+
+    fieldsSame :: forall (xs :: [UnliftedType]). All UEq xs => NP (I @'Unlifted @'Unlifted) xs -> NP (I @'Unlifted @'Unlifted) xs -> Bool
+    fieldsSame (UI x' ::* xs) (UI y' ::* ys) = x' `ueq` y' && fieldsSame xs ys
+    fieldsSame UNil UNil = True
+
+instance UEq UT 
+
 -- Tests
 main :: IO ()
 main = do
   print tree
   print abc
   print dataFam
-  print $ (enum :: [ABC])
-  print $ (enum :: [Void])
+  print (enum :: [ABC])
+  print (enum :: [Void])
   print $ datatypeInfo (Proxy :: Proxy Tree)
   print $ datatypeInfo (Proxy :: Proxy Void)
   print $ datatypeInfo (Proxy :: Proxy (DataFam Int (Maybe Int) Int))
   print treeB
   print abcB
   print dataFamB
-  print $ (enum :: [ABCB])
-  print $ (enum :: [VoidB])
+  print (enum :: [ABCB])
+  print (enum :: [VoidB])
   print $ datatypeInfo (Proxy :: Proxy TreeB)
   print $ datatypeInfo (Proxy :: Proxy VoidB)
   print $ datatypeInfo (Proxy :: Proxy (DataFamB Int (Maybe Int) Int))
   print treeC
   print abcC
   print dataFamC
-  print $ (enum :: [ABCC])
-  print $ (enum :: [VoidC])
+  print (enum :: [ABCC])
+  print (enum :: [VoidC])
   print treeDatatypeInfo
   print demotedTreeDatatypeInfo
   print demotedDataFamDatatypeInfo
@@ -238,3 +276,4 @@ main = do
   print (voidDatatypeInfo == demotedVoidDatatypeInfo)
   print (dataFamDatatypeInfo == demotedDataFamDatatypeInfo)
   print $ convertFull tree
+  print $ UN (UN UL UL) (UN UL UL) `ueq` UN (UN UL UL) (UN UL UL)
diff --git a/sop-core/src/Data/SOP.hs b/sop-core/src/Data/SOP.hs
index f48f195..cfa0027 100644
--- a/sop-core/src/Data/SOP.hs
+++ b/sop-core/src/Data/SOP.hs
@@ -7,6 +7,7 @@ module Data.SOP (
   , NS(..)
   , SOP(..)
   , unSOP
+  , unUSOP
   , POP(..)
   , unPOP
     -- * Combinators
diff --git a/sop-core/src/Data/SOP/BasicFunctors.hs b/sop-core/src/Data/SOP/BasicFunctors.hs
index 3e4225e..fab9426 100644
--- a/sop-core/src/Data/SOP/BasicFunctors.hs
+++ b/sop-core/src/Data/SOP/BasicFunctors.hs
@@ -1,4 +1,5 @@
-{-# LANGUAGE PolyKinds, DeriveGeneric #-}
+{-# LANGUAGE PolyKinds, DeriveGeneric, UnliftedNewtypes, StandaloneKindSignatures #-}
+{-# LANGUAGE TypeApplications #-}
 -- | Basic functors.
 --
 -- Definitions of the type-level equivalents of
@@ -41,12 +42,13 @@ module Data.SOP.BasicFunctors
   , mapKIK
   , mapKKI
   , mapKKK
+  -- * Convenience helpers
+  , BoxedType
   ) where
 
 #if !MIN_VERSION_base(4,11,0)
 import Data.Semigroup (Semigroup (..))
 #endif
-import Data.Kind (Type)
 import qualified GHC.Generics as GHC
 
 import Data.Functor.Classes
@@ -57,6 +59,12 @@ import Control.DeepSeq (NFData1(..), NFData2(..))
 #endif
 
 import Data.Coerce (coerce)
+import GHC.Exts (TYPE, RuntimeRep(BoxedRep), Levity (Lifted, Unlifted))
+import Data.Kind (Type)
+
+-- | convenience type to make working with levity polymorphic types easier
+type BoxedType :: Levity -> Type
+type BoxedType levity = TYPE ('BoxedRep levity)
 
 -- * Basic functors
 
@@ -65,9 +73,16 @@ import Data.Coerce (coerce)
 -- Like 'Data.Functor.Constant.Constant', but kind-polymorphic
 -- in its second argument and with a shorter name.
 --
-newtype K (a :: Type) (b :: k) = K a
+data family K :: forall levin levout k. BoxedType levin -> k -> BoxedType levout
+newtype instance K @'Lifted @'Lifted a b = K a
   deriving (Functor, Foldable, Traversable, GHC.Generic)
 
+-- | @since 0.6.0.0
+newtype instance K @'Unlifted @'Unlifted a b = UK {unUK :: a}
+
+-- | @since 0.6.0.0
+data instance K @'Unlifted @'Lifted a b = ULK {unULK :: a}
+
 -- | @since 0.2.4.0
 instance Eq2 K where
     liftEq2 eq _ (K x) (K y) = eq x y
@@ -120,7 +135,7 @@ instance Monoid a => Applicative (K a) where
   pure _      = K mempty
   K x <*> K y = K (mappend x y)
 
--- | Extract the contents of a 'K' value.
+-- | @since 0.6.0.0
 unK :: K a b -> a
 unK (K x) = x
 
@@ -128,9 +143,16 @@ unK (K x) = x
 --
 -- Like 'Data.Functor.Identity.Identity', but with a shorter name.
 --
-newtype I (a :: Type) = I a
+data family I :: forall levin levout. BoxedType levin -> BoxedType levout
+newtype instance I @'Lifted @'Lifted a = I a
   deriving (Functor, Foldable, Traversable, GHC.Generic)
 
+-- | @since 0.6.0.0
+newtype instance I @'Unlifted @'Unlifted a = UI {unUI :: a}
+
+-- | @since 0.6.0.0
+data instance I @'Unlifted @'Lifted a = ULI {unULI :: a}
+
 -- | @since 0.4.0.0
 instance Semigroup a => Semigroup (I a) where
   I x <> I y = I (x <> y)
@@ -178,9 +200,17 @@ unI (I x) = x
 -- Like 'Data.Functor.Compose.Compose', but kind-polymorphic
 -- and with a shorter name.
 --
-newtype (:.:) (f :: l -> Type) (g :: k -> l) (p :: k) = Comp (f (g p))
+data family (:.:) :: forall levin levout k l.
+  (l -> BoxedType levin) -> (k -> l) -> k -> BoxedType levout
+newtype instance (:.:) @'Lifted @'Lifted f g p = Comp (f (g p))
   deriving (GHC.Generic)
 
+-- | @since 0.6.0.0
+newtype instance (:.:) @'Unlifted @'Unlifted f g p = UComp {unUComp :: f (g p)}
+
+-- | @since 0.6.0.0
+data instance (:.:) @'Unlifted @'Lifted f g p = ULComp {unULComp :: f (g p)}
+
 infixr 7 :.:
 
 -- | @since 0.4.0.0
diff --git a/sop-core/src/Data/SOP/NP.hs b/sop-core/src/Data/SOP/NP.hs
index 3d3adfe..14889e5 100644
--- a/sop-core/src/Data/SOP/NP.hs
+++ b/sop-core/src/Data/SOP/NP.hs
@@ -1,6 +1,9 @@
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE UnliftedDatatypes #-}
+{-# LANGUAGE UnliftedNewtypes #-}
+{-# LANGUAGE TypeApplications #-}
 -- | n-ary products (and products of products)
 module Data.SOP.NP
   ( -- * Datatypes
@@ -103,6 +106,7 @@ import Data.SOP.BasicFunctors
 import Data.SOP.Classes
 import Data.SOP.Constraint
 import Data.SOP.Sing
+import GHC.Exts (Levity (Lifted, Unlifted), UnliftedType)
 
 -- | An n-ary product.
 --
@@ -132,11 +136,18 @@ import Data.SOP.Sing
 -- > K 0      :* K 1     :* Nil  ::  NP (K Int) '[ Char, Bool ]
 -- > Just 'x' :* Nothing :* Nil  ::  NP Maybe   '[ Char, Bool ]
 --
-data NP :: (k -> Type) -> [k] -> Type where
+data family NP :: forall levity k. (k -> BoxedType levity) -> [k] -> BoxedType levity
+data instance NP @'Lifted f xs where
   Nil  :: NP f '[]
-  (:*) :: f x -> NP f xs -> NP f (x ': xs)
+  (:*) :: f x -> NP  f xs -> NP f (x ': xs)
+
+data instance NP @'Unlifted f xs where
+  UNil :: NP f '[]
+  (::*) :: f x -> NP f xs -> NP f (x ': xs)
 
 infixr 5 :*
+infixr 5 ::*
+
 
 -- This is written manually,
 -- because built-in deriving doesn't use associativity information!
@@ -184,7 +195,14 @@ instance All (NFData `Compose` f) xs => NFData (NP f xs) where
 -- information that is available for all arguments of all constructors
 -- of a datatype.
 --
-newtype POP (f :: (k -> Type)) (xss :: [[k]]) = POP (NP (NP f) xss)
+data family POP :: forall levin levout k. (k -> BoxedType levin) -> [[k]] -> BoxedType levout
+newtype instance POP @'Lifted @'Lifted f xss  = POP (NP (NP f) xss)
+
+-- | @since 0.6.0.0
+newtype instance POP @'Unlifted @'Unlifted f xss = UPOP {unUPOP :: NP (NP f) xss}
+
+-- | @since 0.6.0.0
+data instance POP @'Unlifted @'Lifted f xss = ULPOP {unULPOP :: NP (NP f) xss}
 
 deriving instance (Show (NP (NP f) xss)) => Show (POP f xss)
 deriving instance (Eq   (NP (NP f) xss)) => Eq   (POP f xss)
diff --git a/sop-core/src/Data/SOP/NS.hs b/sop-core/src/Data/SOP/NS.hs
index 62b214d..0a0cd27 100644
--- a/sop-core/src/Data/SOP/NS.hs
+++ b/sop-core/src/Data/SOP/NS.hs
@@ -5,12 +5,16 @@
 {-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# OPTIONS_GHC -fno-warn-deprecations #-}
+{-# LANGUAGE UnliftedDatatypes #-}
+{-# LANGUAGE UnliftedNewtypes #-}
+{-# LANGUAGE TypeApplications #-}
 -- | n-ary sums (and sums of products)
 module Data.SOP.NS
   ( -- * Datatypes
     NS(..)
   , SOP(..)
   , unSOP
+
     -- * Constructing sums
   , Injection
   , injections
@@ -103,6 +107,7 @@ import Data.SOP.Classes
 import Data.SOP.Constraint
 import Data.SOP.NP
 import Data.SOP.Sing
+import GHC.Exts (Levity (Lifted, Unlifted), UnliftedType)
 
 -- * Datatypes
 
@@ -146,10 +151,15 @@ import Data.SOP.Sing
 -- > S (Z (I True)) :: NS I       '[ Char, Bool ]
 -- > S (Z (K 1))    :: NS (K Int) '[ Char, Bool ]
 --
-data NS :: (k -> Type) -> [k] -> Type where
+data family NS :: forall levity k. (k -> BoxedType levity) -> [k] -> BoxedType levity 
+data instance NS @'Lifted f xs where
   Z :: f x -> NS f (x ': xs)
   S :: NS f xs -> NS f (x ': xs)
 
+data instance NS @'Unlifted f xs where
+  UZ :: f x -> NS f (x ': xs)
+  US :: NS f xs -> NS f (x ': xs)
+
 deriving instance All (Show `Compose` f) xs => Show (NS f xs)
 deriving instance All (Eq   `Compose` f) xs => Eq   (NS f xs)
 deriving instance (All (Eq `Compose` f) xs, All (Ord `Compose` f) xs) => Ord (NS f xs)
@@ -242,7 +252,14 @@ instance HIndex NS where
 -- constructors, the product structure represents the arguments of
 -- each constructor.
 --
-newtype SOP (f :: (k -> Type)) (xss :: [[k]]) = SOP (NS (NP f) xss)
+data family SOP :: forall levin levout k. (k -> BoxedType levin) -> [[k]] -> BoxedType levout
+newtype instance SOP @'Lifted @'Lifted f xss = SOP (NS (NP f) xss)
+
+-- | @since 0.6.0.0
+newtype instance SOP @'Unlifted @'Unlifted f xss = USOP {unUSOP :: NS (NP f) xss}
+
+-- | @since 0.6.0.0
+data instance SOP @'Unlifted @'Lifted f xss = ULSOP {unULSOP :: NS (NP f) xss}
 
 deriving instance (Show (NS (NP f) xss)) => Show (SOP f xss)
 deriving instance (Eq   (NS (NP f) xss)) => Eq   (SOP f xss)