diff --git a/ChangeLog.md b/ChangeLog.md
--- a/ChangeLog.md
+++ b/ChangeLog.md
@@ -1,5 +1,11 @@
 # Changelog for polysemy-check
 
+## v0.4.0.0 (2021-10-12)
+
+- `GArbitraryK` now supports actions that contain existential types.
+- (Internal) Aggressively rewrote the `GArbitraryK` typeclass to make better use
+    of `kind-generics`.
+
 ## v0.3.0.0 (2021-10-09)
 
 - `prepropLaw` now synthesizes a monadic prelude and postlude to your laws, to
diff --git a/polysemy-check.cabal b/polysemy-check.cabal
--- a/polysemy-check.cabal
+++ b/polysemy-check.cabal
@@ -5,7 +5,7 @@
 -- see: https://github.com/sol/hpack
 
 name:           polysemy-check
-version:        0.3.0.0
+version:        0.4.0.0
 synopsis:       QuickCheck for Polysemy
 description:    Please see the README on GitHub at <https://github.com/polysemy-research/polysemy-check#readme>
 category:       Polysemy
@@ -27,6 +27,7 @@
 
 library
   exposed-modules:
+      Generics.Kind.Unexported
       Polysemy.Check
       Polysemy.Check.Arbitrary
       Polysemy.Check.Arbitrary.AnyEff
@@ -60,7 +61,7 @@
       QuickCheck
     , base >=4.7 && <5
     , containers
-    , kind-generics
+    , kind-generics <=0.4.1.0
     , kind-generics-th
     , polysemy
   default-language: Haskell2010
@@ -72,6 +73,7 @@
       CommutativeSpec
       EquivSpec
       LawSpec
+      WeirdEffectsSpec
       Paths_polysemy_check
   hs-source-dirs:
       test
@@ -101,7 +103,7 @@
     , base >=4.7 && <5
     , containers
     , hspec
-    , kind-generics
+    , kind-generics <=0.4.1.0
     , kind-generics-th
     , polysemy
     , polysemy-check
