diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,3 +1,13 @@
+0.6
+-------------------------------------------------
+* Added a MonadCont instance for Eff
+* `(:*)` and `(:|)` are deprecated in favour of `(:&)` and `(:*)` where their
+  type parameters are flipped
+* Flipped the type parameters of `BitProd` and `TangleT`
+* Added `itemKey`, `hmapWithIndexWith`, `hfoldMapWith`, `hfoldMapWithIndexWith`,
+  `hfoldrWithIndexWith`, `hfoldlWithIndexWith`, `hrepeatWith`, `htabulateWith`,
+  and `hgenerateWith`
+
 0.5.1
 -------------------------------------------------
 * Split `Data.Extensible.HList` and `Data.Extensible.Internal` to the
diff --git a/extensible.cabal b/extensible.cabal
--- a/extensible.cabal
+++ b/extensible.cabal
@@ -1,5 +1,5 @@
 name:                extensible
-version:             0.5.1
+version:             0.6
 synopsis:            Extensible, efficient, optics-friendly data types and effects
 homepage:            https://github.com/fumieval/extensible
 bug-reports:         http://github.com/fumieval/extensible/issues
@@ -67,6 +67,7 @@
     , CPP
   build-depends:       base >= 4.8 && <5
     , aeson
+    , barbies
     , bytestring
     , cassava
     , comonad
diff --git a/src/Data/Extensible/Bits.hs b/src/Data/Extensible/Bits.hs
--- a/src/Data/Extensible/Bits.hs
+++ b/src/Data/Extensible/Bits.hs
@@ -45,10 +45,10 @@
 import GHC.TypeLits
 
 -- | Bit-vector product. It has similar interface as @(:*)@ but fields are packed into @r@.
-newtype BitProd r (h :: k -> Type) (xs :: [k]) = BitProd { unBitProd :: r }
+newtype BitProd r (xs :: [k]) (h :: k -> Type) = BitProd { unBitProd :: r }
   deriving (Eq, Ord, Enum, Bounded, Ix, Generic, Hashable, Storable)
 
-instance (Forall (Instance1 Show h) xs, BitFields r h xs) => Show (BitProd r h xs) where
+instance (Forall (Instance1 Show h) xs, BitFields r xs h) => Show (BitProd r xs h) where
   showsPrec d x = showParen (d > 10)
     $ showString "toBitProd " . showsPrec 11 (fromBitProd x)
 
@@ -143,41 +143,41 @@
   fromBits = Field . fromBits
   toBits = toBits . getField
 
-instance (Bits r, KnownNat (TotalBits h xs)) => FromBits r (BitProd r h xs) where
-  type BitWidth (BitProd r h xs) = TotalBits h xs
+instance (Bits r, KnownNat (TotalBits h xs)) => FromBits r (BitProd r xs h) where
+  type BitWidth (BitProd r xs h) = TotalBits h xs
   fromBits = BitProd
   toBits = unBitProd
 
 -- | Fields are instances of 'FromBits' and fit in the representation.
