diff --git a/staged-sop-examples/bench/Bench.hs b/staged-sop-examples/bench/Bench.hs
index 22daae3..f857e10 100644
--- a/staged-sop-examples/bench/Bench.hs
+++ b/staged-sop-examples/bench/Bench.hs
@@ -1,9 +1,14 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE TypeApplications #-}
-{-# OPTIONS_GHC -ddump-simpl #-}
+
+{-# LANGUAGE IncoherentInstances #-}
+
+{-# OPTIONS_GHC -ddump-splices #-}
+-- {-# OPTIONS_GHC -ddump-simpl -dsuppress-all #-}
 module Main where
 
 import Codec.CBOR.Encoding
@@ -13,6 +18,7 @@ import ExampleTypes
 import ExampleFunctions
 import Gauge.Main
 import Gauge.Main.Options
+import Generics.SOP.Staged
 
 genum_Ordering :: () -> [Ordering]
 genum_Ordering () = genum
@@ -30,7 +36,11 @@ gsappend_Foo :: Foo -> Foo -> Foo
 gsappend_Foo = gsappend
 
 sgsappend_Foo :: Foo -> Foo -> Foo
-sgsappend_Foo = $$(sgsappend')
+sgsappend_Foo  =
+  let
+    c = constraints @Foo
+  in
+    $$(sgsappend' (pallC [|| c ||]))
 
 msappend_Foo :: Foo -> Foo -> Foo
 msappend_Foo (Foo is1 o1 txt1) (Foo is2 o2 txt2) =
@@ -48,7 +58,11 @@ instance Eq a => Eq (Tree GHCGenerics a) where
   (==) = ghcgeq
 
 instance Eq a => Eq (Tree StagedSOP a) where
-  x1 == x2 = $$(sgeq [|| x1 ||] [|| x2 ||])
+  x1 == x2 =
+    let
+      c = constraints @(Tree StagedSOP a)
+    in
+      $$(sgeq (allC [|| c ||]) [|| x1 ||] [|| x2 ||])
 
 instance Eq a => Eq (Tree Manual a) where
   Leaf a1 == Leaf a2 = a1 == a2
@@ -64,7 +78,11 @@ instance Eq (Prop GHCGenerics) where
   (==) = ghcgeq
 
 instance Eq (Prop StagedSOP) where
-  x1 == x2 = $$(sgeq [|| x1 ||] [|| x2 ||])
+  x1 == x2 =
+    let
+      c = constraints @(Prop StagedSOP)
+    in
+      $$(sgeq (allC [|| c ||]) [|| x1 ||] [|| x2 ||])
 
 instance Eq (Prop Manual) where
   Var x1 == Var x2 = x1 == x2
@@ -79,9 +97,21 @@ instance Serialise (Prop GenericsSOP) where
   encode = gencode
   decode = gdecode
 
+-- NOTE: decode currently requires IncoherentInstances because the
+-- way we are passing the Applicative instance for Decoder via an
+-- explicit dictionary, it ends up being in scope twice!
+--
 instance Serialise (Prop StagedSOP) where
-  encode = $$(sgencode)
-  decode = $$(sgdecode)
+  encode =
+    let
+      c = constraints @(Prop StagedSOP)
+    in
+      $$(sgencode (allC [|| c ||]))
+  decode =
+    let
+      c = constraints @(Prop StagedSOP)
+    in
+      $$(sgdecode (allC [|| c ||]))
 
 instance Serialise (Prop GHCGenerics)
 
diff --git a/staged-sop-examples/src/ExampleFunctions.hs b/staged-sop-examples/src/ExampleFunctions.hs
index 7584f24..fd6cb98 100644
--- a/staged-sop-examples/src/ExampleFunctions.hs
+++ b/staged-sop-examples/src/ExampleFunctions.hs
@@ -14,37 +14,47 @@ import Codec.CBOR.Encoding
 import Codec.CBOR.Decoding
 import Codec.Serialise
 import Control.DeepSeq
-import Data.SOP.Constraint (And)
+import Data.Kind
+import Data.SOP
+import Data.SOP.Constraint (And, Top)
+import Data.SOP.NP
+import Data.SOP.NS
 import qualified Generics.SOP as SOP
-import qualified Generics.SOP.NP as SOP
-import qualified Generics.SOP.NS as SOP
+-- import qualified Generics.SOP.NP as SOP
+-- import qualified Generics.SOP.NS as SOP
 import Generics.SOP.Staged
 import GHC.Generics as GHC hiding (C, (:.:))
-import Language.Haskell.TH
+import Language.Haskell.TH hiding (Type)
+import Language.Haskell.TH.Syntax hiding (Type)
 import ExampleTypes
 
 sgsappend ::
-  (SIsProductType a xs, All (Quoted Semigroup) xs) =>
-  Code a -> Code a -> Code a
-sgsappend c1 c2 =
+  SIsProductType a xs =>
+  NP (C :.: Dict Semigroup) xs ->
+  CodeQ a -> CodeQ a -> CodeQ a
+sgsappend dicts c1 c2 =
   sproductTypeFrom c1 $ \ a1 -> sproductTypeFrom c2 $ \ a2 ->
     sproductTypeTo
-      (czipWith_NP (Proxy @(Quoted Semigroup))
-        (mapCCC [|| (<>) ||]) a1 a2
+      (zipWith3_NP
+        (\ (Comp (C d)) (C a1) (C a2) -> C [|| case $$d of Dict -> ($$a1 <> $$a2) ||])
+        dicts a1 a2
       )
+-- TODO: it would be nice to simplify this, but it's not clear if it can be done;
+-- perhaps by means of quasi-quotation
 
 sgsappend' ::
-  (SIsProductType a xs, All (Quoted Semigroup) xs) =>
-  Code (a -> a -> a)
-sgsappend' =
-  [|| \ a1 a2 -> $$(sgsappend [|| a1 ||] [|| a2 ||]) ||]
+  SIsProductType a xs =>
+  NP (C :.: Dict Semigroup) xs ->
+  CodeQ (a -> a -> a)
+sgsappend' dicts =
+  [|| \ a1 a2 -> $$(sgsappend dicts [|| a1 ||] [|| a2 ||]) ||]
 
 gsappend ::
-  (SOP.IsProductType a xs, SOP.All Semigroup xs) =>
+  (SOP.IsProductType a xs, All Semigroup xs) =>
   a -> a -> a
 gsappend a1 a2 =
   SOP.productTypeTo
-    (SOP.czipWith_NP (Proxy @Semigroup)
+    (czipWith_NP (Proxy @Semigroup)
       (SOP.mapIII (<>)) (SOP.productTypeFrom a1) (SOP.productTypeFrom a2)
     )
 
@@ -64,25 +74,25 @@ instance Semigroup a => GSappend (K1 r a) where
 instance GSappend a => GSappend (M1 i c a) where
   ghcsappend' (M1 a1) (M1 a2) = M1 (ghcsappend' a1 a2)
 
-ghcsappend :: (GHC.Generic a, GSappend (Rep a)) => a -> a -> a
+ghcsappend :: (GHC.Generic a, GSappend (GHC.Rep a)) => a -> a -> a
 ghcsappend a1 a2 = to (ghcsappend' (from a1) (from a2))
 
-
 sgrnf ::
-  (SGeneric a, All (All (Quoted NFData)) (SDescription a)) =>
-  Code a -> Code ()
-sgrnf c =
+  SGeneric a =>
+  POP (C :.: Dict NFData) (SDescription a) ->
+  CodeQ a -> CodeQ ()
+sgrnf dicts c =
   sfrom c $ \ a ->
     foldr (\ x r -> [|| $$x `seq` $$r ||]) [|| () ||]
-      (collapse_SOP (cmap_SOP (Proxy @(Quoted NFData)) (mapCK [|| rnf ||]) a))
+      (collapse_SOP (selectWith_SOP (\ (Comp (C d)) (C x) -> K [|| withDict $$d (rnf $$x) ||]) dicts a))
 
 gShowEnum ::
   SOP.IsEnumType a => NP (K String) (SOP.Code a) -> a -> String
 gShowEnum names a =
-  SOP.collapse_NS (SOP.hzipWith const names (SOP.enumTypeFrom a))
+  collapse_NS (SOP.hzipWith const names (SOP.enumTypeFrom a))
 
 sgShowEnum ::
-  SIsEnumType a => NP (K String) (SDescription a) -> Code a -> Code String
+  SIsEnumType a => NP (K String) (SDescription a) -> CodeQ a -> CodeQ String
 sgShowEnum names c =
   senumTypeFrom c $ \ a ->
     liftTyped (collapse_NS (selectWith_NS const names a))
@@ -97,29 +107,34 @@ geq ::
 geq a1 a2 =
   SOP.ccompare_SOP (Proxy @Eq)
     False
-    (\ xs1 xs2 -> and (SOP.collapse_NP (SOP.czipWith_NP (Proxy @Eq) (SOP.mapIIK (==)) xs1 xs2)))
+    (\ xs1 xs2 -> and (collapse_NP (czipWith_NP (Proxy @Eq) (SOP.mapIIK (==)) xs1 xs2)))
     False
     (SOP.from a1) (SOP.from a2)
 
+-- This transcription is quite ugly and annoying, because compare_SOP does not exist
+-- with an extra argument ...
 sgeq ::
-  (SGeneric a, All (All (Quoted Eq)) (SDescription a)) =>
-  Code a -> Code a -> Code Bool
-sgeq c1 c2 =
+  SGeneric a =>
+  POP (C :.: Dict Eq) (SDescription a) ->
+  CodeQ a -> CodeQ a -> CodeQ Bool
+sgeq dicts c1 c2 =
   sfrom c1 $ \ a1 -> sfrom c2 $ \ a2 ->
-  ccompare_SOP (Proxy @(Quoted Eq))
-    [|| False ||]
-    (\ xs1 xs2 -> sand (collapse_NP (czipWith_NP (Proxy @(Quoted Eq)) (mapCCK [|| (==) ||]) xs1 xs2)))
-    [|| False ||]
-    a1 a2
+  ccompare_SOP (Proxy @Top)
+    ([|| False ||])
+    (\ xs1 xs2 -> sand (collapse_NP (zipWith_NP (\ (P (Comp (C d)) (C x1)) (C x2) -> K [|| withDict $$d ($$x1 == $$x2) ||]) xs1 xs2)))
+    ([|| False ||])
+    (selectWith_SOP P dicts a1) a2
+
+data P (f :: k -> Type) (g :: k -> Type) (x :: k) = P (f x) (g x)
 
-sand :: [Code Bool] -> Code Bool
+sand :: [CodeQ Bool] -> CodeQ Bool
 sand = foldr (\ x r -> [|| $$x && $$r ||]) [|| True ||]
 
 genum :: (SOP.Generic a, SOP.All ((~) '[]) (SOP.Code a)) => [a]
 genum =
-  SOP.to <$> SOP.apInjs_POP (POP (SOP.cpure_NP (Proxy @((~) '[])) Nil))
+  SOP.to <$> SOP.apInjs_POP (POP (cpure_NP (Proxy @((~) '[])) Nil))
 
-sgenum :: SIsEnumType a => Code [a]
+sgenum :: SIsEnumType a => CodeQ [a]
 sgenum =
   foldr (\ x r -> [|| $$x : $$r ||]) [|| [] ||]
     (sto <$> apInjs_POP (POP (cpure_NP (Proxy @((~) '[])) Nil)))
@@ -150,7 +165,7 @@ ghcgeq a1 a2 = ghcgeq' (from a1) (from a2)
 
 conNumbers :: forall a . (SOP.Generic a) => Proxy a -> NP (K Word) (SOP.Code a)
 conNumbers _ =
-  SOP.ana_NP (\ (K i) -> (K i, K (i + 1))) (K 0)
+  ana_NP (\ (K i) -> (K i, K (i + 1))) (K 0)
 
 sconNumbers :: forall a . (SGeneric a) => Proxy a -> NP (K Word) (SDescription a)
 sconNumbers _ =
@@ -162,7 +177,7 @@ conArities _ =
     go :: forall xs . SOP.SListI xs => K Word xs
     go = K (fromIntegral (SOP.lengthSList (Proxy @xs)))
   in
-    SOP.cpure_NP (Proxy @SOP.SListI) go
+    cpure_NP (Proxy @SOP.SListI) go
 
 sconArities :: forall a . (SGeneric a) => Proxy a -> NP (K Word) (SDescription a)
 sconArities _ =
@@ -172,65 +187,74 @@ sconArities _ =
   in
     cpure_NP (Proxy @SListI) go
 
-
 gencode :: forall a . (SOP.Generic a, SOP.All (SOP.All Serialise) (SOP.Code a)) => a -> Encoding
 gencode x =
   let
     tmp :: SOP (K Encoding) (SOP.Code a)
     tmp =
-      SOP.cmap_SOP (Proxy @Serialise) (SOP.mapIK encode) (SOP.from x)
+      cmap_SOP (Proxy @Serialise) (SOP.mapIK encode) (SOP.from x)
 
     tmp2 :: NS (K Encoding) (SOP.Code a)
     tmp2 =
       SOP.hzipWith3
-        (\ (K i) (K a) es -> K (encodeListLen (a + 1) <> encodeWord i <> mconcat (SOP.collapse_NP es)))
+        (\ (K i) (K a) es -> K (encodeListLen (a + 1) <> encodeWord i <> mconcat (collapse_NP es)))
         (conNumbers (Proxy @a))
         (conArities (Proxy @a))
         (SOP.unSOP tmp)
   in
-    SOP.collapse_NS tmp2
+    collapse_NS tmp2
 
-sgencode :: forall a . (SGeneric a, All (All (Quoted Serialise)) (SDescription a)) => Code (a -> Encoding)
-sgencode =
+sgencode :: forall a . SGeneric a => POP (C :.: Dict Serialise) (SDescription a) -> CodeQ (a -> Encoding)
+sgencode dicts =
   [||
     \ a ->
     $$(sfrom [|| a ||] $ \ a' ->
       let
-        tmp :: SOP (K (Code Encoding)) (SDescription a)
-        tmp =
-          cmap_SOP (Proxy @(Quoted Serialise)) (mapCK [|| encode ||]) a'
-
-        tmp2 :: NS (K (Code Encoding)) (SDescription a)
-        tmp2 =
-          cselectWith_NS
-            (Proxy @(All (Quoted Serialise)))
-            (\ (K (i, a)) es -> let a' = a + 1 in K [|| encodeListLen a' <> encodeWord i <> $$(foldr (\ x y -> [|| $$x <> $$y ||]) [|| mempty ||] (collapse_NP es)) ||])
-            (tmp3 @a) -- (czipWith_NP (Proxy @(All (Quoted Serialise))) (SOP.mapKKK (,)) (sconNumbers (Proxy @a)) (sconArities (Proxy @a)))
-            (unSOP tmp)
-
-        tmp3 :: forall a . (SGeneric a, All (All (Quoted Serialise)) (SDescription a)) => NP (K (Word, Word)) (SDescription a)
+        tmp1 :: SOP (K (CodeQ Encoding)) (SDescription a)
+        tmp1 =
+          selectWith_SOP (\ (Comp (C d)) (C a) -> K [|| withDict $$d (encode $$a) ||]) dicts a'
+
+        tmp2 :: forall a . SGeneric a => Proxy a -> NP (K (Word, Word)) (SDescription a)
+        tmp2 _ =
+          zipWith_NP
+            (\ (K cn) (K ca) -> K (cn, ca))
+            (sconNumbers (Proxy @a)) (sconArities (Proxy @a))
+
+        tmp3 :: NS (K (CodeQ Encoding)) (SDescription a)
         tmp3 =
-          (czipWith_NP (Proxy @(All (Quoted Serialise))) (SOP.mapKKK (,)) (sconNumbers (Proxy @a)) (sconArities (Proxy @a)))
+          selectWith_NS
+            (\ (K (i, a)) es ->
+              let
+                a' = a + 1
+              in
+                K [||
+                     encodeListLen a'
+                  <> encodeWord i
+                  <> $$(foldr (\ x y -> [|| $$x <> $$y ||]) [|| mempty ||] (collapse_NP es))
+                ||]
+            )
+            (tmp2 (Proxy @a))
+            (unSOP tmp1)
       in
-        collapse_NS tmp2
+        collapse_NS tmp3
     )
   ||]
 
-gdecode :: forall a s . (SOP.Generic a, SOP.All (SOP.All Serialise) (SOP.Code a)) => Decoder s a
+gdecode :: forall a s . (SOP.Generic a, All (All Serialise) (SOP.Code a)) => Decoder s a
 gdecode =
   let
     tmp :: POP (Decoder s) (SOP.Code a)
     tmp =
-      SOP.cpure_POP (Proxy @Serialise) decode
+      cpure_POP (Proxy @Serialise) decode
 
     tmp2 :: NP (K (SOP (Decoder s) (SOP.Code a))) (SOP.Code a)
     tmp2 =
-      SOP.apInjs'_POP tmp
+      apInjs'_POP tmp
 
     tmp3 :: NP (K ((Word, Word), Decoder s a)) (SOP.Code a)
     tmp3 =
-      SOP.zipWith3_NP
-        (\ (K i) (K a) (K dec) -> K ((a + 1, i), SOP.to <$> SOP.sequence_SOP dec))
+      zipWith3_NP
+        (\ (K i) (K a) (K dec) -> K ((a + 1, i), SOP.to <$> sequence_SOP dec))
         (conNumbers (Proxy @a))
         (conArities (Proxy @a))
         tmp2
@@ -242,34 +266,36 @@ gdecode =
         Just dec -> dec
         Nothing  -> fail "invalid encoding"
 
-sgdecode :: forall a s . (SGeneric a, LiftT s, All (All (Quoted Serialise)) (SDescription a), All (And (All LiftT) (AllTails (LiftTCurry a))) (SDescription a)) => Code (Decoder s a)
-sgdecode =
+dApplicativeDecoder :: Dict Applicative (Decoder s)
+dApplicativeDecoder = Dict
+
+sgdecode :: forall a s . SGeneric a => POP (C :.: Dict Serialise) (SDescription a) -> CodeQ (Decoder s a)
+sgdecode dicts =
   let
     tmp :: POP (C :.: Decoder s) (SDescription a)
     tmp =
-      cpure_POP (Proxy @(Quoted Serialise)) (Comp (C [|| decode ||]))
+      map_POP (\ (Comp (C d)) -> Comp (C [|| withDict $$d decode ||])) dicts
 
     tmp2 :: NP (K (SOP (C :.: Decoder s) (SDescription a))) (SDescription a)
     tmp2 =
       apInjs'_POP tmp
 
-    tmp3 :: NP (K ((Word, Word), Code (Decoder s a))) (SDescription a)
+    tmp3 :: NP (K ((Word, Word), CodeQ (Decoder s a))) (SDescription a)
     tmp3 =
-      czipWith_NP
-        (Proxy @(All (Quoted Serialise)))
-        (\ (K (i, a)) (K dec) -> K ((a + 1, i), stoA dec))
-        (tmp3' @a)
+      zipWith_NP
+        (\ (K (i, a)) (K dec) -> K ((a + 1, i), stoA [|| dApplicativeDecoder ||] dec))
+        (tmp3' (Proxy @a))
         tmp2
 
-    tmp3' :: forall a . (SGeneric a, All (All (Quoted Serialise)) (SDescription a)) => NP (K (Word, Word)) (SDescription a)
-    tmp3' =
-      (czipWith_NP (Proxy @(All (Quoted Serialise))) (SOP.mapKKK (,)) (sconNumbers (Proxy @a)) (sconArities (Proxy @a)))
+    tmp3' :: forall a . SGeneric a => Proxy a -> NP (K (Word, Word)) (SDescription a)
+    tmp3' _ =
+      zipWith_NP (SOP.mapKKK (,)) (sconNumbers (Proxy @a)) (sconArities (Proxy @a))
 
-    tmp4 :: [((Word, Word), Code (Decoder s a))]
+    tmp4 :: [((Word, Word), CodeQ (Decoder s a))]
     tmp4 =
       collapse_NP tmp3
 
-    tmp5 :: Code (Word, Word) -> [((Word, Word), Code (Decoder s a))] -> Code (Decoder s a)
+    tmp5 :: CodeQ (Word, Word) -> [((Word, Word), CodeQ (Decoder s a))] -> CodeQ (Decoder s a)
     tmp5 _sym []                  = [|| fail "invalid encoding" ||]
     tmp5 sym ((key, rhs) : cases) =
       [|| if $$sym == key then $$rhs else $$(tmp5 sym cases) ||]
diff --git a/staged-sop-examples/src/ExampleTypes.hs b/staged-sop-examples/src/ExampleTypes.hs
index a49f7c4..f3e85be 100644
--- a/staged-sop-examples/src/ExampleTypes.hs
+++ b/staged-sop-examples/src/ExampleTypes.hs
@@ -21,6 +21,8 @@ SOP.deriveGeneric ''Foo
 
 instance SGeneric Foo where
   type SDescription Foo = SOP.Code Foo
+  type Constraints c Foo = (c [Int], c Ordering, c Text)
+  data ConstraintsD c Foo = CFoo !(Dict c [Int]) !(Dict c Ordering) !(Dict c Text)
 
   sfrom c k =
     [|| case $$c of
@@ -29,6 +31,14 @@ instance SGeneric Foo where
 
   sto (SOP (Z (C is :* C o :* C txt :* Nil))) = [|| Foo $$is $$o $$txt ||]
 
+  constraints =
+    CFoo Dict Dict Dict
+  allC c =
+    POP $
+      (  Comp (C [|| case $$c of CFoo d _ _ -> d ||])
+      :* Comp (C [|| case $$c of CFoo _ d _ -> d ||])
+      :* Comp (C [|| case $$c of CFoo _ _ d -> d ||]) :* Nil) :* Nil
+
 instance NFData Foo where
   rnf (Foo is o txt) = rnf is `seq` rnf o `seq` rnf txt
 
@@ -42,8 +52,10 @@ data Tree (tag :: Tag) a = Leaf a | Node (Tree tag a) (Tree tag a)
 
 SOP.deriveGeneric ''Tree
 
-instance (LiftT a, LiftT tag) => SGeneric (Tree tag a) where
+instance SGeneric (Tree tag a) where
   type SDescription (Tree tag a) = SOP.Code (Tree tag a)
+  type Constraints c (Tree tag a) = (c a, c (Tree tag a))
+  data ConstraintsD c (Tree tag a) = CTree !(Dict c a) !(Dict c (Tree tag a))
 
   sfrom c k =
     [|| case $$c of
@@ -54,6 +66,18 @@ instance (LiftT a, LiftT tag) => SGeneric (Tree tag a) where
   sto (SOP (Z (C a :* Nil)))            = [|| Leaf $$a ||]
   sto (SOP (S (Z (C l :* C r :* Nil)))) = [|| Node $$l $$r ||]
 
+  constraints =
+    CTree Dict Dict
+  allC c =
+    let
+      da = Comp (C [|| case $$c of CTree d _ -> d ||])
+      dt = Comp (C [|| case $$c of CTree _ d -> d ||])
+    in
+      POP $
+           (da :* Nil)
+        :* (dt :* dt :* Nil)
+        :* Nil
+
 instance NFData a => NFData (Tree tag a) where
   rnf (Leaf a) = rnf a
   rnf (Node l r) = rnf l `seq` rnf r
@@ -63,8 +87,10 @@ data Pair a b = Pair a b
 
 SOP.deriveGeneric ''Pair
 
-instance (LiftT a, LiftT b) => SGeneric (Pair a b) where
+instance SGeneric (Pair a b) where
   type SDescription (Pair a b) = '[ '[ a, b ] ]
+  type Constraints c (Pair a b) = (c a, c b)
+  data ConstraintsD c (Pair a b) = CPair !(Dict c a) !(Dict c b)
 
   sfrom c k =
     [|| case $$c of
@@ -73,11 +99,24 @@ instance (LiftT a, LiftT b) => SGeneric (Pair a b) where
 
   sto (SOP (Z (C a :* C b :* Nil))) = [|| Pair $$a $$b ||]
 
+  constraints =
+    CPair Dict Dict
+  allC c =
+    let
+      da = Comp (C [|| case $$c of CPair d _ -> d ||])
+      db = Comp (C [|| case $$c of CPair _ d -> d ||])
+    in
+      POP $
+           (da :* db :* Nil)
+        :* Nil
+
 instance (NFData a, NFData b) => NFData (Pair a b) where
   rnf (Pair a b) = rnf a `seq` rnf b
 
 instance SGeneric Ordering where
   type SDescription Ordering = '[ '[], '[], '[] ]
+  type Constraints c Ordering = ()
+  data ConstraintsD c Ordering = COrdering
 
   sfrom c k =
     [|| case $$c of
@@ -90,6 +129,11 @@ instance SGeneric Ordering where
   sto (SOP (S (Z Nil)))     = [|| EQ ||]
   sto (SOP (S (S (Z Nil)))) = [|| GT ||]
 
+  constraints =
+    COrdering
+  allC _ =
+    POP $ Nil :* Nil :* Nil :* Nil
+
 data Person = Person { personId :: Int, name :: String, date :: Day }
   deriving GHC.Generic
 
@@ -97,6 +141,8 @@ SOP.deriveGeneric ''Person
 
 instance SGeneric Person where
   type SDescription Person = '[ '[ Int, String, Day ] ]
+  type Constraints c Person = (c Int, c String, c Day)
+  data ConstraintsD c Person = CPerson !(Dict c Int) !(Dict c String) !(Dict c Day)
 
   sfrom c k =
     [|| case $$c of
@@ -105,6 +151,18 @@ instance SGeneric Person where
 
   sto (SOP (Z (C i :* C n :* C d :* Nil))) = [|| Person $$i $$n $$d ||]
 
+  constraints =
+    CPerson Dict Dict Dict
+  allC c =
+    let
+      di = Comp (C [|| case $$c of CPerson d _ _ -> d ||])
+      ds = Comp (C [|| case $$c of CPerson _ d _ -> d ||])
+      dd = Comp (C [|| case $$c of CPerson _ _ d -> d ||])
+    in
+      POP $
+           (di :* ds :* dd :* Nil)
+        :* Nil
+
 instance NFData Person where
   rnf (Person i n d) = rnf i `seq` rnf n `seq` rnf d
 
@@ -119,8 +177,10 @@ data Prop (tag :: Tag) =
 
 SOP.deriveGeneric ''Prop
 
-instance LiftT tag => SGeneric (Prop tag) where
+instance SGeneric (Prop tag) where
   type SDescription (Prop tag) = SOP.Code (Prop tag)
+  type Constraints c (Prop tag) = (c String, c (Prop tag))
+  data ConstraintsD c (Prop tag) = CProp !(Dict c String) !(Dict c (Prop tag))
 
   sfrom c k =
     [|| case $$c of
@@ -139,6 +199,22 @@ instance LiftT tag => SGeneric (Prop tag) where
   sto (SOP (S (S (S (S (Z (C p1 :* C p2 :* Nil)))))))     = [|| And $$p1 $$p2 ||]
   sto (SOP (S (S (S (S (S (Z (C p1 :* C p2 :* Nil)))))))) = [|| Or $$p1 $$p2 ||]
 
+  constraints =
+    CProp Dict Dict
+  allC c =
+    let
+      ds = Comp (C [|| case $$c of CProp d _ -> d ||])
+      dp = Comp (C [|| case $$c of CProp _ d -> d ||])
+    in
+      POP $
+           (ds :* Nil)
+        :* Nil
+        :* Nil
+        :* (dp :* Nil)
+        :* (dp :* dp :* Nil)
+        :* (dp :* dp :* Nil)
+        :* Nil
+
 instance NFData (Prop tag) where
   rnf (Var s) = rnf s
   rnf T = ()
@@ -189,6 +265,8 @@ SOP.deriveGeneric ''S15
 
 instance SGeneric S15 where
   type SDescription S15 = SOP.Code S15
+  type Constraints c S15 = ()
+  data ConstraintsD c S15 = CS15
 
   sfrom c k =
     [|| case $$c of
@@ -225,6 +303,27 @@ instance SGeneric S15 where
   sto (SOP (S (S (S (S (S (S (S (S (S (S (S (S (S (Z Nil)))))))))))))))     = [|| S15_13 ||]
   sto (SOP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (Z Nil)))))))))))))))) = [|| S15_14 ||]
 
+  constraints =
+    CS15
+  allC _ =
+    POP $
+       Nil
+    :* Nil
+    :* Nil
+    :* Nil
+    :* Nil
+    :* Nil
+    :* Nil
+    :* Nil
+    :* Nil
+    :* Nil
+    :* Nil
+    :* Nil
+    :* Nil
+    :* Nil
+    :* Nil
+    :* Nil
+
 tree :: Tree tag Int
 tree = Node (Node (Leaf 1) (Leaf 2)) (Node (Leaf 3) (Leaf 4))
 
diff --git a/staged-sop/src/Generics/SOP/Staged.hs b/staged-sop/src/Generics/SOP/Staged.hs
index 026e0f5..a0ff2e7 100644
--- a/staged-sop/src/Generics/SOP/Staged.hs
+++ b/staged-sop/src/Generics/SOP/Staged.hs
@@ -23,11 +23,11 @@ import Data.Kind
 import Data.Proxy as X
 import Data.SOP.BasicFunctors as X
 import Data.SOP.Classes
-import Data.SOP.Constraint (And, Top)
+import Data.SOP.Constraint (And, All, Top, SListI, ccase_SList)
 -- import Data.SOP.Constraint hiding (SListI(..))
-import Data.SOP.Dict as X (Dict(..), withDict)
-import Data.SOP.NP as X (NP(..), POP(..), unPOP)
-import Data.SOP.NS as X (NS(..), SOP(..), unSOP)
+import Data.SOP.Dict as X (Dict(..), withDict, hdicts)
+import Data.SOP.NP as X (NP(..), POP(..), unPOP, map_NP, hd)
+import Data.SOP.NS as X (NS(..), SOP(..), unSOP, map_NS, cmap_NS, collapse_NS, injections)
 -- import Generics.SOP hiding (CodeQ)
 import Language.Haskell.TH (CodeQ, TExp)
 
@@ -44,24 +44,33 @@ mapCK op (C a) = K [|| $$op $$a ||]
 
 -- | Still undecided about the name, but going to use an s-prefix for now to
 -- clearly disambiguate.
+--
+-- NOTE: The decision to flatten the constraints in Constraints and ConstraintsD
+-- is necessary to ensure the limited overhead we will introduce into the generated
+-- code will be optimised away completely.
+--
 class ( SListI (SDescription a), All SListI (SDescription a)
       -- , All (All LiftT `And` AllTails (LiftTCurry a)) (SDescription a) -- needed for stoA, hiding it here for now
       ) => SGeneric a where
   type SDescription a :: [[Type]] -- there's an argument to call this 'Description' in any case, because it's unchanged
+  type Constraints (c :: Type -> Constraint) a :: Constraint -- flattened list of constraints
+  data ConstraintsD (c :: Type -> Constraint) a -- flattended product of dictionaries
+  -- newtype Constraints c a = Constraints (POP (C :.: Dict c) (SDescription a)) -- morally correct implementation, but we choose a simpler one
+
   sfrom :: CodeQ a -> (SRep a -> CodeQ r) -> CodeQ r
   sto :: SRep a -> CodeQ a
 
-type SListI = All Top
+  constraints :: Constraints c a => ConstraintsD c a -- outside top-level splice
+  allC :: CodeQ (ConstraintsD c a) -> POP (C :.: Dict c) (SDescription a) -- inside top-level splice
+
+pallC :: SIsProductType a xs => CodeQ (ConstraintsD c a) -> NP (C :.: Dict c) xs
+pallC d = hd $ unPOP $ allC d
+
 type SRep a = SOP C (SDescription a)
 
 type SIsProductType a xs = (SGeneric a, SDescription a ~ '[ xs ])
 type SIsEnumType a = (SGeneric a, All ((~) '[]) (SDescription a))
 
-{-
-class (CodeC (c a), LiftT a) => Quoted (c :: k -> Constraint) (a :: k)
-instance (CodeC (c a), LiftT a) => Quoted c a
--}
-
 sproductTypeFrom :: (SIsProductType a xs) => CodeQ a -> (NP C xs -> CodeQ r) -> CodeQ r
 sproductTypeFrom c k =
   sfrom c $ \ (SOP (Z xs)) -> k xs
@@ -106,234 +115,45 @@ scurry_NP =
     SNil  -> \ f -> f Nil
     SCons -> \ f -> [|| \ x -> $$(scurry_NP (\ xs -> f (C [|| x ||] :* xs))) ||]
 
-type Injection (f :: k -> Type) (xs :: [k]) = f -.-> K (NS f xs)
-
-injections :: forall xs f. SListI xs => NP (Injection f xs) xs
-injections = case sList :: SList xs of
-  SNil   -> Nil
-  SCons  -> fn (K . Z) :* map_NP shiftInjection injections
-
-shiftInjection :: Injection f xs a -> Injection f (x ': xs) a
-shiftInjection (Fn f) = Fn $ K . S . unK . f
-
-{-
-stoA ::
-  forall a f . (SGeneric a, Quoted Applicative f, All (All LiftT `And` AllTails (LiftTCurry a)) (SDescription a)) =>
-  SOP (C :.: f) (SDescription a) -> CodeQ (f a)
-stoA (SOP sop) =
+stoA :: forall a f . SGeneric a => CodeQ (Dict Applicative f) -> SOP (C :.: f) (SDescription a) -> CodeQ (f a)
+stoA d (SOP sop) =
   let
-    go :: forall xs . (All LiftT xs, AllTails (LiftTCurry a) xs) => CodeQ (f (Curry a xs)) -> NP (C :.: f) xs -> CodeQ (f a)
+    go :: forall xs . CodeQ (f (Curry a xs)) -> NP (C :.: f) xs -> CodeQ (f a)
     go acc Nil                = acc
-    go acc (Comp (C x) :* xs) = go [|| $$acc <*> $$x ||] xs
+    go acc (Comp (C x) :* xs) = go [|| withDict $$d ($$acc <*> $$x) ||] xs
   in
     collapse_NS $
-      cselectWith_NS (Proxy @(All LiftT `And` AllTails (LiftTCurry a)))
-        (\ (Fn inj) -> K . go [|| pure $$(scurry_NP @a $ sto . SOP . unK . inj) ||])
+      cselectWith_NS (Proxy @SListI)
+        (\ (Fn inj) -> K . go [|| withDict $$d (pure $$(scurry_NP @a $ sto . SOP . unK . inj)) ||])
         (injections @(SDescription a) @(NP C))
         sop
--}
 
-{-
 sproductTypeToA ::
-  forall a f xs . (SIsProductType a xs, Quoted Applicative f, AllTails (LiftTCurry a) xs) =>
-  NP (C :.: f) xs -> CodeQ (f a)
-sproductTypeToA =
-  go [|| pure $$(scurry_NP (sproductTypeTo @a)) ||]
+  forall a f xs . SIsProductType a xs => CodeQ (Dict Applicative f) -> NP (C :.: f) xs -> CodeQ (f a)
+sproductTypeToA d =
+  go [|| withDict $$d (pure $$(scurry_NP (sproductTypeTo @a))) ||]
   where
-    go :: forall ys . (All LiftT ys, AllTails (LiftTCurry a) ys) => CodeQ (f (Curry a ys)) -> NP (C :.: f) ys -> CodeQ (f a)
+    go :: forall ys . CodeQ (f (Curry a ys)) -> NP (C :.: f) ys -> CodeQ (f a)
     go acc Nil                  = acc
-    go acc (Comp (C fx) :* fxs) = go [|| $$acc <*> $$fx ||] fxs
+    go acc (Comp (C fx) :* fxs) = go [|| withDict $$d ($$acc <*> $$fx) ||] fxs
 
 senumTypeToA ::
-  forall a f xs . (SIsEnumType a, Quoted Applicative f, All (All LiftT `And` AllTails (LiftTCurry a)) (SDescription a)) =>
-  NS (K ()) (SDescription a) -> CodeQ (f a)
-senumTypeToA ns =
-  stoA (SOP (cmap_NS (Proxy @((~) '[])) (const Nil) ns))
--}
-
-dictImplies :: (SListI xs, forall x . c x => d x) => Dict (All c) xs -> Dict (All d) xs
-dictImplies =
-  dictImplies' (\ Dict -> Dict)
-
-dictImplies' :: SListI xs => (forall x . Dict c x -> Dict d x) -> Dict (All c) xs -> Dict (All d) xs
-dictImplies' f dict =
-  all_NP (map_NP f (unAll_NP dict))
-
-all_NP :: NP (Dict c) xs -> Dict (All c) xs
-all_NP Nil          = Dict
-all_NP (Dict :* ds) = withDict (all_NP ds) Dict
-
-unAll_NP :: Dict (All c) xs -> NP (Dict c) xs
-unAll_NP d = withDict d dicts_NP
-
--- Stuff we currently reproduce from sop-core
-
-class AllF c xs => All (c :: k -> Constraint) xs where
-  cpara_SList ::
-       proxy c
-    -> r '[]
-    -> (forall y ys . (c y, All c ys) => r ys -> r (y ': ys))
-    -> r xs
-  dicts_NP :: NP (Dict c) xs
-  cpure_NP' :: (forall x . c x => f x) -> NP f xs
-
-instance All c '[] where
-  cpara_SList _p nil _cons = nil
-  dicts_NP = Nil
-  cpure_NP' p = Nil
-
-instance (c x, All c xs) => All c (x : xs) where
-  cpara_SList p nil cons =
-    cons (cpara_SList p nil cons)
-  dicts_NP = Dict :* dicts_NP
-  cpure_NP' p = p :* cpure_NP' @_ @c p
-
-type family AllF (c :: k -> Constraint) (xs :: [k]) :: Constraint where
-  AllF c '[] = ()
-  AllF c (x : xs) = (c x, All c xs)
-
-ccase_SList ::
-     All c xs
-  => proxy c
-  -> r '[]
-  -> (forall y ys . (c y, All c ys) => r (y ': ys))
-  -> r xs
-ccase_SList p nil cons =
-  cpara_SList p nil (const cons)
-
-cmap_NP :: forall c f g xs . All c xs => Proxy c -> (forall x . c x => f x -> g x) -> NP f xs -> NP g xs
-cmap_NP _ f Nil       = Nil
-cmap_NP p f (x :* xs) = f x :* cmap_NP p f xs
-
-map_NP :: forall f g xs . SListI xs => (forall x . f x -> g x) -> NP f xs -> NP g xs
-map_NP = cmap_NP (Proxy @Top)
-
-cmap_NS :: forall c f g xs . All c xs => Proxy c -> (forall x . c x => f x -> g x) -> NS f xs -> NS g xs
-cmap_NS _ f (Z x) = Z (f x)
-cmap_NS p f (S y) = S (cmap_NS p f y)
+  forall a f xs . SIsEnumType a => CodeQ (Dict Applicative f) -> NS (K ()) (SDescription a) -> CodeQ (f a)
+senumTypeToA d ns =
+  stoA d (SOP (cmap_NS (Proxy @((~) '[])) (const Nil) ns))
 
-map_NS :: forall f g xs . SListI xs => (forall x . f x -> g x) -> NS f xs -> NS g xs
-map_NS = cmap_NS (Proxy @Top)
+-- Stuff we should actually define in sop-core
+--
 
-cmap_SOP :: forall c f g xss . All (All c) xss => Proxy c -> (forall x . c x => f x -> g x) -> SOP f xss -> SOP g xss
-cmap_SOP p f (SOP sop) = SOP (cmap_NS (Proxy @(All c)) (cmap_NP (Proxy @c) f) sop)
+cselectWith_SOP :: forall c f g h xs . All (All c) xs => Proxy c -> (forall x . c x => f x -> g x -> h x) -> POP f xs -> SOP g xs -> SOP h xs
+cselectWith_SOP p op = hczipWith p op
 
-czipWith_NP :: forall c f g h xs . All c xs => Proxy c -> (forall x . c x => f x -> g x -> h x) -> NP f xs -> NP g xs -> NP h xs
-czipWith_NP p f xs ys = cpure_NP p (Fn $ \x -> Fn $ \ y -> f x y) `ap_NP` xs `ap_NP` ys
+selectWith_SOP :: forall f g h xs . All SListI xs => (forall x . f x -> g x -> h x) -> POP f xs -> SOP g xs -> SOP h xs
+selectWith_SOP p op = hzipWith p op
 
 cselectWith_NS :: forall c f g h xs . All c xs => Proxy c -> (forall x . c x => f x -> g x -> h x) -> NP f xs -> NS g xs -> NS h xs
-cselectWith_NS _ f (x :* _)  (Z y) = Z (f x y)
-cselectWith_NS p f (_ :* xs) (S i) = S (cselectWith_NS p f xs i)
+cselectWith_NS p op = hczipWith p op
 
 selectWith_NS :: forall f g h xs . SListI xs => (forall x . f x -> g x -> h x) -> NP f xs -> NS g xs -> NS h xs
-selectWith_NS = cselectWith_NS (Proxy @Top)
+selectWith_NS p op = hzipWith p op
 
-cpure_POP :: forall c f xss . All (All c) xss => Proxy c -> (forall x . c x => f x) -> POP f xss
-cpure_POP _ f = POP (cpure_NP (Proxy @(All c)) (cpure_NP (Proxy @c) f))
-
-cpure_NP :: forall c f xs . All c xs => Proxy c -> (forall x . c x => f x) -> NP f xs
-cpure_NP _ f = cpure_NP' @_ @c f
-
-pure_NP :: forall f xs . SListI xs => (forall x . f x) -> NP f xs
-pure_NP p = cpure_NP (Proxy @Top) p
-
-ap_NP :: NP (f -.-> g) xs -> NP f xs -> NP g xs
-ap_NP Nil       Nil       = Nil
-ap_NP (f :* fs) (x :* xs) = apFn f x :* ap_NP fs xs
-
-collapse_NP :: NP (K a) xs -> [a]
-collapse_NP Nil         = []
-collapse_NP (K a :* xs) = a : collapse_NP xs
-
-collapse_NS :: NS (K a) xs -> a
-collapse_NS (Z (K x)) = x
-collapse_NS (S i)     = collapse_NS i
-
-collapse_SOP :: SOP (K a) xs -> [a]
-collapse_SOP (SOP (Z xs)) = collapse_NP xs
-collapse_SOP (SOP (S i))  = collapse_SOP (SOP i)
-
-ccompare_NS ::
-     forall c proxy r f g xs .
-     (All c xs)
-  => proxy c
-  -> r                                    -- ^ what to do if first is smaller
-  -> (forall x . c x => f x -> g x -> r)  -- ^ what to do if both are equal
-  -> r                                    -- ^ what to do if first is larger
-  -> NS f xs -> NS g xs
-  -> r
-ccompare_NS _ lt eq gt = go
-  where
-    go :: forall ys . (All c ys) => NS f ys -> NS g ys -> r
-    go (Z x)  (Z y)  = eq x y
-    go (Z _)  (S _)  = lt
-    go (S _)  (Z _)  = gt
-    go (S xs) (S ys) = go xs ys
-
-ccompare_SOP ::
-     forall c proxy r f g xss .
-     (All (All c) xss)
-  => proxy c
-  -> r                                                  -- ^ what to do if first is smaller
-  -> (forall xs . All c xs => NP f xs -> NP g xs -> r)  -- ^ what to do if both are equal
-  -> r                                                  -- ^ what to do if first is larger
-  -> SOP f xss -> SOP g xss
-  -> r
-ccompare_SOP _ lt eq gt (SOP xs) (SOP ys) =
-  ccompare_NS (Proxy @(All c)) lt eq gt xs ys
-
-apInjs'_NP :: SListI xs => NP f xs -> NP (K (NS f xs)) xs
-apInjs'_NP = ap_NP injections
-
-apInjs_NP :: SListI xs => NP f xs -> [NS f xs]
-apInjs_NP = collapse_NP . apInjs'_NP
-
-apInjs_POP :: forall k (f :: k -> Type) (xss :: [[k]]) . SListI xss => POP f xss -> [SOP f xss]
-apInjs_POP = map SOP . apInjs_NP . unPOP
-
-apInjs'_POP :: forall k (f :: k -> Type) (xss :: [[k]]) . SListI xss => POP f xss -> NP (K (SOP f xss)) xss
-apInjs'_POP = map_NP (K . SOP . unK) . ap_NP injections . unPOP
-
-ana_NP ::
-     forall s f xs .
-     SListI xs
-  => (forall y ys . s (y ': ys) -> (f y, s ys))
-  -> s xs
-  -> NP f xs
-ana_NP uncons = go sList
-  where
-    go :: forall ys . SList ys -> s ys -> NP f ys
-    go SNil  _ = Nil
-    go SCons s = case uncons s of
-      (x, s') -> x :* go sList s'
-
-{-
-cana_NP ::
-   forall c proxy s f xs . (All c xs)
-=> proxy c
--> (forall y ys . c y => s (y ': ys) -> (f y, s ys))
--> s xs
--> NP f xs
-cana_NP _ uncons = go sList
-where
-  go :: forall ys . (All c ys) => SList ys -> s ys -> NP f ys
-  go SNil  _ = Nil
-  go SCons s = case uncons s of
-    (x, s') -> x :* go sList s'
--}
-
-data Shape :: [k] -> Type where
-  ShapeNil  :: Shape '[]
-  ShapeCons :: SListI xs => Shape xs -> Shape (x ': xs)
-
-shape :: forall k (xs :: [k]). SListI xs => Shape xs
-shape = case sList :: SList xs of
-          SNil  -> ShapeNil
-          SCons -> ShapeCons shape
-
-lengthSList :: forall k (xs :: [k]) proxy. SListI xs => proxy xs -> Int
-lengthSList _ = lengthShape (shape :: Shape xs)
-  where
-    lengthShape :: forall xs'. Shape xs' -> Int
-    lengthShape ShapeNil      = 0
-    lengthShape (ShapeCons s) = 1 + lengthShape s