diff --git a/src/Generics/Kind/Unexported.hs b/src/Generics/Kind/Unexported.hs
new file mode 100644
--- /dev/null
+++ b/src/Generics/Kind/Unexported.hs
@@ -0,0 +1,51 @@
+module Generics.Kind.Unexported where
+
+import Generics.Kind hiding (SubstRep)
+
+
+class SubstRep' (f :: LoT (t -> k) -> *) (x :: t) (xs :: LoT k) where
+  type family SubstRep f x :: LoT k -> *
+  substRep   :: f (x ':&&: xs) -> SubstRep f x xs
+  unsubstRep :: SubstRep f x xs -> f (x ':&&: xs)
+
+instance SubstRep' U1 x xs where
+  type SubstRep U1 x = U1
+  substRep   U1 = U1
+  unsubstRep U1 = U1
+
+instance (SubstRep' f x xs, SubstRep' g x xs) => SubstRep' (f :+: g) x xs where
+  type SubstRep (f :+: g)  x = (SubstRep f x) :+: (SubstRep g x)
+  substRep   (L1 x) = L1 (substRep   x)
+  substRep   (R1 x) = R1 (substRep   x)
+  unsubstRep (L1 x) = L1 (unsubstRep x)
+  unsubstRep (R1 x) = R1 (unsubstRep x)
+
+instance (SubstRep' f x xs, SubstRep' g x xs) => SubstRep' (f :*: g) x xs where
+  type SubstRep (f :*: g) x = (SubstRep f x) :*: (SubstRep g x)
+  substRep   (x :*: y) = substRep   x :*: substRep   y
+  unsubstRep (x :*: y) = unsubstRep x :*: unsubstRep y
+
+instance SubstRep' f x xs => SubstRep' (M1 i c f) x xs where
+  type SubstRep (M1 i c f) x = M1 i c (SubstRep f x)
+  substRep   (M1 x) = M1 (substRep   x)
+  unsubstRep (M1 x) = M1 (unsubstRep x)
+
+instance (Interpret (SubstAtom c x) xs, Interpret c (x ':&&: xs), SubstRep' f x xs)
+         => SubstRep' (c :=>: f) x xs where
+  type SubstRep (c :=>: f) x = (SubstAtom c x) :=>: (SubstRep f x)
+  substRep   (SuchThat x) = SuchThat (substRep   x)
+  unsubstRep (SuchThat x) = SuchThat (unsubstRep x)
+
+instance (Interpret (SubstAtom t x) xs ~ Interpret t (x ':&&: xs))
+         => SubstRep' (Field t) x xs where
+  type SubstRep (Field t) x = Field (SubstAtom t x)
+  substRep   (Field x) = Field x
+  unsubstRep (Field x) = Field x
+
+type family SubstAtom (f :: Atom (t -> k) d) (x :: t) :: Atom k d where
+  SubstAtom ('Var 'VZ)     x = 'Kon x
+  SubstAtom ('Var ('VS v)) x = 'Var v
+  SubstAtom ('Kon t)       x = 'Kon t
+  SubstAtom (t1 ':@: t2)   x = (SubstAtom t1 x) ':@: (SubstAtom t2 x)
+  SubstAtom (t1 ':&: t2)   x = (SubstAtom t1 x) ':&: (SubstAtom t2 x)
+
diff --git a/src/Polysemy/Check.hs b/src/Polysemy/Check.hs
--- a/src/Polysemy/Check.hs
+++ b/src/Polysemy/Check.hs
@@ -16,6 +16,9 @@
   , SomeEff (..)
   , SomeEffOfType (..)
 
+    -- * Support for Existential Types
+  , ExistentialFor
+
     -- * Constraints for Generators of Effects
   , GArbitraryK
   , ArbitraryAction
@@ -36,7 +39,7 @@
 import Polysemy
 import Polysemy.Check.Arbitrary
 import Polysemy.Check.Arbitrary.AnyEff
-import Polysemy.Check.Arbitrary.Generic (GArbitraryK)
+import Polysemy.Check.Arbitrary.Generic (GArbitraryK, ExistentialFor)
 import Polysemy.Check.Orphans ()
 import Polysemy.Internal
 import Polysemy.Internal.Union.Inject (Inject, inject)
diff --git a/src/Polysemy/Check/Arbitrary.hs b/src/Polysemy/Check/Arbitrary.hs
--- a/src/Polysemy/Check/Arbitrary.hs
+++ b/src/Polysemy/Check/Arbitrary.hs
@@ -21,10 +21,10 @@
 -- | Generate any action for effect @e@ that produces type @a@.
 arbitraryActionOfType
     :: forall e a r
-     . (GenericK (e (Sem r) a), GArbitraryK a (RepK (e (Sem r) a)))
+     . (GenericK e, GArbitraryK e (RepK e) r a)
     => Gen (e (Sem r) a)
        -- ^
-arbitraryActionOfType = genEff @e @a @(Sem r)
+arbitraryActionOfType = genEff @e @r @a
 
 
 ------------------------------------------------------------------------------
diff --git a/src/Polysemy/Check/Arbitrary/AnyEff.hs b/src/Polysemy/Check/Arbitrary/AnyEff.hs
--- a/src/Polysemy/Check/Arbitrary/AnyEff.hs
+++ b/src/Polysemy/Check/Arbitrary/AnyEff.hs
@@ -39,9 +39,10 @@
 ------------------------------------------------------------------------------
 -- | A type family that expands to a 'GArbitraryK' constaint for every type in
 -- the first list.
-type family ArbitraryForAll (as :: [Type]) (m :: Type -> Type) :: Constraint where
-  ArbitraryForAll '[] f = ()
-  ArbitraryForAll (a ': as) f = (Eq a, Show a, GArbitraryK a (RepK (f a)), ArbitraryForAll as f)
+type family ArbitraryForAll (e :: Effect) (as :: [Type]) (r :: EffectRow) :: Constraint where
+  ArbitraryForAll e '[] f = ()
+  ArbitraryForAll e (a ': as) r =
+    (Eq a, Show a, GArbitraryK e (RepK e) r a, ArbitraryForAll e as r)
 
 
 ------------------------------------------------------------------------------
@@ -112,15 +113,15 @@
     , Show a
     , Show (e (Sem r) a)
     , ArbitraryEffOfType a es r
-    , GenericK (e (Sem r) a)
-    , GArbitraryK a (RepK (e (Sem r) a))
+    , GenericK e
+    , GArbitraryK e (RepK e) r a
     , CoArbitrary a
     , Member e r
     )
     => ArbitraryEffOfType a (e ': es) r
     where
   genSomeEffOfType
-    = fmap SomeEffOfType (genEff @e @a @(Sem r))
+    = fmap SomeEffOfType (genEff @e @r @a)
     : genSomeEffOfType @a @es @r
 
 
@@ -139,11 +140,11 @@
     , Show a
     , Member e r
     , Show (e (Sem r) a)
-    , GenericK (e (Sem r) a)
+    , GenericK e
     , CoArbitrary a
-    , GArbitraryK a (RepK (e (Sem r) a))
+    , GArbitraryK e (RepK e) r a
     )
     => ArbitraryAction (a : as) e r
     where
-  genSomeAction = (fmap SomeAction $ genEff @e @a @(Sem r)) : genSomeAction @as @e @r
+  genSomeAction = (fmap SomeAction $ genEff @e @r @a) : genSomeAction @as @e @r
 
diff --git a/src/Polysemy/Check/Arbitrary/Generic.hs b/src/Polysemy/Check/Arbitrary/Generic.hs
--- a/src/Polysemy/Check/Arbitrary/Generic.hs
+++ b/src/Polysemy/Check/Arbitrary/Generic.hs
@@ -3,77 +3,87 @@
 import Control.Applicative (liftA2)
 import Data.Kind (Type)
 import GHC.Exts (type (~~))
-import Generics.Kind
-import Test.QuickCheck
+import Generics.Kind hiding (SubstRep)
+import Generics.Kind.Unexported
 import Polysemy
 import Polysemy.Check.Arbitrary.AnyEff
 import Polysemy.Internal (send)
+import Test.QuickCheck
 
 
 ------------------------------------------------------------------------------
-
-type a :~~~: b = 'Kon (~~) ':@: a ':@: b
+-- | Data family for the instantiation of existential variables. If you want to
+-- check properties for an effect @e@ that contains an existential type, the
+-- synthesized 'Arbitrary' instance will instantiate all of @e@'s existential
+-- types at @'ExistentialFor' e@.
+--
+-- @'ExistentialFor' e@ must have instances for every dictionary required by
+-- @e@, and will likely require an 'Arbitrary' instance.
+data family ExistentialFor (e :: Effect)
 
 
 ------------------------------------------------------------------------------
--- | Given @'GArbitraryK' a ('RepK' (e m a))@, this typeclass computes
--- generators for every well-typed constructor of @e m a@. It is capable of
--- building generators for GADTs.
-class GArbitraryK (a :: Type) (f :: LoT Type -> Type) where
-  garbitraryk :: [Gen (f x)]
+-- | Given @'GArbitraryK' a ('RepK' e) r a@, this typeclass computes
+-- generators for every well-typed constructor of @e (Sem r) a@. It is capable
+-- of building generators for GADTs.
+class GArbitraryK (e :: Effect) (f :: LoT Effect -> Type) (r :: EffectRow) (a :: Type)  where
+  garbitraryk :: [Gen (f (LoT2 (Sem r) a))]
 
-instance GArbitraryK a U1 where
+instance GArbitraryK e U1 r a where
   garbitraryk = pure $ pure U1
 
-instance (GArbitraryK1 (f :*: g)) => GArbitraryK a (f :*: g) where
-  garbitraryk = garbitraryk1
+instance (GArbitraryK e f r a, GArbitraryK e g r a) => GArbitraryK e (f :*: g) r a where
+  garbitraryk = liftA2 (liftA2 (:*:)) (garbitraryk @e) (garbitraryk @e)
 
-instance (GArbitraryK1 (Field b)) => GArbitraryK a (Field b) where
-  garbitraryk = garbitraryk1
+instance GArbitraryKTerm (Interpret f (LoT2 (Sem r) a)) => GArbitraryK e (Field f) r a where
+  garbitraryk = pure $ fmap Field $ garbitrarykterm @(Interpret f (LoT2 (Sem r) a))
 
-instance (GArbitraryK a f, GArbitraryK a g) => GArbitraryK a (f :+: g) where
-  garbitraryk = fmap (fmap L1) (garbitraryk @a @f)
-             <> fmap (fmap R1) (garbitraryk @a @g)
+instance
+    ( GArbitraryK e (SubstRep f (ExistentialFor e)) r a
+    , SubstRep' f (ExistentialFor e) (LoT2 (Sem r) a)
+    ) => GArbitraryK e (Exists Type f) r a where
+  garbitraryk = fmap (Exists . unsubstRep @_ @_ @_ @(ExistentialFor e)) <$>
+    garbitraryk @e @(SubstRep f (ExistentialFor e)) @r @a
 
-instance GArbitraryK1 f => GArbitraryK a ('Kon (a ~~ a) :=>: f) where
-  garbitraryk = fmap SuchThat <$> garbitraryk1
+instance (GArbitraryK e f r a, GArbitraryK e g r a) => GArbitraryK e (f :+: g) r a where
+  garbitraryk = fmap (fmap L1) (garbitraryk @e @f)
+             <> fmap (fmap R1) (garbitraryk @e @g)
 
-instance {-# INCOHERENT #-} GArbitraryK a ('Kon (a ~~ b) :=>: f) where
-  garbitraryk = []
+instance (Interpret c (LoT2 (Sem r) a), GArbitraryK e f r a) => GArbitraryK e (c :=>: f) r a where
+  garbitraryk = fmap (fmap SuchThat) (garbitraryk @e @f)
 
-instance {-# INCOHERENT #-} GArbitraryK a ('Kon (b ~~ c) :=>: f) where
-  garbitraryk = []
+instance {-# OVERLAPPING #-} GArbitraryK e (c1 :=>: (c2 :=>: f)) r a
+    => GArbitraryK e ((c1 ':&: c2) :=>: f) r a where
+  garbitraryk =
+    fmap
+      ((\(SuchThat (SuchThat x)) -> SuchThat x)
+            :: (c1 :=>: (c2 :=>: f)) x -> ((c1 ':&: c2) :=>: f) x)
+        <$> garbitraryk @e
 
-instance (GArbitraryK a f) => GArbitraryK a (M1 _1 _2 f) where
-  garbitraryk = fmap M1 <$> garbitraryk @a
+instance {-# OVERLAPPING #-} GArbitraryK e f r a => GArbitraryK e ('Kon ((~~) a) ':@: Var1 :=>: f) r a where
+  garbitraryk = fmap SuchThat <$> garbitraryk @e @f
 
+instance {-# OVERLAPPING #-} GArbitraryK e f r a => GArbitraryK e ('Kon (~~) ':@: Var1 ':@: 'Kon a :=>: f) r a where
+  garbitraryk = fmap SuchThat <$> garbitraryk @e @f
 
-------------------------------------------------------------------------------
--- | @genEff \@e \@a \@m@ gets a generator capable of producing every
--- well-typed GADT constructor of @e m a@.
-genEff :: forall e a m. (GArbitraryK a (RepK (e m a)), GenericK (e m a)) => Gen (e m a)
-genEff = fmap toK $ oneof $ garbitraryk @a @(RepK (e m a))
+instance {-# INCOHERENT #-} GArbitraryK e ('Kon ((~~) b) ':@: Var1 :=>: f) r a where
+  garbitraryk = []
 
+instance {-# INCOHERENT #-} GArbitraryK e ('Kon (~~) ':@: Var1 ':@: 'Kon b :=>: f) r a where
+  garbitraryk = []
 
-------------------------------------------------------------------------------
--- | Like @GArbitraryK@, but gets run after we've already discharged the @a
--- ~ T@ GADT constraint.
-class GArbitraryK1 (f :: LoT Type -> Type) where
-  garbitraryk1 :: [Gen (f x)]
+instance (GArbitraryK e f r a) => GArbitraryK e (M1 _1 _2 f) r a where
+  garbitraryk = fmap M1 <$> garbitraryk @e
 
-instance (GArbitraryK1 f, GArbitraryK1 g) => GArbitraryK1 (f :*: g) where
-  garbitraryk1 = liftA2 (liftA2 (:*:)) garbitraryk1 garbitraryk1
 
-instance GArbitraryKTerm t => GArbitraryK1 (Field ('Kon t)) where
-  garbitraryk1 = pure $ fmap Field garbitrarykterm
+------------------------------------------------------------------------------
+-- | @genEff \@e \@r \@a@ gets a generator capable of producing every
+-- well-typed GADT constructor of @e (Sem r) a@.
+genEff :: forall e r a. (GenericK e, GArbitraryK e (RepK e) r a) => Gen (e (Sem r) a)
+genEff = fmap toK $ oneof $ garbitraryk @e @(RepK e) @r
 
-instance (GArbitraryK1 f) => GArbitraryK1 (M1 _1 _2 f) where
-  garbitraryk1 = fmap M1 <$> garbitraryk1
 
-instance GArbitraryK1 U1 where
-  garbitraryk1 = pure $ pure U1
 
-
 class GArbitraryKTerm (t :: Type) where
   garbitrarykterm :: Gen t
 
@@ -87,5 +97,4 @@
 
 instance Arbitrary a => GArbitraryKTerm a where
   garbitrarykterm = arbitrary
-
 
diff --git a/src/Polysemy/Check/Arbitrary/Generic.hs-boot b/src/Polysemy/Check/Arbitrary/Generic.hs-boot
--- a/src/Polysemy/Check/Arbitrary/Generic.hs-boot
+++ b/src/Polysemy/Check/Arbitrary/Generic.hs-boot
@@ -3,17 +3,18 @@
 import Data.Kind (Type)
 import Generics.Kind
 import Test.QuickCheck
+import Polysemy
 
 
 ------------------------------------------------------------------------------
 -- | Given @'GArbitraryK' a ('RepK' (e m a))@, this typeclass computes
 -- generators for every well-typed constructor of @e m a@. It is capable of
 -- building generators for GADTs.
-class GArbitraryK (a :: Type) (f :: LoT Type -> Type) where
-  garbitraryk :: [Gen (f x)]
+class GArbitraryK (e :: Effect) (f :: LoT Effect -> Type) (r :: EffectRow) (a :: Type)  where
+  garbitraryk :: [Gen (f (LoT2 (Sem r) a))]
 
 ------------------------------------------------------------------------------
 -- | @genEff \@e \@a \@m@ gets a generator capable of producing every
 -- well-typed GADT constructor of @e m a@.
-genEff :: forall e a m. (GArbitraryK a (RepK (e m a)), GenericK (e m a)) => Gen (e m a)
+genEff :: forall e r a. (GenericK e, GArbitraryK e (RepK e) r a) => Gen (e (Sem r) a)
 
diff --git a/test/LawSpec.hs b/test/LawSpec.hs
--- a/test/LawSpec.hs
+++ b/test/LawSpec.hs
@@ -36,17 +36,25 @@
       pure $ putGetLaw $ runIOState s
 
 
-putPutLaw
-    :: forall s r
-     . ( Arbitrary s
-       , Member (State s) r
+type LawConstraints f effs s r =
+       ( Arbitrary s
+       , Members effs r
        , Eq s
        , Show s
-       , ArbitraryEff '[State s] r
+       , ArbitraryEff effs r
+       , f ~ (,) s
+       , effs ~ '[State s]
        )
-    => (forall a. Sem r ((), a) -> IO (s, ((), a)))
+
+
+putPutLaw
+    :: forall s r res effs f
+     . ( res ~ ()
+       , LawConstraints f effs s r
+       )
+    => (forall a. Sem r (res, a) -> IO (f (res, a)))
     -> Property
-putPutLaw = prepropLaw @'[State s] $ do
+putPutLaw = prepropLaw @effs $ do
   s1 <- arbitrary
   s2 <- arbitrary
   pure
@@ -59,16 +67,13 @@
 
 
 getPutLaw
-    :: forall s r
-     . ( Arbitrary s
-       , Member (State s) r
-       , Eq s
-       , Show s
-       , ArbitraryEff '[State s] r
+    :: forall s r res effs f
+     . ( res ~ ()
+       , LawConstraints f effs s r
        )
-    => (forall a. Sem r ((), a) -> IO (s, ((), a)))
+    => (forall a. Sem r (res, a) -> IO (f (res, a)))
     -> Property
-getPutLaw = prepropLaw @'[State s] $ do
+getPutLaw = prepropLaw @effs $ do
   pure
     ( get >>= put
     , pure ()
@@ -76,16 +81,13 @@
 
 
 putGetLaw
-    :: forall s r
-     . ( Arbitrary s
-       , Member (State s) r
-       , Eq s
-       , Show s
-       , ArbitraryEff '[State s] r
+    :: forall s r res effs f
+     . ( res ~ s
+       , LawConstraints f effs s r
        )
-    => (forall a. Sem r (s, a) -> IO (s, (s, a)))
+    => (forall a. Sem r (res, a) -> IO (f (res, a)))
     -> Property
-putGetLaw = prepropLaw @'[State s] $ do
+putGetLaw = prepropLaw @effs $ do
   s <- arbitrary
   pure
     ( do
diff --git a/test/WeirdEffectsSpec.hs b/test/WeirdEffectsSpec.hs
new file mode 100644
--- /dev/null
+++ b/test/WeirdEffectsSpec.hs
@@ -0,0 +1,41 @@
+module WeirdEffectsSpec where
+
+import Data.Typeable
+import Polysemy
+import Polysemy.Check
+import Test.Hspec
+import Test.Hspec.QuickCheck
+import Test.QuickCheck
+
+
+data MyEffect m a where
+  -- | Here, @e@ is existential!
+  CanShow :: (Show e, Typeable e) => e -> MyEffect m ()
+
+makeSem ''MyEffect
+
+deriving instance Show (MyEffect m a)
+deriveGenericK ''MyEffect
+
+
+------------------------------------------------------------------------------
+-- | When we synthesize a @MyEffect@ action, we instantiate all existentials at
+-- @'ExistentialFor' MyEffect@.
+--
+-- This type must satisfy all of the constraints required by @CanShow@.
+data instance ExistentialFor MyEffect = Hello
+  deriving (Eq, Show)
+
+-- It also requires an 'Arbitrary' instance!
+instance Arbitrary (ExistentialFor MyEffect) where
+  arbitrary = pure Hello
+
+
+spec :: Spec
+spec = do
+  prop @(Gen Expectation) "Existentials get instantiated at 'ExistentialFor MyEffect'" $ do
+    SomeAction e <- arbitraryAction @MyEffect @'[MyEffect]
+    pure $ case e of
+      CanShow t ->
+        cast t `shouldBe` Just Hello
+