diff --git a/ChangeLog.md b/ChangeLog.md
--- a/ChangeLog.md
+++ b/ChangeLog.md
@@ -1,5 +1,12 @@
 # Changelog for barbies
 
+## 2.0.3.0
+  - Add Barbies.Bi.bttraverse_
+  - Add Barbies.Bi.btfoldMap
+  - Fix failure to derive Constraints{B,T} for proper
+    bi-barbies.
+  - Builds with ghc 9 (Fumiaki Kinoshita)
+
 ## 2.0.2.0
   - Add `Barbies.Bare.WearTwo` type family to support having _field-specific_
     newtype wrappers that get applied only to the covered barbie (Lennart
diff --git a/LICENSE b/LICENSE
--- a/LICENSE
+++ b/LICENSE
@@ -1,4 +1,4 @@
-Copyright Author name here (c) 2018
+Copyright Daniel Gorin (c) 2018
 
 All rights reserved.
 
diff --git a/barbies.cabal b/barbies.cabal
--- a/barbies.cabal
+++ b/barbies.cabal
@@ -1,5 +1,5 @@
 name:           barbies
-version:        2.0.2.0
+version:        2.0.3.0
 synopsis:       Classes for working with types that can change clothes.
 description:    Types that are parametric on a functor are like Barbies that have an outfit for each role. This package provides the basic abstractions to work with them comfortably.
 category:       Data-structures
diff --git a/src/Barbies/Bi.hs b/src/Barbies/Bi.hs
--- a/src/Barbies/Bi.hs
+++ b/src/Barbies/Bi.hs
@@ -20,6 +20,8 @@
     --   and a 'TraversableB'.
   , bttraverse
   , bttraverse1
+  , bttraverse_
+  , btfoldMap
 
    -- * Applicative
    -- | If @t@ is an 'ApplicativeT', the type of 'tpure' shows that its
@@ -37,12 +39,15 @@
 
 
 import Barbies.Internal.Trivial (Unit(..))
+import Barbies.Internal.Writer (execWr, tell)
 import Data.Functor.Barbie
 import Data.Functor.Transformer
 
 import Control.Applicative (Alternative(..))
 import Control.Monad ((>=>))
 import Data.Monoid (Alt(..))
+import Data.Functor (void)
+import Data.Functor.Const (Const(..))
 import Data.Functor.Product (Product(..))
 
 -- {{ Functor -----------------------------------------------------------------
@@ -103,6 +108,36 @@
 bttraverse1 h
   = bttraverse h h
 {-# INLINE bttraverse1 #-}
+
+-- | Map each element to an action, evaluate these actions from left to right
+--   and ignore the results.
+bttraverse_
+  :: ( TraversableB (b f)
+     , TraversableT b
+     , Monad e
+     )
+  => (forall a. f a -> e c)
+  -> (forall a. g a -> e d)
+  -> b f g
+  -> e ()
+bttraverse_ hf hg
+  = void . bttraverse (neuter . hf) (neuter . hg)
+  where
+    neuter
+      = fmap (const $ Const ())
+
+-- | Map each element to a monoid, and combine the results.
+btfoldMap
+  :: ( TraversableB (b f)
+     , TraversableT b
+     , Monoid m
+     )
+  => (forall a. f a -> m)
+  -> (forall a. g a -> m)
+  -> b f g -> m
+btfoldMap hf hg
+  = execWr . bttraverse_ (tell . hf) (tell . hg)
+
 -- }} Traversable -------------------------------------------------------------
 
 
diff --git a/src/Barbies/Generics/Applicative.hs b/src/Barbies/Generics/Applicative.hs
--- a/src/Barbies/Generics/Applicative.hs
+++ b/src/Barbies/Generics/Applicative.hs
@@ -8,12 +8,13 @@
 
 
 import Data.Functor.Product(Product(..))
+import Data.Kind(Type)
 import Data.Proxy(Proxy (..))
 
 import Data.Generics.GenericN
 
 
-class GApplicative n (f :: k -> *) (g :: k -> *) repbf repbg repbfg where
+class GApplicative n (f :: k -> Type) (g :: k -> Type) repbf repbg repbfg where
   gprod
     :: Proxy n
     -> Proxy f
diff --git a/src/Barbies/Generics/Constraints.hs b/src/Barbies/Generics/Constraints.hs
--- a/src/Barbies/Generics/Constraints.hs
+++ b/src/Barbies/Generics/Constraints.hs
@@ -4,7 +4,7 @@
 module Barbies.Generics.Constraints
   ( GAll
   , X, Y
-  , TagSelf, TagSelf', Self, Other
+  , Self, Other, SelfOrOther
   , GConstraints(..)
   )
 
@@ -14,7 +14,7 @@
 
 import Data.Functor.Product (Product (..))
 import Data.Kind            (Constraint, Type)
-import GHC.TypeLits         (Nat, type (+))
+import GHC.TypeLits         (Nat)
 
 import Data.Generics.GenericN
 
@@ -26,8 +26,6 @@
 data X a
 data family Y :: k
 
-
-
 -- ----------------------------------
 -- Trivial cases
 -- ----------------------------------
@@ -96,34 +94,39 @@
 
 type P = Param
 
-
-type instance GAll n c (Rec (P n X _) (X a)) = c a
+type instance GAll n c (Rec l r) = GAllRec n c l r
+type family GAllRec
+  (n :: Nat)
+  (c :: k -> Constraint)
+  (l :: Type)
+  (r :: Type) :: Constraint
+  where
+    GAllRec n c (P n X _) (X a) = c a
+    GAllRec _ _ _ _ = ()
 
 -- {{ Functor application -----------------------------------------------------
 instance
+  -- a' is a, maybe with Param applications
   GConstraints n c f (Rec (P n X a') (X a))
-                     (Rec (P n f a) (f a))
-                     (Rec (P n (Dict c `Product` f) a)
+                     (Rec (P n f a') (f a))
+                     (Rec (P n (Dict c `Product` f) a')
                               ((Dict c `Product` f) a))
   where
   gaddDicts
     = Rec . K1 . Pair Dict . unK1 . unRec
   {-# INLINE gaddDicts #-}
+
 -- }} Functor application -----------------------------------------------------
 
 -- {{ Not a functor application -----------------------------------------------
 
--- Break all recursive cases
--- b' is b, maybe with 'Param' annotations
-type instance GAll 0 c (Rec (Self b' (P 0 X)) (b X)) = ()
-type instance GAll 1 c (Rec (Self b' (P 1 X) (P 0 Y)) (b X Y)) = ()
-
-type instance GAll n c (Rec a a) = ()
-
 instance
-  GConstraints n c f (Rec a' a)
-                     (Rec a a)
-                     (Rec a a)
+  -- b is a, but with X or Y instead of Param ...
+  -- a' is a, maybe with occurrences of Param
+  -- b' is b, maybe with occurences of Param
+  GConstraints n c f (Rec a' a) -- a' may contain Y or Param m (m > n)
+                     (Rec b' b) -- a'' may only contain Param m (m > n)
+                     (Rec b' b)
   where
   gaddDicts = id
   {-# INLINE gaddDicts #-}
@@ -135,49 +138,9 @@
 --
 -- ============================================================================
 
-data family Self  (b :: k -> k') :: k -> k'
-data family Other (b :: k -> k') :: k -> k'
-
--- | We use the type-families to generically compute @'Barbies.AllB' c b@. Intuitively, if
---   @b' f@ occurs inside @b f@, then we should just add @'Barbies.AllB' b' c@ to
---   @'Barbies.AllB' b c@. The problem is that if @b@ is a recursive type, and @b'@ is @b@,
---   then ghc will choke and blow the stack (instead of computing a fixpoint).
---
---   So, we would like to behave differently when @b = b'@ and add @()@ instead
---   of @'Barbies.AllB' b f@ to break the recursion. Our trick will be to use a type
---   family to inspect @'RepN' (b f)@ and distinguish recursive usages from
---   non-recursive ones, tagging them with different types, so we can distinguish
---   them in the instances.
-type TagSelf n b repbf
-  = TagSelf' n b (Indexed b (n + 1)) repbf
-
-type family TagSelf' (n :: Nat) (b :: kb) (b' :: kb) (repbf :: * -> *) :: * -> * where
-  TagSelf' n b b' (M1 mt m s)
-    = M1 mt m (TagSelf' n b b' s)
-
-  TagSelf' n b b' (l :+: r)
-    = TagSelf' n b b' l :+: TagSelf' n b b' r
-
-  TagSelf' n b b' (l :*: r)
-    = TagSelf' n b b' l :*: TagSelf' n b b' r
-
-  TagSelf' 0 b  b' (Rec (b' f) (b g))
-    = Rec (Self b' f) (b g)
-
-  TagSelf' 0 (b :: k -> *) b' (Rec ((b'' :: k -> *) f) ((b''' :: k -> *) g))
-    = Rec (Other b'' f) (b''' g)
-
-  TagSelf' 1 b  b' (Rec (b' fl fr) (b gl gr))
-    = Rec (Self b' fl fr) (b gl gr)
-
-  TagSelf' 1 (b :: kl -> kr ->  *) b' (Rec ((b'' :: kl -> kr -> *) fl fr) ((b''' :: kl -> kr -> *) gl gr))
-    = Rec (Other b'' fl fr) (b''' gl gr)
-
-  TagSelf' n b b' (Rec p a)
-    = Rec p a
-
-  TagSelf' n b b' U1
-    = U1
+data Self  (p :: Type) (a :: Type) (x :: Type)
+data Other (p :: Type) (a :: Type) (x :: Type)
 
-  TagSelf' n b b' V1
-    = V1
+type family SelfOrOther (b :: k) (b' :: k) :: Type -> Type -> Type -> Type where
+  SelfOrOther b b = Self
+  SelfOrOther b b' = Other
diff --git a/src/Barbies/Internal.hs b/src/Barbies/Internal.hs
--- a/src/Barbies/Internal.hs
+++ b/src/Barbies/Internal.hs
@@ -31,20 +31,19 @@
   , Internal.CanDeriveConstraintsB
   , Internal.CanDeriveConstraintsT
 
-
   , Generics.GAll
   , Internal.GAllRepB
   , Internal.GAllRepT
   , Generics.X, Generics.Y
-  , Generics.TagSelf, Generics.TagSelf', Generics.Self, Generics.Other
+  , Generics.Self, Generics.Other, Generics.SelfOrOther
+  , Internal.TagSelf0, Internal.TagSelf0'
+  , Internal.TagSelf1, Internal.TagSelf1'
 
     -- * Bare values
   , Internal.gbcoverDefault
   , Internal.gbstripDefault
   , Generics.GBare(..)
   , Internal.CanDeriveBareB
-
-
 
     -- * Generic derivation support
   , module Data.Generics.GenericN
diff --git a/src/Barbies/Internal/ApplicativeT.hs b/src/Barbies/Internal/ApplicativeT.hs
--- a/src/Barbies/Internal/ApplicativeT.hs
+++ b/src/Barbies/Internal/ApplicativeT.hs
@@ -73,7 +73,7 @@
 class FunctorT t => ApplicativeT (t :: (k -> Type) -> (k' -> Type)) where
   tpure
     :: (forall a . f a)
-    -> (forall x . t f x)
+    -> t f x
 
   tprod
     :: t f x
diff --git a/src/Barbies/Internal/ConstraintsB.hs b/src/Barbies/Internal/ConstraintsB.hs
--- a/src/Barbies/Internal/ConstraintsB.hs
+++ b/src/Barbies/Internal/ConstraintsB.hs
@@ -19,11 +19,20 @@
   , CanDeriveConstraintsB
   , gbaddDictsDefault
   , GAllRepB
+
+  , TagSelf0, TagSelf0'
   )
 
 where
 
-import Barbies.Generics.Constraints(GConstraints(..), GAll, TagSelf, Self, Other, X)
+import Barbies.Generics.Constraints
+  ( GConstraints(..)
+  , GAll
+  , Self
+  , Other
+  , SelfOrOther
+  , X
+  )
 import Barbies.Internal.ApplicativeB(ApplicativeB(..))
 import Barbies.Internal.Dicts(ClassF, Dict (..), requiringDict)
 import Barbies.Internal.FunctorB(FunctorB (..))
@@ -33,7 +42,7 @@
 import Data.Functor.Const   (Const (..))
 import Data.Functor.Product (Product (..))
 import Data.Functor.Sum     (Sum (..))
-import Data.Kind            (Constraint)
+import Data.Kind            (Constraint, Type)
 import Data.Proxy           (Proxy (..))
 
 import Data.Generics.GenericN
@@ -70,7 +79,7 @@
 -- derive instance 'Generic' (T f)
 -- instance 'ConstraintsB' T
 -- @
-class FunctorB b => ConstraintsB (b :: (k -> *) -> *) where
+class FunctorB b => ConstraintsB (b :: (k -> Type) -> Type) where
   -- | @'AllB' c b@ should contain a constraint @c a@ for each
   --   @a@ occurring under an @f@ in @b f@. E.g.:
   --
@@ -229,16 +238,15 @@
 --       @'ConstraintsB' b@ instance. In particular, recursive usages of @B f@
 --       are allowed.
 type CanDeriveConstraintsB c b f
-  = ( GenericP 0 (b f)
-    , GenericP 0 (b (Dict c `Product` f))
+  = ( GenericN (b f)
+    , GenericN (b (Dict c `Product` f))
     , AllB c b ~ GAll 0 c (GAllRepB b)
-    , GConstraints 0 c f (GAllRepB b) (RepP 0 (b f)) (RepP 0 (b (Dict c `Product` f)))
+    , GConstraints 0 c f (GAllRepB b) (RepN (b f)) (RepN (b (Dict c `Product` f)))
     )
 
 -- | The representation used for the generic computation of the @'AllB' c b@
---   constraints. Here 'X' is an arbitrary constant since the actual
---   argument to @b@ is irrelevant.
-type GAllRepB b = TagSelf 0 b (RepN (b X))
+--   constraints.
+type GAllRepB b = TagSelf0 b
 
 
 -- ===============================================================
@@ -254,7 +262,7 @@
   => b f
   -> b (Dict c `Product` f)
 gbaddDictsDefault
-  = toP (Proxy @0) . gaddDicts @0 @c @f @(GAllRepB b) . fromP (Proxy @0)
+  = toN . gaddDicts @0 @c @f @(GAllRepB b) . fromN
 {-# INLINE gbaddDictsDefault #-}
 
 
@@ -264,35 +272,40 @@
 
 type P = Param
 
+-- Break recursive case
+type instance GAll 0 c (Self (b' (P 0 X)) (b X)) = ()
 
 instance
   ( ConstraintsB b
   , AllB c b
-  ) => -- b' is b, maybe with 'Param' annotations
-       GConstraints 0 c f (Rec (Self b' (P 0 X)) (b X))
-                          (Rec (b (P 0 f)) (b f))
-                          (Rec (b (P 0 (Dict c `Product` f)))
-                               (b      (Dict c `Product` f)))
+  ) => -- b' is b with maybe some Param occurrences
+       GConstraints 0 c f (Self (b' (P 0 X)) (b X))
+                          (Rec (b' (P 0 f)) (b f))
+                          (Rec (b' (P 0 (Dict c `Product` f)))
+                               (b       (Dict c `Product` f)))
   where
   gaddDicts
     = Rec . K1 . baddDicts . unK1 . unRec
   {-# INLINE gaddDicts #-}
 
 
-type instance GAll 0 c (Rec (Other b (P 0 X)) (b' X)) = AllB c b'
+type instance GAll 0 c (Other (b' (P 0 X)) (b X)) = AllB c b
 
+
 instance
   ( ConstraintsB b
   , AllB c b
-  ) => GConstraints 0 c f (Rec (Other b' (P 0 X)) (b X))
-                          (Rec (b (P 0 f)) (b f))
-                          (Rec (b (P 0 (Dict c `Product` f)))
-                               (b      (Dict c `Product` f)))
+  ) => -- b' is b with maybe some Param occurrences
+       GConstraints 0 c f (Other (b' (P 0 X)) (b X))
+                          (Rec (b' (P 0 f)) (b f))
+                          (Rec (b' (P 0 (Dict c `Product` f)))
+                               (b       (Dict c `Product` f)))
   where
   gaddDicts
     = Rec . K1 . baddDicts . unK1 . unRec
   {-# INLINE gaddDicts #-}
 
+
 -- --------------------------------
 -- Instances for base types
 -- --------------------------------
@@ -328,3 +341,46 @@
   baddDicts (Compose x)
     = Compose (baddDicts <$> x)
   {-# INLINE baddDicts #-}
+
+-- ============================================================================
+-- ## Identifying recursive usages of the barbie-type ##
+-- ============================================================================
+
+-- | We use the type-families to generically compute @'Barbies.AllB' c b@.
+--   Intuitively, if @b' f'@ occurs inside @b f@, then we should just add
+--   @'Barbies.AllB' b' c@ to @'Barbies.AllB' b c@. The problem is that if @b@
+--   is a recursive type, and @b'@ is @b@, then ghc will choke and blow the stack
+--   (instead of computing a fixpoint).
+--
+--   So, we would like to behave differently when @b = b'@ and add @()@ instead
+--   of @'Barbies.AllB' b c@ to break the recursion. Our trick will be to use a type
+--   family to inspect @'Rep' (b X)@, for an arbitrary @X@,  and distinguish
+--   recursive usages from non-recursive ones, tagging them with different types,
+--   so we can distinguish them in the instances.
+type TagSelf0 b
+  = TagSelf0' (Indexed b 1) (RepN (b X))
+
+type family TagSelf0' (b :: kf -> Type) (repbf :: Type -> Type) :: Type -> Type where
+  TagSelf0' b (M1 mt m s)
+    = M1 mt m (TagSelf0' b s)
+
+  TagSelf0' b (l :+: r)
+    = TagSelf0' b l :+: TagSelf0' b r
+
+  TagSelf0' b (l :*: r)
+    = TagSelf0' b l :*: TagSelf0' b r
+
+  TagSelf0' (b :: kf -> Type)
+            (Rec ((b'  :: kf -> Type) f)
+                 ((b'' :: kf -> Type) g)
+            )
+    = (SelfOrOther b b') (b' f) (b'' g)
+
+  TagSelf0' b (Rec x y)
+    = Rec x y
+
+  TagSelf0' b U1
+    = U1
+
+  TagSelf0' b V1
+    = V1
diff --git a/src/Barbies/Internal/ConstraintsT.hs b/src/Barbies/Internal/ConstraintsT.hs
--- a/src/Barbies/Internal/ConstraintsT.hs
+++ b/src/Barbies/Internal/ConstraintsT.hs
@@ -19,19 +19,26 @@
   , CanDeriveConstraintsT
   , gtaddDictsDefault
   , GAllRepT
+
+  , TagSelf1, TagSelf1'
   )
 
 where
 
 import Barbies.Internal.ApplicativeT(ApplicativeT (..))
-import Barbies.Generics.Constraints(GConstraints(..), GAll, TagSelf, Self, Other, X, Y)
+import Barbies.Generics.Constraints
+  ( GConstraints(..)
+  , GAll
+  , Self, Other, SelfOrOther
+  , X, Y
+  )
 import Barbies.Internal.Dicts(ClassF, Dict (..), requiringDict)
 import Barbies.Internal.FunctorT(FunctorT (..))
 import Barbies.Internal.TraversableT(TraversableT (..))
 
 import Data.Functor.Const(Const(..))
 import Data.Functor.Product(Product(..))
-import Data.Kind(Constraint)
+import Data.Kind(Constraint, Type)
 import Data.Proxy(Proxy(..))
 
 import Data.Generics.GenericN
@@ -68,7 +75,7 @@
 -- derive instance 'Generic' (T f a)
 -- instance 'ConstraintsT' T
 -- @
-class FunctorT t => ConstraintsT (t :: (kl -> *) -> (kr -> *)) where
+class FunctorT t => ConstraintsT (t :: (kl -> Type) -> (kr -> Type)) where
   -- | @'AllT' c t@ should contain a constraint @c a@ for each
   --   @a@ occurring under an @f@ in @t f@.
   --
@@ -220,17 +227,17 @@
 --       @'ConstraintsT' t@ instance. In particular, recursive usages of @T f x@
 --       are allowed.
 type CanDeriveConstraintsT c t f x
-  = ( GenericP 1 (t f x)
-    , GenericP 1 (t (Dict c `Product` f) x)
+  = ( GenericN (t f x)
+    , GenericN (t (Dict c `Product` f) x)
     , AllT c t ~ GAll 1 c (GAllRepT t)
-    , GConstraints 1 c f (GAllRepT t) (RepP 1 (t f x)) (RepP 1 (t (Dict c `Product` f) x))
+    , GConstraints 1 c f (GAllRepT t) (RepN (t f x)) (RepN (t (Dict c `Product` f) x))
     )
 
 -- | The representation used for the generic computation of the @'AllT' c t@
---   constraints. Here 'X' and 'Y' are arbitrary constants since the actual
---   argument to @t@ is irrelevant.
-type GAllRepT t = TagSelf 1 t (RepN (t X Y))
+--   constraints. .
+type GAllRepT t = TagSelf1 t
 
+
 -- ===============================================================
 --  Generic derivations
 -- ===============================================================
@@ -244,7 +251,8 @@
   => t f x
   -> t (Dict c `Product` f) x
 gtaddDictsDefault
-  = toP (Proxy @1) . gaddDicts @1 @c @f @(GAllRepT t) . fromP (Proxy @1)
+  = toN . gaddDicts @1 @c @f @(GAllRepT t) . fromN
+
 {-# INLINE gtaddDictsDefault #-}
 
 
@@ -254,30 +262,73 @@
 
 type P = Param
 
+-- Break recursive case
+type instance GAll 1 c (Self (t' (P 1 X) Y) (t X Y)) = ()
+
 instance
   ( ConstraintsT t
   , AllT c t
-  ) => -- t' is t, maybe with 'Param' annotations
-       GConstraints 1 c f (Rec (Self t' (P 1 X) (P 0 Y)) (t X Y))
-                          (Rec (t (P 1 f) y) (t f y))
-                          (Rec (t (P 1 (Dict c `Product` f)) y)
-                               (t      (Dict c `Product` f)  y))
+  ) => -- t' is t, maybe with some Param occurrences
+       GConstraints 1 c f (Self (t' (P 1 X) Y) (t X Y))
+                          (Rec (t' (P 1 f) (P 0 y)) (t f y))
+                          (Rec (t' (P 1 (Dict c `Product` f)) (P 0 y))
+                               (t       (Dict c `Product` f)       y))
   where
   gaddDicts
     = Rec . K1 . taddDicts . unK1 . unRec
   {-# INLINE gaddDicts #-}
 
 
-type instance GAll 1 c (Rec (Other t (P 1 X) (P 0 Y)) (t' X Y)) = AllT c t'
+type instance GAll 1 c (Other (t' (P 1 X) Y) (t X Y)) = AllT c t
 
 instance
   ( ConstraintsT t
   , AllT c t
-  ) => GConstraints 1 c f (Rec (Other t' (P 1 X) (P 0 Y)) (t X Y))
-                          (Rec (t (P 1 f) y) (t f y))
-                          (Rec (t (P 1 (Dict c `Product` f)) y)
-                               (t      (Dict c `Product` f)  y))
+  ) => -- t' is t maybe with some Param occurrences
+       GConstraints 1 c f (Other (t' (P 1 X) Y) (t X Y))
+                          (Rec (t' (P 1 f) (P 0 y)) (t f y))
+                          (Rec (t' (P 1 (Dict c `Product` f)) (P 0 y))
+                               (t       (Dict c `Product` f)       y))
   where
   gaddDicts
     = Rec . K1 . taddDicts . unK1 . unRec
   {-# INLINE gaddDicts #-}
+
+-- | We use the type-families to generically compute @'Barbies.AllT' c b@.
+--   Intuitively, if @t' f' x'@ occurs inside @t f x@, then we should just add
+--   @'Barbies.AllT' t' c@ to @'Barbies.AllT' t c@. The problem is that if @t@
+--   is a recursive type, and @t'@ is @t@, then ghc will choke and blow the
+--   stack (instead of computing a fixpoint).
+--
+--   So, we would like to behave differently when @t = t'@ and add @()@ instead
+--   of @'Barbies.AllT' t c@ to break the recursion. Our trick will be to use a
+--   type family to inspect @'Rep' (t X Y)@, for arbitrary @X@ and @Y@ and
+--   distinguish recursive usages from non-recursive ones, tagging them with
+--   different types, so we can distinguish them in the instances.
+type TagSelf1 b
+  = TagSelf1' (Indexed b 2) (Zip (Rep (Indexed (b X) 1 Y)) (Rep (b X Y)))
+
+type family TagSelf1' (b :: kf -> kg -> Type) (repbf :: Type -> Type) :: Type -> Type where
+  TagSelf1' b (M1 mt m s)
+    = M1 mt m (TagSelf1' b s)
+
+  TagSelf1' b (l :+: r)
+    = TagSelf1' b l :+: TagSelf1' b r
+
+  TagSelf1' b (l :*: r)
+    = TagSelf1' b l :*: TagSelf1' b r
+
+  TagSelf1' (b :: kf -> kg -> Type)
+            (Rec ((b'  :: kf -> kg -> Type) fl fr)
+                 ((b'' :: kf -> kg -> Type) gl gr)
+            )
+    = (SelfOrOther b b') (b' fl gr) (b'' gl gr)
+
+  TagSelf1' b (Rec x y)
+    = Rec x y
+
+  TagSelf1' b U1
+    = U1
+
+  TagSelf1' b V1
+    = V1
diff --git a/src/Barbies/Internal/FunctorT.hs b/src/Barbies/Internal/FunctorT.hs
--- a/src/Barbies/Internal/FunctorT.hs
+++ b/src/Barbies/Internal/FunctorT.hs
@@ -45,7 +45,7 @@
 -- There is a default 'tmap' implementation for 'Generic' types, so
 -- instances can derived automatically.
 class FunctorT (t :: (k -> Type) -> k' -> Type) where
-  tmap :: (forall a . f a -> g a) -> (forall x. t f x -> t g x)
+  tmap :: (forall a . f a -> g a) -> t f x -> t g x
 
   default tmap
     :: forall f g x
diff --git a/src/Barbies/Internal/TraversableT.hs b/src/Barbies/Internal/TraversableT.hs
--- a/src/Barbies/Internal/TraversableT.hs
+++ b/src/Barbies/Internal/TraversableT.hs
@@ -53,7 +53,7 @@
   ttraverse
     :: Applicative e
     => (forall a . f a -> e (g a))
-    -> (forall x . t f x -> e (t g x))
+    -> t f x -> e (t g x)
 
   default ttraverse
     :: ( Applicative e, CanDeriveTraversableT t f g x)
diff --git a/src/Barbies/Internal/Writer.hs b/src/Barbies/Internal/Writer.hs
--- a/src/Barbies/Internal/Writer.hs
+++ b/src/Barbies/Internal/Writer.hs
@@ -32,6 +32,19 @@
         in (f x, s'')
   {-# INLINE (<*>) #-}
 
+instance Monad (St s) where
+  return = pure
+  {-# INLINE return #-}
+
+  St action >>= f
+    = St $ \s ->
+        let
+          (a, s') = action s
+          St go  = f a
+        in
+          go s'
+  {-# INLINE (>>=) #-}
+
 type Wr = St
 
 execWr :: Monoid w => Wr w a -> w
@@ -40,4 +53,4 @@
 
 tell :: Monoid w => w -> Wr w ()
 tell w
-  = St (\s -> ((), s `mappend` w))
+  = St (\s -> ((), seq s s `mappend` w))
diff --git a/src/Data/Barbie/Internal/Product.hs b/src/Data/Barbie/Internal/Product.hs
--- a/src/Data/Barbie/Internal/Product.hs
+++ b/src/Data/Barbie/Internal/Product.hs
@@ -74,7 +74,7 @@
   = toN $ gbuniq (Proxy @f) (Proxy @(RepN (b f))) (Proxy @(RepN (b (f `Product` f)))) x
 {-# INLINE gbuniqDefault #-}
 
-class GProductB (f :: k -> *) (g :: k -> *) repbf repbg repbfg where
+class GProductB (f :: k -> Type) (g :: k -> Type) repbf repbg repbfg where
   gbprod :: Proxy f -> Proxy g -> repbf x -> repbg x -> repbfg x
 
   gbuniq :: (f ~ g, repbf ~ repbg) => Proxy f -> Proxy repbf -> Proxy repbfg -> (forall a . f a) -> repbf x
diff --git a/src/Data/Barbie/Internal/ProductC.hs b/src/Data/Barbie/Internal/ProductC.hs
--- a/src/Data/Barbie/Internal/ProductC.hs
+++ b/src/Data/Barbie/Internal/ProductC.hs
@@ -100,25 +100,23 @@
 
 type P0 = Param 0
 
-instance GProductBC c (Rec (P0 X a_or_pma) (X a))
-                      (Rec (P0 (Dict c) a_or_pma) (Dict c a)) where
+instance c a => GProductBC c (Rec (P0 X a_or_pma) (X a))
+                             (Rec (P0 (Dict c) a_or_pma) (Dict c a)) where
   gbdicts = Rec (K1 Dict)
   {-# INLINE gbdicts #-}
 
 instance
   ( ProductBC b
   , AllB c b
-  ) => GProductBC c (Rec (Self b' (P0 X)) (b X))
-                    (Rec      (b' (P0 (Dict c)))
-                              (b     (Dict c))) where
+  ) => GProductBC c (Self (b' (P0 X)) (b X))
+                    (Rec (b' (P0 (Dict c))) (b (Dict c))) where
   gbdicts = Rec $ K1 $ bdicts @_ @b
 
 instance
   ( ProductBC b
   , AllB c b
-  ) => GProductBC c (Rec (Other b' (P0 X)) (b X))
-                    (Rec       (b' (P0 (Dict c)))
-                               (b      (Dict c))) where
+  ) => GProductBC c (Other (b' (P0 X)) (b X))
+                    (Rec (b' (P0 (Dict c))) (b (Dict c))) where
   gbdicts = Rec $ K1 $ bdicts @_ @b
 
 
diff --git a/test-legacy/Legacy/TestBarbies.hs b/test-legacy/Legacy/TestBarbies.hs
--- a/test-legacy/Legacy/TestBarbies.hs
+++ b/test-legacy/Legacy/TestBarbies.hs
@@ -28,6 +28,7 @@
 
 import Data.Barbie
 
+import Data.Kind(Type)
 import Data.Typeable
 import GHC.Generics
 import Test.Tasty.QuickCheck
@@ -36,7 +37,7 @@
 -- Product Barbies
 ----------------------------------------------------
 
-data Record0 (f :: * -> *)
+data Record0 (f :: Type -> Type)
   = Record0
   deriving
     ( Generic, Typeable
@@ -134,7 +135,7 @@
 -- Bad products
 -----------------------------------------------------
 
-data Ignore1 (f :: * -> *)
+data Ignore1 (f :: Type -> Type)
   = Ignore1 { ign1_f1 :: Int }
   deriving (Generic, Typeable, Eq, Show)
 
@@ -258,7 +259,7 @@
 -- Parametric barbies
 -----------------------------------------------------
 
-data ParB b (f :: * -> *)
+data ParB b (f :: Type -> Type)
   = ParB (b f)
   deriving (Generic, Typeable)
 
@@ -268,7 +269,7 @@
 instance ConstraintsB b => ConstraintsB (ParB b)
 instance ProductBC b => ProductBC (ParB b)
 
-data ParBH h b (f :: * -> *)
+data ParBH h b (f :: Type -> Type)
   = ParBH (h (b f))
   deriving (Generic, Typeable)
 
diff --git a/test-legacy/Legacy/TestBarbiesW.hs b/test-legacy/Legacy/TestBarbiesW.hs
--- a/test-legacy/Legacy/TestBarbiesW.hs
+++ b/test-legacy/Legacy/TestBarbiesW.hs
@@ -24,6 +24,7 @@
 import Data.Barbie
 import Data.Barbie.Bare
 
+import Data.Kind(Type)
 import Data.Typeable
 import GHC.Generics
 import Test.Tasty.QuickCheck
@@ -278,7 +279,7 @@
 -- Parametric barbies
 -----------------------------------------------------
 
-data ParBW b t (f :: * -> *)
+data ParBW b t (f :: Type -> Type)
   = ParBW (b t f)
   deriving (Generic, Typeable)
 
@@ -302,7 +303,7 @@
 instance ProductBC (b t) => ProductBC (ParBW b t) where
   bdicts = ParBW bdicts
 
-data ParBHW h b t (f :: * -> *)
+data ParBHW h b t (f :: Type -> Type)
   = ParBHW (h (b t f))
   deriving (Generic, Typeable)
 
diff --git a/test/Spec.hs b/test/Spec.hs
--- a/test/Spec.hs
+++ b/test/Spec.hs
@@ -70,6 +70,10 @@
             , Functor.laws @(Flip Bi.NestedF ())
             , Functor.laws @(Flip Bi.Nested2F ())
             , Functor.laws @(Flip Bi.NestedB Maybe)
+
+
+            , Functor.laws @(Bi.MixedBT Maybe)
+            , Functor.laws @(Flip Bi.MixedBT Maybe)
             ]
 
         , testGroup "Distributive Laws"
@@ -127,7 +131,6 @@
 
             , Traversable.laws @(ParF Maybe)
 
-
             , Traversable.laws @(Flip Bi.Record0 ())
             , Traversable.laws @(Flip Bi.Record1 ())
             , Traversable.laws @(Flip Bi.Record3 ())
@@ -140,6 +143,9 @@
             , Traversable.laws @(Flip Bi.NestedF ())
             , Traversable.laws @(Flip Bi.Nested2F ())
             , Traversable.laws @(Flip Bi.NestedB Maybe)
+
+            , Traversable.laws @(Bi.MixedBT Maybe)
+            , Traversable.laws @(Flip Bi.MixedBT Maybe)
             ]
 
         , testGroup "Applicative laws"
@@ -174,6 +180,8 @@
             , Applicative.laws @(Flip Bi.NestedF ())
             , Applicative.laws @(Flip Bi.Nested2F ())
             , Applicative.laws @(Flip (Bi.ParX (Maybe ())) ())
+
+            , Applicative.laws @(Bi.MixedBT [])
             ]
 
         , testGroup "addDict projection"
@@ -200,6 +208,8 @@
 
             , Constraints.lawAddDictPrj @CompositeRecord
             , Constraints.lawAddDictPrj @(CompositeRecordW Covered)
+
+            , Constraints.lawAddDictPrj @(Bi.MixedBT Maybe)
             ]
 
         , testGroup "Bare laws"
diff --git a/test/TestBarbies.hs b/test/TestBarbies.hs
--- a/test/TestBarbies.hs
+++ b/test/TestBarbies.hs
@@ -33,6 +33,7 @@
 import Data.Functor.Barbie
 import Data.Distributive
 
+import Data.Kind(Type)
 import Data.Typeable
 import GHC.Generics
 import Test.Tasty.QuickCheck
@@ -41,7 +42,7 @@
 -- Product Barbies
 ----------------------------------------------------
 
-data Record0 (f :: * -> *)
+data Record0 (f :: Type -> Type)
   = Record0
   deriving
     ( Generic, Typeable
@@ -140,7 +141,7 @@
 -- Bad products
 -----------------------------------------------------
 
-data Ignore1 (f :: * -> *)
+data Ignore1 (f :: Type -> Type)
   = Ignore1 { ign1_f1 :: Int }
   deriving (Generic, Typeable, Eq, Show)
 
@@ -282,7 +283,7 @@
 -- Parametric barbies
 -----------------------------------------------------
 
-data ParB b (f :: * -> *)
+data ParB b (f :: Type -> Type)
   = ParB (b f)
   deriving (Generic, Typeable)
 
@@ -292,7 +293,7 @@
 instance ApplicativeB b => ApplicativeB (ParB b)
 instance ConstraintsB b => ConstraintsB (ParB b)
 
-data ParBH h b (f :: * -> *)
+data ParBH h b (f :: Type -> Type)
   = ParBH (h (b f))
   deriving (Generic, Typeable)
 
diff --git a/test/TestBarbiesW.hs b/test/TestBarbiesW.hs
--- a/test/TestBarbiesW.hs
+++ b/test/TestBarbiesW.hs
@@ -25,6 +25,7 @@
 import Data.Functor.Barbie
 import Barbies.Bare
 
+import Data.Kind(Type)
 import Data.Typeable
 import GHC.Generics
 import Test.Tasty.QuickCheck
@@ -303,7 +304,7 @@
 -- Parametric barbies
 -----------------------------------------------------
 
-data ParBW b t (f :: * -> *)
+data ParBW b t (f :: Type -> Type)
   = ParBW (b t f)
   deriving (Generic, Typeable)
 
@@ -324,7 +325,7 @@
   baddDicts (ParBW btf) = ParBW (baddDicts btf)
 
 
-data ParBHW h b t (f :: * -> *)
+data ParBHW h b t (f :: Type -> Type)
   = ParBHW (h (b t f))
   deriving (Generic, Typeable)
 
diff --git a/test/TestBiBarbies.hs b/test/TestBiBarbies.hs
--- a/test/TestBiBarbies.hs
+++ b/test/TestBiBarbies.hs
@@ -28,6 +28,7 @@
   , HKB(..)
 
   , NestedB(..)
+  , MixedBT(..)
   )
 
 where
@@ -36,6 +37,7 @@
 import Data.Distributive
 import qualified TestBarbies
 
+import Data.Kind(Type)
 import Data.Typeable
 import GHC.Generics
 import Test.Tasty.QuickCheck
@@ -47,7 +49,7 @@
 -- Product Barbies
 ----------------------------------------------------
 
-data Record0 (f :: kl -> *) (x :: kr)
+data Record0 (f :: kl -> Type) (x :: kr)
   = Record0
   deriving
     ( Generic, Typeable
@@ -145,7 +147,7 @@
 -- Bad products
 -----------------------------------------------------
 
-data Ignore1 (f :: * -> *) (x :: kx)
+data Ignore1 (f :: Type -> Type) (x :: kx)
   = Ignore1 { ign1_f1 :: Int }
   deriving (Generic, Typeable, Eq, Show)
 
@@ -287,7 +289,7 @@
 -- Parametric barbies
 -----------------------------------------------------
 
-data ParB b (f :: k -> *) (x :: kx)
+data ParB b (f :: k -> Type) (x :: kx)
   = ParB (b f x)
   deriving (Generic, Typeable)
 
@@ -297,7 +299,7 @@
 instance TraversableT b => TraversableT (ParB b)
 instance ConstraintsT b => ConstraintsT (ParB b)
 
-data ParBH h b (f :: k -> *) (x :: kx)
+data ParBH h b (f :: k -> Type) (x :: kx)
   = ParBH (h (b f x))
   deriving (Generic, Typeable)
 
@@ -370,3 +372,25 @@
 instance (Arbitrary (f (g Bool)), AllBF Arbitrary g Record1', Arbitrary (f (Record1' g))) => Arbitrary (NestedB f g) where
   arbitrary
     = NestedB <$> arbitrary <*> arbitrary <*> arbitrary <*> arbitrary
+
+data MixedBT f g
+  = MixedBT
+    { mx_1 :: f Int
+    , mx_2 :: g Bool
+    }
+  deriving (Generic, Typeable)
+
+instance FunctorT MixedBT
+instance TraversableT MixedBT
+instance ConstraintsT MixedBT
+
+instance FunctorB (MixedBT f)
+instance (Monoid (f Int)) => ApplicativeB (MixedBT f)
+instance TraversableB (MixedBT f)
+instance ConstraintsB (MixedBT f)
+
+deriving instance (AllBF Show g (MixedBT f), AllTF Show f MixedBT) => Show (MixedBT f g)
+deriving instance (AllBF Eq g (MixedBT f), AllTF Eq f MixedBT) => Eq (MixedBT f g)
+
+instance (AllBF Arbitrary g (MixedBT f), AllTF Arbitrary f MixedBT) => Arbitrary (MixedBT f g) where
+  arbitrary = MixedBT <$> arbitrary <*> arbitrary