-type BitFields r h xs = (FromBits r r
+type BitFields r xs h = (FromBits r r
   , TotalBits h xs <= BitWidth r
   , Forall (Instance1 (FromBits r) h) xs)
 
 -- | Convert a normal extensible record into a bit record.
-toBitProd :: forall r h xs. BitFields r h xs => h :* xs -> BitProd r h xs
+toBitProd :: forall r xs h. BitFields r xs h => xs :& h -> BitProd r xs h
 toBitProd p = hfoldrWithIndexFor (Proxy :: Proxy (Instance1 (FromBits r) h))
   (\i v f r -> f $! bupdate i r v) id p (BitProd zeroBits)
 {-# INLINE toBitProd #-}
 
 -- | Convert a normal extensible record into a bit record.
-fromBitProd :: forall r h xs. BitFields r h xs => BitProd r h xs -> h :* xs
+fromBitProd :: forall r xs h. BitFields r xs h => BitProd r xs h -> xs :& h
 fromBitProd p = htabulateFor (Proxy :: Proxy (Instance1 (FromBits r) h))
   $ flip blookup p
 {-# INLINE fromBitProd #-}
 
 -- | 'hlookup' for 'BitProd'
-blookup :: forall x r h xs.
-  (BitFields r h xs, FromBits r (h x))
-  => Membership xs x -> BitProd r h xs -> h x
+blookup :: forall x r xs h.
+  (BitFields r xs h, FromBits r (h x))
+  => Membership xs x -> BitProd r xs h -> h x
 blookup i (BitProd r) = fromBits $ unsafeShiftR r
   $ bitOffsetAt (Proxy :: Proxy r) (Proxy :: Proxy h) (Proxy :: Proxy xs)
   $ getMemberId i
 {-# INLINE blookup #-}
 
 -- | Update a field of a 'BitProd'.
-bupdate :: forall x r h xs.
-  (BitFields r h xs, FromBits r (h x))
-  => Membership xs x -> BitProd r h xs -> h x -> BitProd r h xs
+bupdate :: forall x r xs h.
+  (BitFields r xs h, FromBits r (h x))
+  => Membership xs x -> BitProd r xs h -> h x -> BitProd r xs h
 bupdate i (BitProd r) a = BitProd $ r .&. mask
   .|. unsafeShiftL (toBits a) offset
   where
@@ -201,13 +201,13 @@
 proxyBitWidth _ _ = Proxy
 
 -- | Bit-packed record
-type BitRecordOf r h = BitProd r (Field h)
+type BitRecordOf r h xs = BitProd r xs (Field h)
 
 -- | Bit-packed record
-type BitRecord r = BitRecordOf r Identity
+type BitRecord r xs = BitRecordOf r Identity xs
 
 instance (Corepresentable p, Comonad (Corep p), Functor f) => Extensible f p (BitProd r) where
-  type ExtensibleConstr (BitProd r) h xs x
-    = (BitFields r h xs, FromBits r (h x))
+  type ExtensibleConstr (BitProd r) xs h x
+    = (BitFields r xs h, FromBits r (h x))
   pieceAt i pafb = cotabulate $ \ws -> bupdate i (extract ws) <$> cosieve pafb (blookup i <$> ws)
   {-# INLINE pieceAt #-}
diff --git a/src/Data/Extensible/Class.hs b/src/Data/Extensible/Class.hs
--- a/src/Data/Extensible/Class.hs
+++ b/src/Data/Extensible/Class.hs
@@ -1,4 +1,6 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
 {-# LANGUAGE MultiParamTypeClasses, UndecidableInstances, ScopedTypeVariables, TypeFamilies #-}
+{-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE UndecidableSuperClasses #-}
 -----------------------------------------------------------------------------
 -- |
@@ -17,6 +19,7 @@
   , itemAt
   , item
   , itemAssoc
+  , itemKey
   -- * Membership
   , Membership
   , mkMembership
@@ -48,36 +51,42 @@
 import Type.Membership.Internal
 
 -- | This class allows us to use 'pieceAt' for both sums and products.
-class (Functor f, Profunctor p) => Extensible f p (t :: (k -> *) -> [k] -> *) where
-  type ExtensibleConstr t (h :: k -> *) (xs :: [k]) (x :: k) :: Constraint
-  type ExtensibleConstr t h xs x = ()
-  pieceAt :: ExtensibleConstr t h xs x => Membership xs x -> Optic' p f (t h xs) (h x)
+class (Functor f, Profunctor p) => Extensible f p (t :: [k] -> (k -> *) -> *) where
+  type ExtensibleConstr t (xs :: [k]) (h :: k -> *) (x :: k) :: Constraint
+  type ExtensibleConstr t xs h x = ()
+  pieceAt :: ExtensibleConstr t xs h x => Membership xs x -> Optic' p f (t xs h) (h x)
 
 -- | Accessor for an element.
-piece :: (x ∈ xs, Extensible f p t, ExtensibleConstr t h xs x) => Optic' p f (t h xs) (h x)
+piece :: (x ∈ xs, Extensible f p t, ExtensibleConstr t xs h x) => Optic' p f (t xs h) (h x)
 piece = pieceAt membership
 {-# INLINE piece #-}
 
 -- | Like 'piece', but reckon membership from its key.
-pieceAssoc :: (Lookup xs k v, Extensible f p t, ExtensibleConstr t h xs (k ':> v)) => Optic' p f (t h xs) (h (k ':> v))
+pieceAssoc :: (Lookup xs k v, Extensible f p t, ExtensibleConstr t xs h (k ':> v)) => Optic' p f (t xs h) (h (k ':> v))
 pieceAssoc = pieceAt association
 {-# INLINE pieceAssoc #-}
 
 -- | Access a specified element through a wrapper.
-itemAt :: (Wrapper h, Extensible f p t, ExtensibleConstr t h xs x) => Membership xs x -> Optic' p f (t h xs) (Repr h x)
+itemAt :: (Wrapper h, Extensible f p t, ExtensibleConstr t xs h x) => Membership xs x -> Optic' p f (t xs h) (Repr h x)
 itemAt m = pieceAt m . _Wrapper
 {-# INLINE itemAt #-}
 
 -- | Access an element through a wrapper.
-item :: (Wrapper h, Extensible f p t, x ∈ xs, ExtensibleConstr t h xs x) => proxy x -> Optic' p f (t h xs) (Repr h x)
+item :: (Wrapper h, Extensible f p t, x ∈ xs, ExtensibleConstr t xs h x) => proxy x -> Optic' p f (t xs h) (Repr h x)
 item p = piece . _WrapperAs p
 {-# INLINE item #-}
 
 -- | Access an element specified by the key type through a wrapper.
-itemAssoc :: (Wrapper h, Extensible f p t, Lookup xs k v, ExtensibleConstr t h xs (k ':> v))
-  => proxy k -> Optic' p f (t h xs) (Repr h (k ':> v))
+itemAssoc :: (Wrapper h, Extensible f p t, Lookup xs k v, ExtensibleConstr t xs h (k ':> v))
+  => proxy k -> Optic' p f (t xs h) (Repr h (k ':> v))
 itemAssoc p = pieceAssoc . _WrapperAs (proxyKey p)
 {-# INLINE itemAssoc #-}
+
+-- | Access an element specified by the key type through a wrapper.
+itemKey :: forall k v xs h f p t. (Wrapper h, Extensible f p t, Lookup xs k v, ExtensibleConstr t xs h (k ':> v))
+  => Optic' p f (t xs h) (Repr h (k ':> v))
+itemKey = pieceAssoc . _WrapperAs (Proxy @ (k ':> v))
+{-# INLINE itemKey #-}
 
 proxyKey :: proxy k -> Proxy (k ':> v)
 proxyKey _ = Proxy
diff --git a/src/Data/Extensible/Dictionary.hs b/src/Data/Extensible/Dictionary.hs
--- a/src/Data/Extensible/Dictionary.hs
+++ b/src/Data/Extensible/Dictionary.hs
@@ -5,6 +5,7 @@
 {-# LANGUAGE UndecidableSuperClasses #-}
 {-# LANGUAGE TypeInType #-}
 {-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE InstanceSigs #-}
 {-# OPTIONS_GHC -fno-warn-orphans #-}
 -----------------------------------------------------------------------
 -- |
@@ -20,6 +21,8 @@
 module Data.Extensible.Dictionary (library, WrapForall, Instance1, And) where
 import Control.DeepSeq
 import qualified Data.Aeson as J
+import Data.Barbie
+import qualified Data.Barbie.Constraints as B
 import qualified Data.Csv as Csv
 import qualified Data.ByteString.Char8 as BC
 import Data.Extensible.Class
@@ -32,6 +35,7 @@
 import Data.Extensible.Struct
 import Data.Extensible.Wrapper
 import Data.Functor.Identity
+import Data.Functor.Product
 import Data.Hashable
 import qualified Data.HashMap.Strict as HM
 import Data.Text.Prettyprint.Doc
@@ -49,16 +53,16 @@
 import Type.Membership
 
 -- | Reify a collection of dictionaries, as you wish.
-library :: forall c xs. Forall c xs => Comp Dict c :* xs
+library :: forall c xs. Forall c xs => xs :& Comp Dict c
 library = hrepeatFor (Proxy :: Proxy c) $ Comp Dict
 {-# INLINE library #-}
 
 class (f x, g x) => And f g x
 instance (f x, g x) => And f g x
 
-instance WrapForall Show h xs => Show (h :* xs) where
+instance WrapForall Show h xs => Show (xs :& h) where
   showsPrec d xs = showParen (d > 0)
-    $ henumerateFor (Proxy :: Proxy (Instance1 Show h)) xs
+    $ henumerateFor (Proxy :: Proxy (Instance1 Show h)) (Proxy :: Proxy xs)
     (\i r -> showsPrec 0 (hlookup i xs) . showString " <: " . r)
     (showString "nil")
 
@@ -70,40 +74,41 @@
   pretty = pretty . getConst
 #endif
 
-instance WrapForall Pretty h xs => Pretty (h :* xs) where
+instance WrapForall Pretty h xs => Pretty (xs :& h) where
   pretty xs = align
     $ encloseSep (flatAlt "" "{ ") (flatAlt "" " }") (flatAlt "" "; ")
-    $ henumerateFor (Proxy :: Proxy (Instance1 Pretty h)) xs
+    $ henumerateFor (Proxy :: Proxy (Instance1 Pretty h)) (Proxy :: Proxy xs)
     (\i r -> pretty (hlookup i xs) : r)
     []
 
-instance WrapForall Eq h xs => Eq (h :* xs) where
-  xs == ys = henumerateFor (Proxy :: Proxy (Instance1 Eq h)) xs
+
+instance WrapForall Eq h xs => Eq (xs :& h) where
+  xs == ys = henumerateFor (Proxy :: Proxy (Instance1 Eq h)) (Proxy :: Proxy xs)
     (\i r -> hlookup i xs == hlookup i ys && r) True
   {-# INLINE (==) #-}
 
-instance (Eq (h :* xs), WrapForall Ord h xs) => Ord (h :* xs) where
-  compare xs ys = henumerateFor (Proxy :: Proxy (Instance1 Ord h)) xs
+instance (Eq (xs :& h), WrapForall Ord h xs) => Ord (xs :& h) where
+  compare xs ys = henumerateFor (Proxy :: Proxy (Instance1 Ord h)) (Proxy :: Proxy xs)
     (\i r -> (hlookup i xs `compare` hlookup i ys) `mappend` r) mempty
   {-# INLINE compare #-}
 
-instance WrapForall Semigroup h xs => Semigroup (h :* xs) where
+instance WrapForall Semigroup h xs => Semigroup (xs :& h) where
   (<>) = hzipWith3 (\(Comp Dict) -> (<>))
-    (library :: Comp Dict (Instance1 Semigroup h) :* xs)
+    (library :: xs :& Comp Dict (Instance1 Semigroup h))
   {-# INLINE (<>) #-}
 
-instance (WrapForall Semigroup h xs, WrapForall Monoid h xs) => Monoid (h :* xs) where
+instance (WrapForall Semigroup h xs, WrapForall Monoid h xs) => Monoid (xs :& h) where
   mempty = hrepeatFor (Proxy :: Proxy (Instance1 Monoid h)) mempty
   {-# INLINE mempty #-}
   mappend = (<>)
   {-# INLINE mappend #-}
 
-instance WrapForall Hashable h xs => Hashable (h :* xs) where
+instance WrapForall Hashable h xs => Hashable (xs :& h) where
   hashWithSalt = hfoldlWithIndexFor (Proxy :: Proxy (Instance1 Hashable h))
     (const hashWithSalt)
   {-# INLINE hashWithSalt #-}
 
-instance WrapForall Bounded h xs => Bounded (h :* xs) where
+instance WrapForall Bounded h xs => Bounded (xs :& h) where
   minBound = hrepeatFor (Proxy :: Proxy (Instance1 Bounded h)) minBound
   maxBound = hrepeatFor (Proxy :: Proxy (Instance1 Bounded h)) maxBound
 
@@ -115,17 +120,17 @@
   lift = appE (conE 'Const) . TH.lift . getConst
 #endif
 
-instance WrapForall TH.Lift h xs => TH.Lift (h :* xs) where
+instance WrapForall TH.Lift h xs => TH.Lift (xs :& h) where
   lift = hfoldrWithIndexFor (Proxy :: Proxy (Instance1 TH.Lift h))
     (\_ x xs -> infixE (Just $ TH.lift x) (varE '(<:)) (Just xs)) (varE 'nil)
 
-newtype instance U.MVector s (h :* xs) = MV_Product (Comp (U.MVector s) h :* xs)
-newtype instance U.Vector (h :* xs) = V_Product (Comp U.Vector h :* xs)
+newtype instance U.MVector s (xs :& h) = MV_Product (xs :& Comp (U.MVector s) h)
+newtype instance U.Vector (xs :& h) = V_Product (xs :& Comp U.Vector h)
 
-hlookupC :: Membership xs a -> Comp f g :* xs -> f (g a)
+hlookupC :: Membership xs a -> xs :& Comp f g -> f (g a)
 hlookupC i = getComp . hlookup i
 
-instance WrapForall U.Unbox h (x ': xs) => G.Vector U.Vector (h :* (x ': xs)) where
+instance WrapForall U.Unbox h (x ': xs) => G.Vector U.Vector ((x ': xs) :& h) where
   basicUnsafeFreeze (MV_Product v) = fmap V_Product
     $ hgenerateFor (Proxy :: Proxy (Instance1 U.Unbox h))
     $ \m -> Comp <$> G.basicUnsafeFreeze (hlookupC m v)
@@ -141,7 +146,7 @@
   basicUnsafeCopy (MV_Product v) (V_Product w)
     = henumerateFor (Proxy :: Proxy (Instance1 U.Unbox h)) (Proxy :: Proxy (x ': xs)) ((>>) . \i -> G.basicUnsafeCopy (hlookupC i v) (hlookupC i w)) (return ())
 
-instance WrapForall U.Unbox h (x ': xs) => M.MVector U.MVector (h :* (x ': xs)) where
+instance WrapForall U.Unbox h (x ': xs) => M.MVector U.MVector ((x ': xs) :& h) where
   basicLength (MV_Product v) = M.basicLength $ getComp $ hindex v leadership
   basicUnsafeSlice i n (MV_Product v) = MV_Product
     $ htabulateFor (Proxy :: Proxy (Instance1 U.Unbox h))
@@ -172,97 +177,97 @@
     $ hgenerateFor (Proxy :: Proxy (Instance1 U.Unbox h))
     $ \i -> Comp <$> M.basicUnsafeGrow (hlookupC i v) n
 
-instance WrapForall U.Unbox h (x ': xs) => U.Unbox (h :* (x ': xs))
+instance WrapForall U.Unbox h (x ': xs) => U.Unbox ((x ': xs) :& h)
 
-instance WrapForall Arbitrary h xs => Arbitrary (h :* xs) where
+instance WrapForall Arbitrary h xs => Arbitrary (xs :& h) where
   arbitrary = hgenerateFor (Proxy :: Proxy (Instance1 Arbitrary h)) (const arbitrary)
   shrink xs = henumerateFor (Proxy :: Proxy (Instance1 Arbitrary h))
     (Proxy :: Proxy xs) (\i -> (++)
     $ map (\x -> hmodify (\s -> set s i x) xs) $ shrink $ hindex xs i)
     []
 
-instance WrapForall NFData h xs => NFData (h :* xs) where
+instance WrapForall NFData h xs => NFData (xs :& h) where
   rnf xs = henumerateFor (Proxy :: Proxy (Instance1 NFData h)) (Proxy :: Proxy xs)
     (\i -> deepseq (hlookup i xs)) ()
   {-# INLINE rnf #-}
 
-instance WrapForall Csv.FromField h xs => Csv.FromRecord (h :* xs) where
+instance WrapForall Csv.FromField h xs => Csv.FromRecord (xs :& h) where
   parseRecord rec = hgenerateFor (Proxy :: Proxy (Instance1 Csv.FromField h))
     $ \i -> G.indexM rec (getMemberId i) >>= Csv.parseField
 
-instance Forall (KeyTargetAre KnownSymbol (Instance1 Csv.FromField h)) xs => Csv.FromNamedRecord (Field h :* xs) where
+instance Forall (KeyTargetAre KnownSymbol (Instance1 Csv.FromField h)) xs => Csv.FromNamedRecord (xs :& Field h) where
   parseNamedRecord rec = hgenerateFor (Proxy :: Proxy (KeyTargetAre KnownSymbol (Instance1 Csv.FromField h)))
-    $ \i -> rec Csv..: BC.pack (symbolVal (proxyAssocKey i)) >>= Csv.parseField
+    $ \i -> rec Csv..: BC.pack (symbolVal (proxyKeyOf i)) >>= Csv.parseField
 
-instance WrapForall Csv.ToField h xs => Csv.ToRecord (h :* xs) where
+instance WrapForall Csv.ToField h xs => Csv.ToRecord (xs :& h) where
   toRecord = V.fromList
     . hfoldrWithIndexFor (Proxy :: Proxy (Instance1 Csv.ToField h))
       (\_ v -> (:) $ Csv.toField v) []
 
-instance Forall (KeyTargetAre KnownSymbol (Instance1 Csv.ToField h)) xs => Csv.ToNamedRecord (Field h :* xs) where
+instance Forall (KeyTargetAre KnownSymbol (Instance1 Csv.ToField h)) xs => Csv.ToNamedRecord (xs :& Field h) where
   toNamedRecord = hfoldlWithIndexFor (Proxy :: Proxy (KeyTargetAre KnownSymbol (Instance1 Csv.ToField h)))
-    (\k m v -> HM.insert (BC.pack (symbolVal (proxyAssocKey k))) (Csv.toField v) m)
+    (\k m v -> HM.insert (BC.pack (symbolVal (proxyKeyOf k))) (Csv.toField v) m)
     HM.empty
 
 -- | @'parseJSON' 'J.Null'@ is called for missing fields.
-instance Forall (KeyTargetAre KnownSymbol (Instance1 J.FromJSON h)) xs => J.FromJSON (Field h :* xs) where
+instance Forall (KeyTargetAre KnownSymbol (Instance1 J.FromJSON h)) xs => J.FromJSON (xs :& Field h) where
   parseJSON = J.withObject "Object" $ \v -> hgenerateFor
     (Proxy :: Proxy (KeyTargetAre KnownSymbol (Instance1 J.FromJSON h)))
-    $ \m -> let k = symbolVal (proxyAssocKey m)
+    $ \m -> let k = symbolVal (proxyKeyOf m)
       in fmap Field $ J.parseJSON $ maybe J.Null id $ HM.lookup (T.pack k) v
 
-instance Forall (KeyTargetAre KnownSymbol (Instance1 J.ToJSON h)) xs => J.ToJSON (Field h :* xs) where
+instance Forall (KeyTargetAre KnownSymbol (Instance1 J.ToJSON h)) xs => J.ToJSON (xs :& Field h) where
   toJSON = J.Object . hfoldlWithIndexFor
     (Proxy :: Proxy (KeyTargetAre KnownSymbol (Instance1 J.ToJSON h)))
-    (\k m v -> HM.insert (T.pack (symbolVal (proxyAssocKey k))) (J.toJSON v) m)
+    (\k m v -> HM.insert (T.pack (symbolVal (proxyKeyOf k))) (J.toJSON v) m)
     HM.empty
 
-instance Forall (KeyTargetAre KnownSymbol (Instance1 J.FromJSON h)) xs => J.FromJSON (Nullable (Field h) :* xs) where
+instance Forall (KeyTargetAre KnownSymbol (Instance1 J.FromJSON h)) xs => J.FromJSON (xs :& Nullable (Field h)) where
   parseJSON = J.withObject "Object" $ \v -> hgenerateFor
     (Proxy :: Proxy (KeyTargetAre KnownSymbol (Instance1 J.FromJSON h)))
-    $ \m -> let k = symbolVal (proxyAssocKey m)
+    $ \m -> let k = symbolVal (proxyKeyOf m)
       in fmap Nullable $ traverse J.parseJSON $ HM.lookup (T.pack k) v
 
-instance Forall (KeyTargetAre KnownSymbol (Instance1 J.ToJSON h)) xs => J.ToJSON (Nullable (Field h) :* xs) where
+instance Forall (KeyTargetAre KnownSymbol (Instance1 J.ToJSON h)) xs => J.ToJSON (xs :& Nullable (Field h)) where
   toJSON = J.Object . hfoldlWithIndexFor
     (Proxy :: Proxy (KeyTargetAre KnownSymbol (Instance1 J.ToJSON h)))
-    (\k m (Nullable v) -> maybe id (HM.insert (T.pack $ symbolVal $ proxyAssocKey k) . J.toJSON) v m)
+    (\k m (Nullable v) -> maybe id (HM.insert (T.pack $ symbolVal $ proxyKeyOf k) . J.toJSON) v m)
     HM.empty
 
-instance WrapForall Show h xs => Show (h :| xs) where
+instance WrapForall Show h xs => Show (xs :/ h) where
   showsPrec d (EmbedAt i h) = showParen (d > 10) $ showString "EmbedAt "
     . showsPrec 11 i
     . showString " "
-    . views (pieceAt i) (\(Comp Dict) -> showsPrec 11 h) (library :: Comp Dict (Instance1 Show h) :* xs)
+    . views (pieceAt i) (\(Comp Dict) -> showsPrec 11 h) (library :: xs :& Comp Dict (Instance1 Show h))
 
-instance WrapForall Eq h xs => Eq (h :| xs) where
+instance WrapForall Eq h xs => Eq (xs :/ h) where
   EmbedAt p g == EmbedAt q h = case compareMembership p q of
     Left _ -> False
-    Right Refl -> views (pieceAt p) (\(Comp Dict) -> g == h) (library :: Comp Dict (Instance1 Eq h) :* xs)
+    Right Refl -> views (pieceAt p) (\(Comp Dict) -> g == h) (library :: xs :& Comp Dict (Instance1 Eq h))
   {-# INLINE (==) #-}
 
-instance (Eq (h :| xs), WrapForall Ord h xs) => Ord (h :| xs) where
+instance (Eq (xs :/ h), WrapForall Ord h xs) => Ord (xs :/ h) where
   EmbedAt p g `compare` EmbedAt q h = case compareMembership p q of
     Left x -> x
-    Right Refl -> views (pieceAt p) (\(Comp Dict) -> compare g h) (library :: Comp Dict (Instance1 Ord h) :* xs)
+    Right Refl -> views (pieceAt p) (\(Comp Dict) -> compare g h) (library :: xs :& Comp Dict (Instance1 Ord h))
   {-# INLINE compare #-}
 
-instance WrapForall NFData h xs => NFData (h :| xs) where
-  rnf (EmbedAt i h) = views (pieceAt i) (\(Comp Dict) -> rnf h) (library :: Comp Dict (Instance1 NFData h) :* xs)
+instance WrapForall NFData h xs => NFData (xs :/ h) where
+  rnf (EmbedAt i h) = views (pieceAt i) (\(Comp Dict) -> rnf h) (library :: xs :& Comp Dict (Instance1 NFData h))
   {-# INLINE rnf #-}
 
-instance WrapForall Hashable h xs => Hashable (h :| xs) where
+instance WrapForall Hashable h xs => Hashable (xs :/ h) where
   hashWithSalt s (EmbedAt i h) = views (pieceAt i)
     (\(Comp Dict) -> s `hashWithSalt` i `hashWithSalt` h)
-    (library :: Comp Dict (Instance1 Hashable h) :* xs)
+    (library :: xs :& Comp Dict (Instance1 Hashable h))
   {-# INLINE hashWithSalt #-}
 
-instance WrapForall TH.Lift h xs => TH.Lift (h :| xs) where
+instance WrapForall TH.Lift h xs => TH.Lift (xs :/ h) where
   lift (EmbedAt i h) = views (pieceAt i)
     (\(Comp Dict) -> conE 'EmbedAt `appE` TH.lift i `appE` TH.lift h)
-    (library :: Comp Dict (Instance1 TH.Lift h) :* xs)
+    (library :: xs :& Comp Dict (Instance1 TH.Lift h))
 
-instance WrapForall Arbitrary h xs => Arbitrary (h :| xs) where
+instance WrapForall Arbitrary h xs => Arbitrary (xs :/ h) where
   arbitrary = choose (0, hcount (Proxy :: Proxy xs)) >>= henumerateFor
       (Proxy :: Proxy (Instance1 Arbitrary h))
       (Proxy :: Proxy xs)
@@ -272,14 +277,14 @@
         (error "Impossible")
   shrink (EmbedAt i h) = views (pieceAt i)
     (\(Comp Dict) -> EmbedAt i <$> shrink h)
-    (library :: Comp Dict (Instance1 Arbitrary h) :* xs)
+    (library :: xs :& Comp Dict (Instance1 Arbitrary h))
 
-instance WrapForall Pretty h xs => Pretty (h :| xs) where
+instance WrapForall Pretty h xs => Pretty (xs :/ h) where
   pretty (EmbedAt i h) = "EmbedAt "
     <> pretty i
     <> " "
     <> views (pieceAt i) (\(Comp Dict) -> pretty h)
-    (library :: Comp Dict (Instance1 Pretty h) :* xs)
+    (library :: xs :& Comp Dict (Instance1 Pretty h))
 
 -- | Forall upon a wrapper
 type WrapForall c h = Forall (Instance1 c h)
@@ -337,3 +342,31 @@
 instance (U.Unbox a) => U.Unbox (Identity a)
 
 #endif
+
+instance FunctorB ((:&) xs) where
+  bmap = hmap
+
+instance FunctorB ((:/) xs) where
+  bmap = hoist
+
+instance TraversableB ((:&) xs) where
+  btraverse = htraverse
+
+instance TraversableB ((:/) xs) where
+  btraverse f (EmbedAt i x) = EmbedAt i <$> f x
+
+instance Generate xs => ProductB ((:&) xs) where
+  bprod = hzipWith Pair
+  buniq = hrepeat
+
+instance ConstraintsB ((:&) xs) where
+  type AllB c ((:&) xs) = Forall c xs
+  baddDicts = bprod bdicts
+
+instance ConstraintsB ((:/) xs) where
+  type AllB c ((:/) xs) = Forall c xs
+  baddDicts (EmbedAt i x) = EmbedAt i (Pair (hlookup i bdicts) x)
+
+instance Generate xs => ProductBC ((:&) xs) where
+  bdicts :: forall c ys. Forall c ys => ys :& B.Dict c
+  bdicts = hrepeatFor (Proxy :: Proxy c) $ B.Dict
diff --git a/src/Data/Extensible/Effect.hs b/src/Data/Extensible/Effect.hs
--- a/src/Data/Extensible/Effect.hs
+++ b/src/Data/Extensible/Effect.hs
@@ -73,6 +73,7 @@
   , throwEff
   , catchEff
   , runEitherEff
+  , mapLeftEff
   -- ** Iter
   , Identity
   , tickEff
@@ -81,9 +82,11 @@
   , ContT
   , contEff
   , runContEff
+  , callCCEff
   ) where
 
 import Control.Applicative
+import Data.Bifunctor (first)
 import Control.Monad.Skeleton
 import Control.Monad.Trans.State.Strict
 import Control.Monad.Trans.Cont (ContT(..))
@@ -436,6 +439,15 @@
 tickEff k = liftEff k $ Identity ()
 {-# INLINE tickEff #-}
 
+mapHeadEff :: (forall x. s x -> t x) -> Eff ((k >: s) ': xs) a -> Eff ((k' >: t) ': xs) a
+mapHeadEff f = hoistSkeleton $ \(Instruction i t) -> testMembership i 
+  (\Refl -> Instruction leadership $ f t) 
+  (\j -> Instruction (nextMembership j) t)
+
+-- | Take a function and applies it to an Either effect iff the effect takes the form Left _.
+mapLeftEff :: (e -> e') -> Eff ((k >: EitherEff e) ': xs) a -> Eff ((k >: EitherEff e') ': xs) a
+mapLeftEff f = mapHeadEff (first f)
+
 -- | Run a computation until the first call of 'tickEff'.
 runIterEff :: Eff (k >: Identity ': xs) a
   -> Eff xs (Either a (Eff (k >: Identity ': xs) a))
@@ -459,3 +471,10 @@
   Instruction i t :>>= k -> testMembership i
     (\Refl -> runContT t (flip runContEff cont . k))
     $ \j -> boned $ Instruction j t :>>= flip runContEff cont . k
+
+-- | Call a function with the current continuation as its argument
+callCCEff :: Proxy k -> ((a -> Eff ((k >: ContT r (Eff xs)) : xs) b) -> Eff ((k >: ContT r (Eff xs)) : xs) a) -> Eff ((k >: ContT r (Eff xs)) : xs) a
+callCCEff k f = contHead k . ContT $ \c -> runContEff (f (\x -> contHead k . ContT $ \_ -> c x)) c
+  where
+    contHead :: Proxy k -> ContT r (Eff xs) a -> Eff ((k >: ContT r (Eff xs)) ': xs) a
+    contHead _ c = boned $ Instruction leadership c :>>= return
diff --git a/src/Data/Extensible/Effect/Default.hs b/src/Data/Extensible/Effect/Default.hs
--- a/src/Data/Extensible/Effect/Default.hs
+++ b/src/Data/Extensible/Effect/Default.hs
@@ -27,11 +27,14 @@
   , runMaybeDef
   , EitherDef
   , runEitherDef
+  , ContDef
+  , runContDef
 ) where
 import Control.Applicative
 import Data.Extensible.Effect
 import Control.Monad.Except
 import Control.Monad.Catch
+import Control.Monad.Cont
 import Control.Monad.Reader.Class
 import Control.Monad.Skeleton
 import Control.Monad.State.Strict
@@ -102,6 +105,12 @@
   mzero = empty
   mplus = (<|>)
 
+pCont :: Proxy "Cont"
+pCont = Proxy
+
+instance MonadCont (Eff ((ContDef r (Eff xs)) ': xs)) where
+  callCC = callCCEff pCont
+
 -- | mtl-compatible reader
 type ReaderDef r = "Reader" >: ReaderEff r
 
@@ -156,3 +165,11 @@
 runEitherDef :: Eff (EitherDef e ': xs) a -> Eff xs (Either e a)
 runEitherDef = runEitherEff
 {-# INLINE runEitherDef #-}
+
+-- | mtl-compatible continuation
+type ContDef r m = "Cont" >: ContT r m
+
+-- | 'runContEff' specialised for the 'MonadCont' instance.
+runContDef :: Eff (ContDef r (Eff xs) ': xs) a -> (a -> Eff xs r) -> Eff xs r
+runContDef = runContEff
+{-# INLINE runContDef #-}
diff --git a/src/Data/Extensible/Field.hs b/src/Data/Extensible/Field.hs
--- a/src/Data/Extensible/Field.hs
+++ b/src/Data/Extensible/Field.hs
@@ -200,19 +200,19 @@
 --
 -- @RecordOf :: (v -> *) -> [Assoc k v] -> *@
 --
-type RecordOf h = (:*) (Field h)
+type RecordOf h xs = xs :& Field h
 
 -- | The dual of 'RecordOf'
 --
 -- @VariantOf :: (v -> *) -> [Assoc k v] -> *@
 --
-type VariantOf h = (:|) (Field h)
+type VariantOf h xs = xs :/ Field h
 
 -- | Simple record
-type Record = RecordOf Identity
+type Record xs = RecordOf Identity xs
 
 -- | Simple variant
-type Variant = VariantOf Identity
+type Variant xs = VariantOf Identity xs
 
 -- | An empty 'Record'.
 emptyRecord :: Record '[]
@@ -246,21 +246,21 @@
 --
 type FieldOptic k = forall kind. forall f p t xs (h :: kind -> Type) (v :: kind).
   (Extensible f p t
-  , ExtensibleConstr t (Field h) xs (k ':> v)
+  , ExtensibleConstr t xs (Field h) (k ':> v)
   , Lookup xs k v
   , Labelling k p
   , Wrapper h)
-  => Optic' p f (t (Field h) xs) (Repr h v)
+  => Optic' p f (t xs (Field h)) (Repr h v)
 
 -- | The trivial inextensible data type
-data Inextensible (h :: k -> Type) (xs :: [k])
+data Inextensible (xs :: [k]) (h :: k -> Type)
 
 instance (Functor f, Profunctor p) => Extensible f p Inextensible where
   pieceAt _ _ = error "Impossible"
 
 -- | When you see this type as an argument, it expects a 'FieldLens'.
 -- This type is used to resolve the name of the field internally.
-type FieldName k = Optic' (LabelPhantom k) Proxy (Inextensible (Field Proxy) '[k ':> ()]) ()
+type FieldName k = Optic' (LabelPhantom k) Proxy (Inextensible '[k ':> ()] (Field Proxy)) ()
 
 -- | Signifies a field name internally
 type family Labelling s p :: Constraint where
diff --git a/src/Data/Extensible/Inclusion.hs b/src/Data/Extensible/Inclusion.hs
--- a/src/Data/Extensible/Inclusion.hs
+++ b/src/Data/Extensible/Inclusion.hs
@@ -42,17 +42,17 @@
 type Include ys = Forall (Member ys)
 
 -- | Reify the inclusion of type level sets.
-inclusion :: forall xs ys. Include ys xs => Membership ys :* xs
+inclusion :: forall xs ys. Include ys xs => xs :& Membership ys
 inclusion = hrepeatFor (Proxy :: Proxy (Member ys)) membership
 {-# INLINABLE inclusion #-}
 
 -- | /O(n)/ Select some elements.
-shrink :: (xs ⊆ ys) => h :* ys -> h :* xs
+shrink :: (xs ⊆ ys) => ys :& h -> xs :& h
 shrink h = hmap (hindex h) inclusion
 {-# INLINE shrink #-}
 
 -- | /O(1)/ Embed to a larger union.
-spread :: (xs ⊆ ys) => h :| xs -> h :| ys
+spread :: (xs ⊆ ys) => xs :/ h -> ys :/ h
 spread (EmbedAt i h) = views (pieceAt i) EmbedAt inclusion h
 {-# INLINE spread #-}
 
@@ -72,16 +72,16 @@
 type IncludeAssoc ys = Forall (Associated ys)
 
 -- | Reify the inclusion of type level sets.
-inclusionAssoc :: forall xs ys. IncludeAssoc ys xs => Membership ys :* xs
+inclusionAssoc :: forall xs ys. IncludeAssoc ys xs => xs :& Membership ys
 inclusionAssoc = hrepeatFor (Proxy :: Proxy (Associated ys)) getAssociation
 {-# INLINABLE inclusionAssoc #-}
 
 -- | /O(n)/ Select some elements.
-shrinkAssoc :: (IncludeAssoc ys xs) => h :* ys -> h :* xs
+shrinkAssoc :: (IncludeAssoc ys xs) => ys :& h -> xs :& h
 shrinkAssoc h = hmap (hindex h) inclusionAssoc
 {-# INLINE shrinkAssoc #-}
 
 -- | /O(1)/ Embed to a larger union.
-spreadAssoc :: (IncludeAssoc ys xs) => h :| xs -> h :| ys
+spreadAssoc :: (IncludeAssoc ys xs) => xs :/ h -> ys :/ h
 spreadAssoc (EmbedAt i h) = views (pieceAt i) EmbedAt inclusionAssoc h
 {-# INLINE spreadAssoc #-}
diff --git a/src/Data/Extensible/Label.hs b/src/Data/Extensible/Label.hs
--- a/src/Data/Extensible/Label.hs
+++ b/src/Data/Extensible/Label.hs
@@ -33,9 +33,9 @@
   , Lookup xs k v
   , Labelling k p
   , Wrapper h
-  , ExtensibleConstr e (Field h) xs (k ':> v)
+  , ExtensibleConstr e xs (Field h) (k ':> v)
   , rep ~ Repr h v
-  , s ~ e (Field h) xs
+  , s ~ e xs (Field h)
   , s ~ t
   , rep ~ rep'
   )
diff --git a/src/Data/Extensible/Match.hs b/src/Data/Extensible/Match.hs
--- a/src/Data/Extensible/Match.hs
+++ b/src/Data/Extensible/Match.hs
@@ -26,7 +26,7 @@
 import GHC.Generics (Generic)
 
 -- | Retrieve the contents so that they matches and pass both to the given function.
-matchWith :: (forall x. f x -> g x -> r) -> f :* xs -> g :| xs -> r
+matchWith :: (forall x. f x -> g x -> r) -> xs :& f -> xs :/ g -> r
 matchWith f p = \(EmbedAt i h) -> views (pieceAt i) f p h
 {-# INLINE matchWith #-}
 
@@ -36,12 +36,12 @@
 {-# INLINE mapMatch #-}
 
 -- | /O(1)/ Perform pattern matching.
-match :: Match h a :* xs -> h :| xs -> a
+match :: xs :& Match h a -> xs :/ h -> a
 match = matchWith runMatch
 {-# INLINE match #-}
 
 -- | Flipped `match`
-caseOf :: h :| xs -> Match h a :* xs -> a
+caseOf :: xs :/ h -> xs :& Match h a -> a
 caseOf = flip match
 {-# INLINE caseOf #-}
 infix 0 `caseOf`
diff --git a/src/Data/Extensible/Nullable.hs b/src/Data/Extensible/Nullable.hs
--- a/src/Data/Extensible/Nullable.hs
+++ b/src/Data/Extensible/Nullable.hs
@@ -58,22 +58,22 @@
 {-# INLINE mapNullable #-}
 
 -- | The inverse of 'inclusion'.
-coinclusion :: (Include ys xs, Generate ys) => Nullable (Membership xs) :* ys
+coinclusion :: (Include ys xs, Generate ys) => ys :& Nullable (Membership xs)
 coinclusion = S.hfrozen $ do
   s <- S.newRepeat $ Nullable Nothing
   hfoldrWithIndex
     (\i m cont -> S.set s m (Nullable $ Just i) >> cont) (return s) inclusion
 
 -- | A product filled with @'Nullable' 'Nothing'@
-vacancy :: Generate xs => Nullable h :* xs
+vacancy :: Generate xs => xs :& Nullable h
 vacancy = hrepeat $ Nullable Nothing
 
 -- | Extend a product and fill missing fields by 'Null'.
-wrench :: (Generate ys, xs ⊆ ys) => h :* xs -> Nullable h :* ys
+wrench :: (Generate ys, xs ⊆ ys) => xs :& h -> ys :& Nullable h
 wrench xs = mapNullable (flip hlookup xs) `hmap` coinclusion
 {-# INLINE wrench #-}
 
 -- | Narrow the range of the sum, if possible.
-retrench :: (Generate ys, xs ⊆ ys) => h :| ys -> Nullable ((:|) h) xs
+retrench :: (Generate ys, xs ⊆ ys) => ys :/ h -> Nullable ((:/) xs) h
 retrench (EmbedAt i h) = views (pieceAt i) (mapNullable (`EmbedAt`h)) coinclusion
 {-# INLINE retrench #-}
diff --git a/src/Data/Extensible/Plain.hs b/src/Data/Extensible/Plain.hs
--- a/src/Data/Extensible/Plain.hs
+++ b/src/Data/Extensible/Plain.hs
@@ -28,10 +28,10 @@
 import Data.Profunctor.Unsafe
 
 -- | Alias for plain products
-type AllOf xs = Identity :* xs
+type AllOf xs = xs :& Identity
 
 -- | Alias for plain sums
-type OneOf xs = Identity :| xs
+type OneOf xs = xs :/ Identity
 
 -- | /O(log n)/ Add a plain value to a product.
 (<%) :: x -> AllOf xs -> AllOf (x ': xs)
@@ -55,6 +55,6 @@
 infixr 1 <%|
 
 -- | An accessor for newtype constructors.
-accessing :: (Coercible x a, x ∈ xs, Extensible f p t, ExtensibleConstr t Identity xs x) => (a -> x) -> Optic' p f (t Identity xs) a
+accessing :: (Coercible x a, x ∈ xs, Extensible f p t, ExtensibleConstr t xs Identity x) => (a -> x) -> Optic' p f (t xs Identity) a
 accessing c = piece . _Wrapper . dimap coerce (fmap c)
 {-# INLINE accessing #-}
diff --git a/src/Data/Extensible/Product.hs b/src/Data/Extensible/Product.hs
--- a/src/Data/Extensible/Product.hs
+++ b/src/Data/Extensible/Product.hs
@@ -1,6 +1,8 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
 {-# LANGUAGE Trustworthy #-}
 {-# LANGUAGE ViewPatterns, ScopedTypeVariables #-}
 {-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE MultiParamTypeClasses, UndecidableInstances #-}
 -----------------------------------------------------------------------------
 -- |
@@ -13,7 +15,8 @@
 ------------------------------------------------------------------------
 module Data.Extensible.Product (
   -- * Basic operations
-  (:*)
+  (:&)
+  , (:*)
   , nil
   , (<:)
   , (<!)
@@ -23,7 +26,6 @@
   , happend
   , hmap
   , hmapWithIndex
-  , hmapWithIndexFor
   , hzipWith
   , hzipWith3
   , hfoldMap
@@ -34,10 +36,17 @@
   , htraverseWithIndex
   , hsequence
   -- * Constrained fold
+  , hmapWithIndexFor
   , hfoldMapFor
   , hfoldMapWithIndexFor
   , hfoldrWithIndexFor
   , hfoldlWithIndexFor
+  -- * Constraind fold without proxies
+  , hfoldMapWith
+  , hfoldMapWithIndexWith
+  , hfoldrWithIndexWith
+  , hfoldlWithIndexWith
+  , hmapWithIndexWith
   -- * Evaluating
   , hforce
   -- * Update
@@ -59,51 +68,55 @@
   , Forall(..)
   , hgenerateFor
   , htabulateFor
-  , hrepeatFor) where
+  , hrepeatFor
+  , hgenerateWith
+  , htabulateWith
+  , hrepeatWith) where
 
 import Data.Extensible.Internal.Rig (review)
 import Data.Extensible.Struct
 import Data.Extensible.Sum
 import Data.Extensible.Class
 import Data.Extensible.Wrapper
+import Data.Proxy
 import qualified Type.Membership.HList as HList
 
 -- | O(n) Prepend an element onto a product.
 -- Expressions like @a <: b <: c <: nil@ are transformed to a single 'fromHList'.
-(<:) :: h x -> h :* xs -> h :* (x ': xs)
+(<:) :: h x -> xs :& h -> (x ': xs) :& h
 (<:) x = fromHList . HList.HCons x . toHList
 {-# INLINE (<:) #-}
 infixr 0 <:
 
-(=<:) :: Wrapper h => Repr h x -> h :* xs -> h :* (x ': xs)
+(=<:) :: Wrapper h => Repr h x -> xs :& h -> (x ': xs) :& h
 (=<:) = (<:) . review _Wrapper
 {-# INLINE (=<:) #-}
 infixr 0 =<:
 
 -- | Strict version of ('<:').
-(<!) :: h x -> h :* xs -> h :* (x ': xs)
+(<!) :: h x -> xs :& h -> (x ': xs) :& h
 (<!) x = fromHList . (HList.HCons $! x) . toHList
 {-# INLINE (<!) #-}
 infixr 0 <!
 
 -- | An empty product.
-nil :: h :* '[]
+nil :: '[] :& h
 nil = hfrozen $ new $ error "Impossible"
 {-# NOINLINE nil #-}
 {-# RULES "toHList/nil" toHList nil = HList.HNil #-}
 
 -- | Convert 'HList.HList' into a product.
-fromHList :: HList.HList h xs -> h :* xs
+fromHList :: HList.HList h xs -> xs :& h
 fromHList xs = hfrozen (newFromHList xs)
 {-# INLINE fromHList #-}
 
 -- | Flipped 'hlookup'
-hindex :: h :* xs -> Membership xs x ->  h x
+hindex :: xs :& h -> Membership xs x ->  h x
 hindex = flip hlookup
 {-# INLINE hindex #-}
 
 -- | Map a function to every element of a product.
-hmapWithIndex :: (forall x. Membership xs x -> g x -> h x) -> g :* xs -> h :* xs
+hmapWithIndex :: (forall x. Membership xs x -> g x -> h x) -> xs :& g -> xs :& h
 hmapWithIndex t p = hfrozen (newFrom p t)
 {-# INLINE hmapWithIndex #-}
 
@@ -111,105 +124,133 @@
 hmapWithIndexFor :: Forall c xs
   => proxy c
   -> (forall x. c x => Membership xs x -> g x -> h x)
-  -> g :* xs -> h :* xs
+  -> xs :& g -> xs :& h
 hmapWithIndexFor c t p = hfrozen $ newFor c $ \i -> t i $ hlookup i p
 {-# INLINE hmapWithIndexFor #-}
 
+hmapWithIndexWith :: forall c xs g h. Forall c xs
+  => (forall x. c x => Membership xs x -> g x -> h x)
+  -> xs :& g -> xs :& h
+hmapWithIndexWith = hmapWithIndexFor (Proxy @ c)
+
 -- | Transform every element in a product, preserving the order.
 --
 -- @
 -- 'hmap' 'id' ≡ 'id'
 -- 'hmap' (f . g) ≡ 'hmap' f . 'hmap' g
 -- @
-hmap :: (forall x. g x -> h x) -> g :* xs -> h :* xs
+hmap :: (forall x. g x -> h x) -> xs :& g -> xs :& h
 hmap f = hmapWithIndex (const f)
 {-# INLINE hmap #-}
 
 -- | 'zipWith' for heterogeneous product
-hzipWith :: (forall x. f x -> g x -> h x) -> f :* xs -> g :* xs -> h :* xs
+hzipWith :: (forall x. f x -> g x -> h x) -> xs :& f -> xs :& g -> xs :& h
 hzipWith t xs = hmapWithIndex (\i -> t (hlookup i xs))
 {-# INLINE hzipWith #-}
 
 -- | 'zipWith3' for heterogeneous product
-hzipWith3 :: (forall x. f x -> g x -> h x -> i x) -> f :* xs -> g :* xs -> h :* xs -> i :* xs
+hzipWith3 :: (forall x. f x -> g x -> h x -> i x) -> xs :& f -> xs :& g -> xs :& h -> xs :& i
 hzipWith3 t xs ys = hmapWithIndex (\i -> t (hlookup i xs) (hlookup i ys))
 {-# INLINE hzipWith3 #-}
 
 -- | Map elements to a monoid and combine the results.
 --
 -- @'hfoldMap' f . 'hmap' g ≡ 'hfoldMap' (f . g)@
-hfoldMap :: Monoid a => (forall x. h x -> a) -> h :* xs -> a
+hfoldMap :: Monoid a => (forall x. h x -> a) -> xs :& h -> a
 hfoldMap f = hfoldMapWithIndex (const f)
 {-# INLINE hfoldMap #-}
 
 -- | 'hfoldMap' with the membership of elements.
 hfoldMapWithIndex :: Monoid a
-  => (forall x. Membership xs x -> g x -> a) -> g :* xs -> a
+  => (forall x. Membership xs x -> g x -> a) -> xs :& g -> a
 hfoldMapWithIndex f = hfoldrWithIndex (\i -> mappend . f i) mempty
 {-# INLINE hfoldMapWithIndex #-}
 
 -- | Perform a strict left fold over the elements.
-hfoldlWithIndex :: (forall x. Membership xs x -> r -> h x -> r) -> r -> h :* xs -> r
+hfoldlWithIndex :: (forall x. Membership xs x -> r -> h x -> r) -> r -> xs :& h -> r
 hfoldlWithIndex f r xs = hfoldrWithIndex (\i x c a -> c $! f i a x) id xs r
 {-# INLINE hfoldlWithIndex #-}
 
 -- | 'hfoldrWithIndex' with a constraint for each element.
-hfoldrWithIndexFor :: (Forall c xs) => proxy c
-  -> (forall x. c x => Membership xs x -> h x -> r -> r) -> r -> h :* xs -> r
-hfoldrWithIndexFor p f r xs = henumerateFor p xs (\i -> f i (hlookup i xs)) r
+hfoldrWithIndexFor :: forall c xs h r proxy. (Forall c xs) => proxy c
+  -> (forall x. c x => Membership xs x -> h x -> r -> r) -> r -> xs :& h -> r
+hfoldrWithIndexFor p f r xs = henumerateFor p (Proxy :: Proxy xs) (\i -> f i (hlookup i xs)) r
 {-# INLINE hfoldrWithIndexFor #-}
 
+hfoldrWithIndexWith :: forall c xs h r. (Forall c xs)
+  => (forall x. c x => Membership xs x -> h x -> r -> r) -> r -> xs :& h -> r
+hfoldrWithIndexWith f r xs = henumerateFor (Proxy @ c) (Proxy @ xs) (\i -> f i (hlookup i xs)) r
+{-# INLINE hfoldrWithIndexWith #-}
+
 -- | Constrained 'hfoldlWithIndex'
 hfoldlWithIndexFor :: (Forall c xs) => proxy c
-  -> (forall x. c x => Membership xs x -> r -> h x -> r) -> r -> h :* xs -> r
+  -> (forall x. c x => Membership xs x -> r -> h x -> r) -> r -> xs :& h -> r
 hfoldlWithIndexFor p f r xs = hfoldrWithIndexFor p (\i x c a -> c $! f i a x) id xs r
 {-# INLINE hfoldlWithIndexFor #-}
 
+-- | Constrained 'hfoldlWithIndex'
+hfoldlWithIndexWith :: forall c xs h r. (Forall c xs)
+  => (forall x. c x => Membership xs x -> r -> h x -> r) -> r -> xs :& h -> r
+hfoldlWithIndexWith f r xs = hfoldrWithIndexWith @c (\i x c a -> c $! f i a x) id xs r
+{-# INLINE hfoldlWithIndexWith #-}
+
 -- | 'hfoldMapWithIndex' with a constraint for each element.
 hfoldMapWithIndexFor :: (Forall c xs, Monoid a) => proxy c
-  -> (forall x. c x => Membership xs x -> h x -> a) -> h :* xs -> a
+  -> (forall x. c x => Membership xs x -> h x -> a) -> xs :& h -> a
 hfoldMapWithIndexFor p f = hfoldrWithIndexFor p (\i -> mappend . f i) mempty
 {-# INLINE hfoldMapWithIndexFor #-}
 
+-- | 'hfoldMapWithIndex' with a constraint for each element.
+hfoldMapWithIndexWith :: forall c xs h a. (Forall c xs, Monoid a)
+  => (forall x. c x => Membership xs x -> h x -> a) -> xs :& h -> a
+hfoldMapWithIndexWith f = hfoldrWithIndexWith @c (\i -> mappend . f i) mempty
+{-# INLINE hfoldMapWithIndexWith #-}
+
 -- | Constrained 'hfoldMap'
 hfoldMapFor :: (Forall c xs, Monoid a) => proxy c
-  -> (forall x. c x => h x -> a) -> h :* xs -> a
+  -> (forall x. c x => h x -> a) -> xs :& h -> a
 hfoldMapFor p f = hfoldMapWithIndexFor p (const f)
 {-# INLINE hfoldMapFor #-}
 
+-- | Constrained 'hfoldMap'
+hfoldMapWith :: forall c xs h a. (Forall c xs, Monoid a)
+  => (forall x. c x => h x -> a) -> xs :& h -> a
+hfoldMapWith f = hfoldMapWithIndexFor (Proxy @ c) (const f)
+{-# INLINE hfoldMapWith #-}
+
 -- | Traverse all elements and combine the result sequentially.
 -- @
 -- htraverse (fmap f . g) ≡ fmap (hmap f) . htraverse g
 -- htraverse pure ≡ pure
 -- htraverse (Comp . fmap g . f) ≡ Comp . fmap (htraverse g) . htraverse f
 -- @
-htraverse :: Applicative f => (forall x. g x -> f (h x)) -> g :* xs -> f (h :* xs)
+htraverse :: Applicative f => (forall x. g x -> f (h x)) -> xs :& g -> f (xs :& h)
 htraverse f = fmap fromHList . HList.htraverse f . toHList
 {-# INLINE htraverse #-}
 
 -- | 'sequence' analog for extensible products
-hsequence :: Applicative f => Comp f h :* xs -> f (h :* xs)
+hsequence :: Applicative f => xs :& Comp f h -> f (xs :& h)
 hsequence = htraverse getComp
 {-# INLINE hsequence #-}
 
 -- | The dual of 'htraverse'
-hcollect :: (Functor f, Generate xs) => (a -> h :* xs) -> f a -> Comp f h :* xs
+hcollect :: (Functor f, Generate xs) => (a -> xs :& h) -> f a -> xs :& Comp f h
 hcollect f m = htabulate $ \i -> Comp $ fmap (hlookup i . f) m
 {-# INLINABLE hcollect #-}
 
 -- | The dual of 'hsequence'
-hdistribute :: (Functor f, Generate xs) => f (h :* xs) -> Comp f h :* xs
+hdistribute :: (Functor f, Generate xs) => f (xs :& h) -> xs :& Comp f h
 hdistribute = hcollect id
 {-# INLINE hdistribute #-}
 
 -- | 'htraverse' with 'Membership's.
 htraverseWithIndex :: Applicative f
-  => (forall x. Membership xs x -> g x -> f (h x)) -> g :* xs -> f (h :* xs)
+  => (forall x. Membership xs x -> g x -> f (h x)) -> xs :& g -> f (xs :& h)
 htraverseWithIndex f = fmap fromHList . HList.htraverseWithIndex f . toHList
 {-# INLINE htraverseWithIndex #-}
 
 -- | A product filled with the specified value.
-hrepeat :: Generate xs => (forall x. h x) -> h :* xs
+hrepeat :: Generate xs => (forall x. h x) -> xs :& h
 hrepeat x = hfrozen $ newRepeat x
 {-# INLINE hrepeat #-}
 
@@ -220,37 +261,53 @@
 -- 'htabulate' ('hindex' m) ≡ m
 -- 'hindex' ('htabulate' k) ≡ k
 -- @
-htabulate :: Generate xs => (forall x. Membership xs x -> h x) -> h :* xs
+htabulate :: Generate xs => (forall x. Membership xs x -> h x) -> xs :& h
 htabulate f = hfrozen $ new f
 {-# INLINE htabulate #-}
 
 -- | 'Applicative' version of 'htabulate'.
 hgenerate :: (Generate xs, Applicative f)
-  => (forall x. Membership xs x -> f (h x)) -> f (h :* xs)
+  => (forall x. Membership xs x -> f (h x)) -> f (xs :& h)
 hgenerate f = fmap fromHList $ hgenerateList f
 {-# INLINE hgenerate #-}
 
 -- | Pure version of 'hgenerateFor'.
-htabulateFor :: Forall c xs => proxy c -> (forall x. c x => Membership xs x -> h x) -> h :* xs
+htabulateFor :: Forall c xs => proxy c -> (forall x. c x => Membership xs x -> h x) -> xs :& h
 htabulateFor p f = hfrozen $ newFor p f
 {-# INLINE htabulateFor #-}
 
+-- | Pure version of 'hgenerateFor'.
+htabulateWith :: forall c xs h. Forall c xs => (forall x. c x => Membership xs x -> h x) -> xs :& h
+htabulateWith f = hfrozen $ newFor (Proxy @ c) f
+{-# INLINE htabulateWith #-}
+
 -- | A product filled with the specified value.
-hrepeatFor :: Forall c xs => proxy c -> (forall x. c x => h x) -> h :* xs
+hrepeatFor :: Forall c xs => proxy c -> (forall x. c x => h x) -> xs :& h
 hrepeatFor p f = htabulateFor p (const f)
 {-# INLINE hrepeatFor #-}
 
+-- | A product filled with the specified value.
+hrepeatWith :: forall c xs h. Forall c xs => (forall x. c x => h x) -> xs :& h
+hrepeatWith f = htabulateFor (Proxy @ c) (const f)
+{-# INLINE hrepeatWith #-}
+
 -- | 'Applicative' version of 'htabulateFor'.
 hgenerateFor :: (Forall c xs, Applicative f)
-  => proxy c -> (forall x. c x => Membership xs x -> f (h x)) -> f (h :* xs)
+  => proxy c -> (forall x. c x => Membership xs x -> f (h x)) -> f (xs :& h)
 hgenerateFor p f = fmap fromHList $ hgenerateListFor p f
 {-# INLINE hgenerateFor #-}
 
+-- | 'Applicative' version of 'htabulateFor'.
+hgenerateWith :: forall c xs f h. (Forall c xs, Applicative f)
+  => (forall x. c x => Membership xs x -> f (h x)) -> f (xs :& h)
+hgenerateWith f = fmap fromHList $ hgenerateListFor (Proxy @ c) f
+{-# INLINE hgenerateWith #-}
+
 -- | Accumulate sums on a product.
 haccumMap :: Foldable f
-  => (a -> g :| xs)
+  => (a -> xs :/ g)
   -> (forall x. Membership xs x -> g x -> h x -> h x)
-  -> h :* xs -> f a -> h :* xs
+  -> xs :& h -> f a -> xs :& h
 haccumMap f g p0 xs = hmodify
   (\s -> mapM_ (\x -> case f x of EmbedAt i v -> get s i >>= set s i . g i v) xs)
   p0
@@ -259,16 +316,16 @@
 -- | @haccum = 'haccumMap' 'id'@
 haccum :: Foldable f
   => (forall x. Membership xs x -> g x -> h x -> h x)
-  -> h :* xs -> f (g :| xs) -> h :* xs
+  -> xs :& h -> f (xs :/ g) -> xs :& h
 haccum = haccumMap id
 {-# INLINE haccum #-}
 
 -- | Group sums by type.
-hpartition :: (Foldable f, Generate xs) => (a -> h :| xs) -> f a -> Comp [] h :* xs
+hpartition :: (Foldable f, Generate xs) => (a -> xs :/ h) -> f a -> xs :& Comp [] h
 hpartition f = haccumMap f (\_ x (Comp xs) -> Comp (x:xs)) $ hrepeat $ Comp []
 {-# INLINE hpartition #-}
 
 -- | Evaluate every element in a product.
-hforce :: h :* xs -> h :* xs
+hforce :: xs :& h -> xs :& h
 hforce p = hfoldrWithIndex (const seq) p p
 {-# INLINE hforce #-}
diff --git a/src/Data/Extensible/Record.hs b/src/Data/Extensible/Record.hs
--- a/src/Data/Extensible/Record.hs
+++ b/src/Data/Extensible/Record.hs
@@ -103,9 +103,9 @@
 deriveIsRecord :: Name -> DecsQ
 deriveIsRecord name = reify name >>= \case
 #if MIN_VERSION_template_haskell(2,11,0)
-  TyConI (DataD _ _ vars _ [RecC conName vst] _) -> do
+  TyConI (DataD _ _ vars _ [RecC cName vst] _) -> do
 #else
-  TyConI (DataD _ _ vars [RecC conName vst] _) -> do
+  TyConI (DataD _ _ vars [RecC cName vst] _) -> do
 #endif
     let names = [x | (x, _, _) <- vst]
     newNames <- traverse (newName . nameBase) names
@@ -126,11 +126,11 @@
             vst
         , FunD 'recordFromList [Clause
             [shape2Pat $ fmap (\x -> ConP 'Field [ConP 'Identity [VarP x]]) newNames]
-            (NormalB $ RecConE conName [(n, VarE n') | (n, n') <- zip names newNames])
+            (NormalB $ RecConE cName [(n, VarE n') | (n, n') <- zip names newNames])
             []
             ]
         , FunD 'recordToList [Clause
-            [ConP conName (map VarP newNames)]
+            [ConP cName (map VarP newNames)]
             (NormalB $ shape2Exp [AppE (ConE 'Field)
                 $ AppE (ConE 'Identity)
                 $ VarE n
diff --git a/src/Data/Extensible/Struct.hs b/src/Data/Extensible/Struct.hs
--- a/src/Data/Extensible/Struct.hs
+++ b/src/Data/Extensible/Struct.hs
@@ -32,6 +32,7 @@
   , atomicModify_
   , atomicModify'_
   -- * Immutable product
+  , (:&)
   , (:*)
   , unsafeFreeze
   , newFrom
@@ -200,23 +201,26 @@
 
 -- | The type of extensible products.
 --
--- @(:*) :: (k -> *) -> [k] -> *@
+-- @(:&) :: [k] -> (k -> *) -> *@
 --
-data (h :: k -> *) :* (s :: [k]) = HProduct (SmallArray# Any)
+data (s :: [k]) :& (h :: k -> *) = HProduct (SmallArray# Any)
 
+type h :* xs = xs :& h
+{-# DEPRECATED (:*) "Use :& instead" #-}
+
 -- | Turn 'Struct' into an immutable product. The original 'Struct' may not be used.
-unsafeFreeze :: PrimMonad m => Struct (PrimState m) h xs -> m (h :* xs)
+unsafeFreeze :: PrimMonad m => Struct (PrimState m) h xs -> m (xs :& h)
 unsafeFreeze (Struct m) = primitive $ \s -> case unsafeFreezeSmallArray# m s of
   (# s', a #) -> (# s', HProduct a #)
 {-# INLINE unsafeFreeze #-}
 
 -- | Create a new 'Struct' from a product.
-thaw :: PrimMonad m => h :* xs -> m (Struct (PrimState m) h xs)
+thaw :: PrimMonad m => xs :& h -> m (Struct (PrimState m) h xs)
 thaw (HProduct ar) = primitive $ \s -> case thawSmallArray# ar 0# (sizeofSmallArray# ar) s of
   (# s', m #) -> (# s', Struct m #)
 
 -- | The size of a product.
-hlength :: h :* xs -> Int
+hlength :: xs :& h -> Int
 hlength (HProduct ar) = I# (sizeofSmallArray# ar)
 {-# INLINE hlength #-}
 
@@ -228,7 +232,7 @@
 infixr 5 ++
 
 -- | Combine products.
-happend :: (h :* xs) -> (h :* ys) -> (h :* (xs ++ ys))
+happend :: xs :& h -> ys :& h -> (xs ++ ys) :& h
 happend (HProduct lhs) (HProduct rhs) = runST $ primitive $ \s0 ->
   let lhsSz = sizeofSmallArray# lhs
       rhsSz = sizeofSmallArray# rhs
@@ -244,13 +248,13 @@
 unsafeMembership = unsafeCoerce#
 
 -- | Right-associative fold of a product.
-hfoldrWithIndex :: (forall x. Membership xs x -> h x -> r -> r) -> r -> h :* xs -> r
+hfoldrWithIndex :: (forall x. Membership xs x -> h x -> r -> r) -> r -> xs :& h -> r
 hfoldrWithIndex f r p = foldr
   (\i -> let m = unsafeMembership i in f m (hlookup m p)) r [0..hlength p - 1]
 {-# INLINE hfoldrWithIndex #-}
 
 -- | Convert a product into an 'HList'.
-toHList :: forall h xs. h :* xs -> L.HList h xs
+toHList :: forall h xs. xs :& h -> L.HList h xs
 toHList p = go 0 where
   go :: Int -> L.HList h xs
   go i
@@ -265,7 +269,7 @@
 
 -- | Create a new 'Struct' using the contents of a product.
 newFrom :: forall g h m xs. (PrimMonad m)
-  => g :* xs
+  => xs :& g
   -> (forall x. Membership xs x -> g x -> h x)
   -> m (Struct (PrimState m) h xs)
 newFrom hp@(HProduct ar) k = do
@@ -294,18 +298,18 @@
   . newFrom (hfrozen (newForDict d p f)) g = newForDict d p (\i -> g i (f i)) #-}
 
 -- | Get an element in a product.
-hlookup :: Membership xs x -> h :* xs -> h x
+hlookup :: Membership xs x -> xs :& h -> h x
 hlookup (getMemberId -> I# i) (HProduct ar) = case indexSmallArray# ar i of
   (# a #) -> unsafeCoerce# a
 {-# INLINE hlookup #-}
 
 -- | Create a product from an 'ST' action which returns a 'Struct'.
-hfrozen :: (forall s. ST s (Struct s h xs)) -> h :* xs
+hfrozen :: (forall s. ST s (Struct s h xs)) -> xs :& h
 hfrozen m = runST $ m >>= unsafeFreeze
 {-# INLINE[0] hfrozen #-}
 
 -- | Turn a product into a 'Struct' temporarily.
-hmodify :: (forall s. Struct s h xs -> ST s ()) -> h :* xs -> h :* xs
+hmodify :: (forall s. Struct s h xs -> ST s ()) -> xs :& h -> xs :& h
 hmodify f m = runST $ do
   s <- thaw m
   f s
@@ -315,9 +319,9 @@
 {-# RULES "hmodify/batch" forall
   (a :: forall s. Struct s h xs -> ST s ())
   (b :: forall s. Struct s h xs -> ST s ())
-  (x :: h :* xs). hmodify b (hmodify a x) = hmodify (\s -> a s >> b s) x  #-}
+  (x :: xs :& h). hmodify b (hmodify a x) = hmodify (\s -> a s >> b s) x  #-}
 
-instance (Corepresentable p, Comonad (Corep p), Functor f) => Extensible f p (:*) where
+instance (Corepresentable p, Comonad (Corep p), Functor f) => Extensible f p (:&) where
   -- | A lens for a value in a known position.
   pieceAt i pafb = cotabulate $ \ws -> sbt (extract ws) <$> cosieve pafb (hlookup i <$> ws) where
     sbt xs !x = hmodify (\s -> set s i x) xs
diff --git a/src/Data/Extensible/Sum.hs b/src/Data/Extensible/Sum.hs
--- a/src/Data/Extensible/Sum.hs
+++ b/src/Data/Extensible/Sum.hs
@@ -13,7 +13,8 @@
 --
 ------------------------------------------------------------------------
 module Data.Extensible.Sum (
-   (:|)(..)
+  (:/)(..)
+  , (:|)
   , hoist
   , embed
   , strike
@@ -33,34 +34,37 @@
 --
 -- @(:|) :: (k -> *) -> [k] -> *@
 --
-data (h :: k -> *) :| (s :: [k]) where
-  EmbedAt :: !(Membership xs x) -> h x -> h :| xs
+data (xs :: [k]) :/ (h :: k -> *) where
+  EmbedAt :: !(Membership xs x) -> h x -> xs :/ h
 
-instance Enum (Proxy :| xs) where
+type h :| xs = xs :/ h
+{-# DEPRECATED (:|) "Use :/ instead" #-}
+
+instance Enum (xs :/ Proxy) where
   fromEnum (EmbedAt m _) = fromIntegral $ getMemberId m
   toEnum i = reifyMembership (fromIntegral i) $ \m -> EmbedAt m Proxy
 
-instance (Last xs ∈ xs) => Bounded (Proxy :| xs) where
+instance (Last xs ∈ xs) => Bounded (xs :/ Proxy) where
   minBound = reifyMembership 0 $ \m -> EmbedAt m Proxy
   maxBound = EmbedAt (membership :: Membership xs (Last xs)) Proxy
 
 -- | Change the wrapper.
-hoist :: (forall x. g x -> h x) -> g :| xs -> h :| xs
+hoist :: (forall x. g x -> h x) -> xs :/ g -> xs :/ h
 hoist f (EmbedAt p h) = EmbedAt p (f h)
 {-# INLINE hoist #-}
 
 -- | /O(1)/ lift a value.
-embed :: (x ∈ xs) => h x -> h :| xs
+embed :: (x ∈ xs) => h x -> xs :/ h
 embed = EmbedAt membership
 {-# INLINE embed #-}
 
 -- | Try to extract something you want.
-strike :: forall h x xs. (x ∈ xs) => h :| xs -> Maybe (h x)
+strike :: forall h x xs. (x ∈ xs) => xs :/ h -> Maybe (h x)
 strike = strikeAt membership
 {-# INLINE strike #-}
 
 -- | Try to extract something you want.
-strikeAt :: forall h x xs. Membership xs x -> h :| xs -> Maybe (h x)
+strikeAt :: forall h x xs. Membership xs x -> xs :/ h -> Maybe (h x)
 strikeAt q (EmbedAt p h) = case compareMembership p q of
   Right Refl -> Just h
   _ -> Nothing
@@ -68,8 +72,8 @@
 
 -- | /O(1)/ Naive pattern match
 (<:|) :: (h x -> r)
-    -> (h :| xs -> r)
-    -> h :| (x ': xs)
+    -> (xs :/ h -> r)
+    -> (x ': xs) :/ h
     -> r
 (<:|) r c = \(EmbedAt i h) -> testMembership i
   (\Refl -> r h)
@@ -78,15 +82,15 @@
 {-# INLINE (<:|) #-}
 
 -- | There is no empty union.
-exhaust :: h :| '[] -> r
+exhaust :: '[] :/ h -> r
 exhaust _ = error "Impossible"
 
 -- | Embed a value, but focuses on its key.
-embedAssoc :: Lookup xs k a => h (k ':> a) -> h :| xs
+embedAssoc :: Lookup xs k a => h (k ':> a) -> xs :/ h
 embedAssoc = EmbedAt association
 {-# INLINE embedAssoc #-}
 
-instance (Applicative f, Choice p) => Extensible f p (:|) where
+instance (Applicative f, Choice p) => Extensible f p (:/) where
   pieceAt m = dimap (\t@(EmbedAt i h) -> case compareMembership i m of
     Right Refl -> Right h
     Left _ -> Left t) (either pure (fmap (EmbedAt m))) . right'
diff --git a/src/Data/Extensible/Tangle.hs b/src/Data/Extensible/Tangle.hs
--- a/src/Data/Extensible/Tangle.hs
+++ b/src/Data/Extensible/Tangle.hs
@@ -29,28 +29,28 @@
 import Data.Extensible.Wrapper
 
 -- | @'TangleT' h xs m@ is the monad of computations that may depend on the elements in 'xs'.
-newtype TangleT h xs m a = TangleT
-  { unTangleT :: RWST (Comp (TangleT h xs m) h :* xs) () (Nullable h :* xs) m a }
+newtype TangleT xs h m a = TangleT
+  { unTangleT :: RWST (xs :& Comp (TangleT xs h m) h) () (xs :& Nullable h) m a }
   deriving (Functor, Applicative, Monad)
 
-instance MonadTrans (TangleT h xs) where
+instance MonadTrans (TangleT xs h) where
   lift = TangleT . lift
 
-instance (Monad m, Semigroup a) => Semigroup (TangleT h xs m a) where
+instance (Monad m, Semigroup a) => Semigroup (TangleT xs h m a) where
   (<>) = liftA2 (<>)
 
-instance (Monad m, Monoid a) => Monoid (TangleT h xs m a) where
+instance (Monad m, Monoid a) => Monoid (TangleT xs h m a) where
   mempty = pure mempty
   mappend = (<>)
 
 -- | Hitch an element associated to the 'FieldName' through a wrapper.
 lasso :: forall k v m h xs. (Monad m, Lookup xs k v, Wrapper h)
-  => FieldName k -> TangleT h xs m (Repr h (k ':> v))
+  => FieldName k -> TangleT xs h m (Repr h (k ':> v))
 lasso _ = view _Wrapper <$> hitchAt (association :: Membership xs (k ':> v))
 {-# INLINE lasso #-}
 
 -- | Take a value from the tangles. The result is memoized.
-hitchAt :: Monad m => Membership xs x -> TangleT h xs m (h x)
+hitchAt :: Monad m => Membership xs x -> TangleT xs h m (h x)
 hitchAt k = TangleT $ do
   mem <- get
   case getNullable $ hlookup k mem of
@@ -63,27 +63,27 @@
 
 -- | Run a 'TangleT' action and return the result and the calculated values.
 runTangleT :: Monad m
-  => Comp (TangleT h xs m) h :* xs
-  -> Nullable h :* xs
-  -> TangleT h xs m a
-  -> m (a, Nullable h :* xs)
+  => xs :& Comp (TangleT xs h m) h
+  -> xs :& Nullable h
+  -> TangleT xs h m a
+  -> m (a, xs :& Nullable h)
 runTangleT tangles rec0 (TangleT m) = (\(a, s, _) -> (a, s))
   <$> runRWST m tangles rec0
 {-# INLINE runTangleT #-}
 
 -- | Run a 'TangleT' action.
 evalTangleT :: Monad m
-  => Comp (TangleT h xs m) h :* xs
-  -> Nullable h :* xs
-  -> TangleT h xs m a
+  => xs :& Comp (TangleT xs h m) h
+  -> xs :& Nullable h
+  -> TangleT xs h m a
   -> m a
 evalTangleT tangles rec0 (TangleT m) = fst <$> evalRWST m tangles rec0
 {-# INLINE evalTangleT #-}
 
 -- | Run tangles and collect all the results as a 'Record'.
 runTangles :: Monad m
-  => Comp (TangleT h xs m) h :* xs
-  -> Nullable h :* xs
-  -> m (h :* xs)
+  => xs :& Comp (TangleT xs h m) h
+  -> xs :& Nullable h
+  -> m (xs :& h)
 runTangles ts vs = evalTangleT ts vs $ htraverseWithIndex (const . hitchAt) vs
 {-# INLINE runTangles #-}