diff --git a/ChangeLog.md b/ChangeLog.md
new file mode 100644
--- /dev/null
+++ b/ChangeLog.md
@@ -0,0 +1,8 @@
+# Changelog for polysemy-check
+
+## v0.1.0.0 (2021-10-08)
+
+- Released!
+
+## Unreleased changes
+
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright Sandy Maguire (c) 2021
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * Redistributions in binary form must reproduce the above
+      copyright notice, this list of conditions and the following
+      disclaimer in the documentation and/or other materials provided
+      with the distribution.
+
+    * Neither the name of Sandy Maguire nor the names of other
+      contributors may be used to endorse or promote products derived
+      from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,52 @@
+# polysemy-check
+
+[![Hackage](https://img.shields.io/hackage/v/polysemy-check.svg?logo=haskell&label=polysemy-check)](https://hackage.haskell.org/package/polysemy-check)
+
+## Dedication
+
+> Success is most often achieved by those who don't know that failure is
+> inevitable.
+>
+> --Coco Chanel
+
+## Overview
+
+`polysemy-check` is a little package that integrates
+[`polysemy`](https://hackage.haskell.org/package/polysemy) with
+[`QuickCheck`](https://hackage.haskell.org/package/QuickCheck). It allows you to
+prove the equivalence of effects (see `prepropLaw`), the equivalence of
+interpreters (`prepropEquivalent`), and that two effects don't affect one
+another (`prepropCommutative`). These three things are about the only problems
+you could possibly run into with Polysemy --- and now you won't.
+
+In addition `polysemy-check` provides lots of machinery to help avoid
+boilerplate, such as free `Arbitrary` instances for effects.
+
+
+## Usage
+
+`polysemy-check` requires a `Show` and `GenericK` instance for every effect
+you'd like to run tests over.
+
+```haskell
+{-# LANGUAGE TemplateHaskell #-}
+
+import Polysemy
+import Polysemy.Check
+
+data Stack m a where
+  Push :: Int -> Stack m ()
+  Pop  :: Stack m (Maybe Int)
+  Size :: Stack m Int
+
+deriving instance Show (Stack m a)
+makeSem ''Stack
+deriveGenericK ''Stack
+```
+
+
+## Examples
+
+Check the [test
+suite](https://github.com/polysemy-research/polysemy-check/tree/master/test).
+
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/polysemy-check.cabal b/polysemy-check.cabal
new file mode 100644
--- /dev/null
+++ b/polysemy-check.cabal
@@ -0,0 +1,109 @@
+cabal-version: 1.12
+
+-- This file has been generated from package.yaml by hpack version 0.34.4.
+--
+-- see: https://github.com/sol/hpack
+
+name:           polysemy-check
+version:        0.1.0.0
+synopsis:       QuickCheck for Polysemy
+description:    Please see the README on GitHub at <https://github.com/polysemy-research/polysemy-check#readme>
+category:       Polysemy
+homepage:       https://github.com/polysemy-research/polysemy-check#readme
+bug-reports:    https://github.com/polysemy-research/polysemy-check/issues
+author:         Sandy Maguire
+maintainer:     sandy@sandymaguire.me
+copyright:      Sandy Maguire
+license:        BSD3
+license-file:   LICENSE
+build-type:     Simple
+extra-source-files:
+    README.md
+    ChangeLog.md
+
+source-repository head
+  type: git
+  location: https://github.com/polysemy-research/polysemy-check
+
+library
+  exposed-modules:
+      Polysemy.Check
+      Polysemy.Check.Arbitrary
+      Polysemy.Check.Arbitrary.AnyEff
+      Polysemy.Check.Arbitrary.Generic
+      Polysemy.Check.Orphans
+      Polysemy.Internal.Union.Inject
+  other-modules:
+      Paths_polysemy_check
+  hs-source-dirs:
+      src
+  default-extensions:
+      AllowAmbiguousTypes
+      ConstraintKinds
+      DataKinds
+      FlexibleContexts
+      FlexibleInstances
+      GADTs
+      LambdaCase
+      MultiParamTypeClasses
+      PolyKinds
+      RankNTypes
+      ScopedTypeVariables
+      StandaloneDeriving
+      TemplateHaskell
+      TypeApplications
+      TypeFamilies
+      TypeOperators
+      UndecidableInstances
+  ghc-options: -Wall
+  build-depends:
+      QuickCheck
+    , base >=4.7 && <5
+    , containers
+    , kind-generics
+    , kind-generics-th
+    , polysemy
+  default-language: Haskell2010
+
+test-suite test
+  type: exitcode-stdio-1.0
+  main-is: Main.hs
+  other-modules:
+      CommutativeSpec
+      EquivSpec
+      LawSpec
+      Paths_polysemy_check
+  hs-source-dirs:
+      test
+  default-extensions:
+      AllowAmbiguousTypes
+      ConstraintKinds
+      DataKinds
+      FlexibleContexts
+      FlexibleInstances
+      GADTs
+      LambdaCase
+      MultiParamTypeClasses
+      PolyKinds
+      RankNTypes
+      ScopedTypeVariables
+      StandaloneDeriving
+      TemplateHaskell
+      TypeApplications
+      TypeFamilies
+      TypeOperators
+      UndecidableInstances
+  ghc-options: -Wall -threaded -rtsopts -with-rtsopts=-N
+  build-tool-depends:
+      hspec-discover:hspec-discover >=2.0
+  build-depends:
+      QuickCheck
+    , base >=4.7 && <5
+    , containers
+    , hspec
+    , kind-generics
+    , kind-generics-th
+    , polysemy
+    , polysemy-check
+    , polysemy-plugin
+  default-language: Haskell2010
diff --git a/src/Polysemy/Check.hs b/src/Polysemy/Check.hs
new file mode 100644
--- /dev/null
+++ b/src/Polysemy/Check.hs
@@ -0,0 +1,157 @@
+{-# LANGUAGE QuantifiedConstraints #-}
+module Polysemy.Check
+  ( -- * Effect Properties
+    prepropCommutative
+  , prepropEquivalent
+  , prepropLaw
+
+    -- * Generators for Effects
+  , arbitraryAction
+  , arbitraryActionOfType
+  , arbitraryActionFromRow
+  , arbitraryActionFromRowOfType
+
+    -- * Types for Generators for Effects
+  , SomeAction (..)
+  , SomeEff (..)
+  , SomeEffOfType (..)
+
+    -- * Constraints for Generators of Effects
+  , GArbitraryK
+  , ArbitraryAction
+  , ArbitraryEff
+  , ArbitraryEffOfType
+  , TypesOf
+
+    -- * Re-exports
+  , send
+  , deriveGenericK
+  , GenericK
+  ) where
+
+import Generics.Kind (GenericK)
+import Generics.Kind.TH (deriveGenericK)
+import Polysemy
+import Polysemy.Check.Arbitrary
+import Polysemy.Check.Arbitrary.AnyEff
+import Polysemy.Check.Arbitrary.Generic (GArbitraryK)
+import Polysemy.Check.Orphans ()
+import Polysemy.Internal
+import Polysemy.Internal.Union.Inject (Inject, inject)
+import Test.QuickCheck
+
+
+------------------------------------------------------------------------------
+-- | Prove that two effects are commutative (a la
+-- <https://dl.acm.org/doi/10.1145/3473578 Reasoning about effect interaction by fusion>)
+-- under the given interpreter.
+--
+-- Humans naturally expect that disparate effects do not interact, thus
+-- commutativity is an important property for reasoning about the correctness
+-- of your program.
+--
+-- For example,
+--
+-- @
+-- 'prepropCommutative' \@(State Int) \@Trace \@EffStack runEffStack
+-- @
+--
+-- will interleave random @State Int@ and @Trace@ actions, within a bigger
+-- context of @EffStack@ actions. The resulting 'Property' will fail if
+-- permuting the @State Int@ and @Trace@ effects changes the outcome of the
+-- entire computation.
+prepropCommutative
+    :: forall e1 e2 r f
+     . ( forall a. Show a => Show (f a)
+       , forall a. Eq a => Eq (f a)
+       )
+    => ( ArbitraryEff r r
+       , ArbitraryEff '[e1] r
+       , ArbitraryEff '[e2] r
+       )
+    => (forall a. Sem r a -> IO (f a))
+       -- ^ An interpreter for the effect stack down to 'IO'. Pure effect
+       -- stacks can be lifted into 'IO' via 'pure' after the final 'run'.
+    -> Property
+prepropCommutative lower = property @(Gen Property) $ do
+  SomeEff m1 <- arbitraryActionFromRow @r @r
+  SomeEff e1 <- arbitraryActionFromRow @'[e1] @r
+  SomeEff e2 <- arbitraryActionFromRow @'[e2] @r
+  SomeEff m2 <- arbitraryActionFromRow @r @r
+  pure $
+    counterexample "Effects are not commutative!" $
+    counterexample "" $
+    counterexample ("k1  = " <> show m1) $
+    counterexample ("e1 = " <> show e1) $
+    counterexample ("e2 = " <> show e2) $
+    counterexample ("k2  = " <> show m2) $
+    counterexample "" $
+    counterexample "(e1 >> e2 >> k) /= (e2 >> e1 >> k)" $
+      ioProperty $ do
+        r1 <- lower $ send m1 >> send e1 >> send e2 >> send m2
+        r2 <- lower $ send m1 >> send e2 >> send e1 >> send m2
+        pure $ r1 === r2
+
+
+------------------------------------------------------------------------------
+-- | Prove that two programs in @r@ are equivalent under a given
+-- interpretation. This is useful for proving laws about particular effects (or
+-- stacks of effects).
+--
+-- For example, any lawful interpretation of @State@ must satisfy the @put s1
+-- >> put s2 = put s2@ law.
+prepropLaw
+    :: (Eq x, Show x)
+    => Gen (Sem r a, Sem r a)
+       -- ^ A generator for two equivalent programs.
+    -> (Sem r a -> IO x)
+       -- ^ An interpreter for the effect stack down to 'IO'. Pure effect
+       -- stacks can be lifted into 'IO' via 'pure' after the final 'run'.
+    -> Property
+prepropLaw g lower = property $ do
+  (m1, m2) <- g
+  pure $ ioProperty $ do
+    a1 <- lower m1
+    a2 <- lower m2
+    pure $ a1 === a2
+
+
+------------------------------------------------------------------------------
+-- | Prove that two interpreters are equivalent. For the given generator, this
+-- property ensures that the two interpreters give the same result for every
+-- arbitrary program.
+prepropEquivalent
+    :: forall effs x r1 r2
+     . (Eq x, Show x, Inject effs r1, Inject effs r2, Members effs effs)
+    => (forall a. Sem r1 a -> IO a)
+       -- ^ The first interpreter for the effect stack.Pure effect stacks can
+       -- be lifted into 'IO' via 'pure' after the final 'run'.
+    -> (forall a. Sem r2 a -> IO a)
+       -- ^ The second interpreter to prove equivalence for.
+    -> (forall r. Members effs r => Gen (Sem r x))
+       -- ^ A generator producing arbitrary programs in @r@. The property will
+       -- hold true if both interpreters produce the same output for every
+       -- program generated by this.
+    -> Property
+prepropEquivalent int1 int2 mksem = property $ do
+  SomeSem sem <- liftGen @effs @x mksem
+  pure $ ioProperty $ do
+    a1 <- int1 sem
+    a2 <- int2 sem
+    pure $ a1 === a2
+
+
+newtype SomeSem effs a = SomeSem
+  { _getSomeSem :: forall r. (Inject effs r) => Sem r a
+  }
+
+
+liftGen
+    :: forall effs a
+     . Members effs effs
+    => (forall r. Members effs r => Gen (Sem r a))
+    -> Gen (SomeSem effs a)
+liftGen g = do
+  a <- g @effs
+  pure $ SomeSem $ inject a
+
diff --git a/src/Polysemy/Check/Arbitrary.hs b/src/Polysemy/Check/Arbitrary.hs
new file mode 100644
--- /dev/null
+++ b/src/Polysemy/Check/Arbitrary.hs
@@ -0,0 +1,48 @@
+module Polysemy.Check.Arbitrary where
+
+import Generics.Kind
+import Polysemy
+import Polysemy.Check.Arbitrary.AnyEff
+import Polysemy.Check.Arbitrary.Generic
+import Test.QuickCheck
+
+
+------------------------------------------------------------------------------
+-- | Generate any action for effect @e@.
+arbitraryAction
+    :: forall e r
+     . ArbitraryAction (TypesOf e) e r
+    => Gen (SomeAction e r)
+       -- ^
+arbitraryAction = oneof $ genSomeAction @(TypesOf e) @e @r
+
+
+------------------------------------------------------------------------------
+-- | 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)))
+    => Gen (e (Sem r) a)
+       -- ^
+arbitraryActionOfType = genEff @e @a @(Sem r)
+
+
+------------------------------------------------------------------------------
+-- | Generate any action from any effect in @effs@.
+arbitraryActionFromRow
+    :: forall (effs :: EffectRow) r
+     . ArbitraryEff effs r
+    => Gen (SomeEff r)
+       -- ^
+arbitraryActionFromRow = oneof $ genSomeEff @effs @r
+
+
+------------------------------------------------------------------------------
+-- | Generate any action from any effect in @effs@ that produces type @a@.
+arbitraryActionFromRowOfType
+    :: forall (effs :: EffectRow) r a
+     . ArbitraryEffOfType a effs r
+    => Gen (SomeEffOfType r a)
+       -- ^
+arbitraryActionFromRowOfType = oneof $ genSomeEffOfType @a @effs @r
+
diff --git a/src/Polysemy/Check/Arbitrary/AnyEff.hs b/src/Polysemy/Check/Arbitrary/AnyEff.hs
new file mode 100644
--- /dev/null
+++ b/src/Polysemy/Check/Arbitrary/AnyEff.hs
@@ -0,0 +1,149 @@
+module Polysemy.Check.Arbitrary.AnyEff where
+
+import Data.Kind (Type, Constraint)
+import GHC.Exts (type (~~))
+import Generics.Kind
+import Polysemy
+import Polysemy.Internal
+import {-# SOURCE #-} Polysemy.Check.Arbitrary.Generic
+import Test.QuickCheck
+
+
+------------------------------------------------------------------------------
+-- | Helper function for implementing 'GTypesOf'
+type family GTypesOf (f :: LoT Effect -> Type) :: [Type] where
+  GTypesOf (M1 _1 _2 f) = GTypesOf f
+  GTypesOf (f :+: g) = Append (GTypesOf f) (GTypesOf g)
+  GTypesOf (('Kon (~~) ':@: Var1 ':@: 'Kon a) :=>: f) = '[a]
+  GTypesOf (('Kon ((~~) a) ':@: Var1) :=>: f) = '[a]
+  -- Otherwise, we don't have any constraints on @a@, so we can instantiate it
+  -- how we please. Just assume ().
+  GTypesOf _1 = '[()]
+
+
+------------------------------------------------------------------------------
+-- | @'TypesOf' e@ is a list of every type that can be bound via @e@'s actions.
+--
+-- For example, given:
+--
+-- @
+-- data MyEffect m a where
+--   Foo :: MyEffect m Int
+--   Blah :: Bool -> MyEffect m String
+-- @
+--
+-- the result of @'TypesOf' MyEffect@ is @'[Int, String]@.
+type TypesOf (e :: Effect) = GTypesOf (RepK e)
+
+
+------------------------------------------------------------------------------
+-- | 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)
+
+
+------------------------------------------------------------------------------
+-- | @'SomeAction' e r@ is some action for effect @e@ in effect row @r@.
+data SomeAction e (r :: EffectRow) where
+  SomeAction
+      :: (Member e r, Eq a, Show a, CoArbitrary a, Show (e (Sem r) a))
+      => e (Sem r) a
+         -- ^
+      -> SomeAction e r
+         -- ^
+
+instance Show (SomeAction e r) where
+  show (SomeAction ema) = show ema
+
+instance Show (SomeEff r) where
+  show (SomeEff sse) = show sse
+
+
+------------------------------------------------------------------------------
+-- | @'SomeEff' r@ is some action for some effect in the effect row @r@.
+data SomeEff (r :: EffectRow) where
+  SomeEff
+      :: (Member e r, Eq a, Show a, CoArbitrary a, Show (e (Sem r) a))
+      => e (Sem r) a
+         -- ^
+      -> SomeEff r
+         -- ^
+
+------------------------------------------------------------------------------
+-- | @'SomeEff' r@ is some action for some effect in the effect row @r@.
+data SomeEffOfType (r :: EffectRow) a where
+  SomeEffOfType
+      :: (Member e r, Eq a, Show a, CoArbitrary a, Show (e (Sem r) a))
+      => e (Sem r) a
+         -- ^
+      -> SomeEffOfType r a
+         -- ^
+
+
+------------------------------------------------------------------------------
+-- | @'ArbitraryEff' es r@ lets you randomly generate an action in any of
+-- the effects @es@.
+class ArbitraryEff (es :: EffectRow) (r :: EffectRow) where
+  genSomeEff :: [Gen (SomeEff r)]
+
+instance ArbitraryEff '[] r where
+  genSomeEff = []
+
+instance
+    (ArbitraryEff es r, ArbitraryAction (TypesOf e) e r)
+    => ArbitraryEff (e ': es) r
+    where
+  genSomeEff = fmap (fmap (\(SomeAction e) -> SomeEff e)) (genSomeAction @(TypesOf e) @e @r)
+             <> genSomeEff @es @r
+
+------------------------------------------------------------------------------
+-- | @'ArbitraryEffOfType' a es r@ lets you randomly generate an action in any of
+-- the effects @es@ that produces type @a@.
+class ArbitraryEffOfType (a :: Type) (es :: EffectRow) (r :: EffectRow) where
+  genSomeEffOfType :: [Gen (SomeEffOfType r a)]
+
+instance ArbitraryEffOfType a '[] r where
+  genSomeEffOfType = []
+
+instance
+    ( Eq a
+    , Show a
+    , Show (e (Sem r) a)
+    , ArbitraryEffOfType a es r
+    , GenericK (e (Sem r) a)
+    , GArbitraryK a (RepK (e (Sem r) a))
+    , CoArbitrary a
+    , Member e r
+    )
+    => ArbitraryEffOfType a (e ': es) r
+    where
+  genSomeEffOfType
+    = fmap SomeEffOfType (genEff @e @a @(Sem r))
+    : genSomeEffOfType @a @es @r
+
+
+------------------------------------------------------------------------------
+-- | @'ArbitraryAction' as e r@ lets you randomly generate an action
+-- producing any type in @as@ from the effect @e@.
+class ArbitraryAction (as :: [Type]) (e :: Effect) (r :: EffectRow) where
+  genSomeAction :: [Gen (SomeAction e r)]
+
+instance ArbitraryAction '[] e r where
+  genSomeAction = []
+
+instance
+    ( ArbitraryAction as e r
+    , Eq a
+    , Show a
+    , Member e r
+    , Show (e (Sem r) a)
+    , GenericK (e (Sem r) a)
+    , CoArbitrary a
+    , GArbitraryK a (RepK (e (Sem r) a))
+    )
+    => ArbitraryAction (a : as) e r
+    where
+  genSomeAction = (fmap SomeAction $ genEff @e @a @(Sem r)) : genSomeAction @as @e @r
+
diff --git a/src/Polysemy/Check/Arbitrary/Generic.hs b/src/Polysemy/Check/Arbitrary/Generic.hs
new file mode 100644
--- /dev/null
+++ b/src/Polysemy/Check/Arbitrary/Generic.hs
@@ -0,0 +1,91 @@
+module Polysemy.Check.Arbitrary.Generic where
+
+import Control.Applicative (liftA2)
+import Data.Kind (Type)
+import GHC.Exts (type (~~))
+import Generics.Kind
+import Test.QuickCheck
+import Polysemy
+import Polysemy.Check.Arbitrary.AnyEff
+import Polysemy.Internal (send)
+
+
+------------------------------------------------------------------------------
+
+type a :~~~: b = 'Kon (~~) ':@: a ':@: b
+
+
+------------------------------------------------------------------------------
+-- | 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)]
+
+instance GArbitraryK a U1 where
+  garbitraryk = pure $ pure U1
+
+instance (GArbitraryK1 (f :*: g)) => GArbitraryK a (f :*: g) where
+  garbitraryk = garbitraryk1
+
+instance (GArbitraryK1 (Field b)) => GArbitraryK a (Field b) where
+  garbitraryk = garbitraryk1
+
+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 GArbitraryK1 f => GArbitraryK a ('Kon (a ~~ a) :=>: f) where
+  garbitraryk = fmap SuchThat <$> garbitraryk1
+
+instance {-# INCOHERENT #-} GArbitraryK a ('Kon (a ~~ b) :=>: f) where
+  garbitraryk = []
+
+instance {-# INCOHERENT #-} GArbitraryK a ('Kon (b ~~ c) :=>: f) where
+  garbitraryk = []
+
+instance (GArbitraryK a f) => GArbitraryK a (M1 _1 _2 f) where
+  garbitraryk = fmap M1 <$> garbitraryk @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 = fmap toK $ oneof $ garbitraryk @a @(RepK (e m a))
+
+
+------------------------------------------------------------------------------
+-- | 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 (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
+
+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
+
+instance {-# OVERLAPPING #-} ArbitraryEffOfType a r r => GArbitraryKTerm (Sem r a) where
+  garbitrarykterm = do
+    SomeEffOfType act <- oneof $ genSomeEffOfType @a @r @r
+    pure $ send act
+
+instance {-# OVERLAPPING #-} (CoArbitrary a, GArbitraryKTerm b) => GArbitraryKTerm (a -> b) where
+  garbitrarykterm = liftArbitrary garbitrarykterm
+
+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
new file mode 100644
--- /dev/null
+++ b/src/Polysemy/Check/Arbitrary/Generic.hs-boot
@@ -0,0 +1,19 @@
+module Polysemy.Check.Arbitrary.Generic where
+
+import Data.Kind (Type)
+import Generics.Kind
+import Test.QuickCheck
+
+
+------------------------------------------------------------------------------
+-- | 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)]
+
+------------------------------------------------------------------------------
+-- | @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)
+
diff --git a/src/Polysemy/Check/Orphans.hs b/src/Polysemy/Check/Orphans.hs
new file mode 100644
--- /dev/null
+++ b/src/Polysemy/Check/Orphans.hs
@@ -0,0 +1,54 @@
+{-# OPTIONS_GHC -Wno-orphans #-}
+
+module Polysemy.Check.Orphans () where
+
+import Generics.Kind.TH
+import Polysemy
+import Polysemy.Error
+import Polysemy.Fail
+import Polysemy.Fixpoint
+import Polysemy.Input
+import Polysemy.NonDet
+import Polysemy.Output
+import Polysemy.Reader
+import Polysemy.Resource
+import Polysemy.State
+import Polysemy.Tagged
+import Polysemy.Trace
+import Polysemy.View
+import Polysemy.Writer
+
+deriveGenericK ''Embed
+deriveGenericK ''Error
+deriveGenericK ''Fail
+deriveGenericK ''Fixpoint
+deriveGenericK ''Input
+deriveGenericK ''NonDet
+deriveGenericK ''Output
+deriveGenericK ''Reader
+deriveGenericK ''Resource
+deriveGenericK ''State
+deriveGenericK ''Tagged
+deriveGenericK ''Trace
+deriveGenericK ''View
+deriveGenericK ''Writer
+
+deriving instance Show s => Show (State s (Sem r) a)
+deriving instance Show o => Show (Output o (Sem r) a)
+deriving instance Show (Input i (Sem r) a)
+deriving instance Show (Fail (Sem r) a)
+deriving instance Show (Trace (Sem r) a)
+
+instance Show e => Show (Error e (Sem r) a) where
+  show (Throw e2) = "Throw " <> show e2
+  show (Catch _ _) = "<Catch>"
+
+instance Show (Reader e (Sem r) a) where
+  show Ask = "Ask"
+  show (Local _ _) = "<Local>"
+
+instance Show e => Show (Writer e (Sem r) a) where
+  show (Tell e) = "Tell " <> show e
+  show (Listen _) = "<Listen>"
+  show (Pass _) = "<Pass>"
+
diff --git a/src/Polysemy/Internal/Union/Inject.hs b/src/Polysemy/Internal/Union/Inject.hs
new file mode 100644
--- /dev/null
+++ b/src/Polysemy/Internal/Union/Inject.hs
@@ -0,0 +1,36 @@
+module Polysemy.Internal.Union.Inject
+  ( inject
+  , Inject
+  ) where
+
+import Polysemy.Internal
+import Polysemy.Internal.Union
+
+
+------------------------------------------------------------------------------
+-- | Morally:
+--
+-- @
+-- 'inject' :: 'Members' effs r => 'Sem' effs a -> 'Sem' r a
+-- @
+inject :: Inject effs r => Sem effs a -> Sem r a
+inject (Sem a) = a $ liftSem . deject . hoist inject
+
+
+------------------------------------------------------------------------------
+-- | Helper class for munging the 'Union' so that we can implement 'inject'.
+class Inject effs r where
+  deject :: Union effs (Sem r) a -> Union r (Sem r) a
+
+instance Inject '[] r where
+  deject = absurdU
+
+instance {-# INCOHERENT #-} Inject r r where
+  deject = id
+
+instance (Member eff r, Inject effs r) => Inject (eff ': effs) r where
+  deject u =
+    case decomp u of
+      Left  u' -> deject u'
+      Right w  -> Union membership w
+
diff --git a/test/CommutativeSpec.hs b/test/CommutativeSpec.hs
new file mode 100644
--- /dev/null
+++ b/test/CommutativeSpec.hs
@@ -0,0 +1,34 @@
+module CommutativeSpec where
+
+import Data.Functor.Compose
+import Polysemy
+import Polysemy.Check
+import Polysemy.Error (Error, runError)
+import Polysemy.State
+import Polysemy.Trace
+import Test.Hspec
+import Test.Hspec.QuickCheck
+import Test.QuickCheck
+
+
+spec :: Spec
+spec = do
+  prop "State commutes with Trace" $
+    prepropCommutative @(State Int) @Trace @TestEffs $
+      runTestEffs
+
+  prop "State does not commute with itself" $ expectFailure $
+    prepropCommutative @(State Int) @(State Int) @TestEffs $
+      runTestEffs
+
+  prop "Error does not commute with State (really: we can do Arbitrary stuff on Error)" $ expectFailure $
+    prepropCommutative @(Error Int) @(State Int) @[Error Int, State Int] $
+      pure . Compose . run . runState 0 . runError
+
+
+type TestEffs = '[State Int, Trace, State Int]
+
+runTestEffs :: Sem TestEffs a -> IO (Compose ((,) Int) ((,) [String]) a)
+runTestEffs =
+  pure . Compose . run . runState 0 . runTraceList . subsume
+
diff --git a/test/EquivSpec.hs b/test/EquivSpec.hs
new file mode 100644
--- /dev/null
+++ b/test/EquivSpec.hs
@@ -0,0 +1,45 @@
+{-# LANGUAGE PartialTypeSignatures #-}
+
+{-# OPTIONS_GHC -Wno-orphans             #-}
+{-# OPTIONS_GHC -fplugin=Polysemy.Plugin #-}
+
+module EquivSpec where
+
+import Polysemy
+import Polysemy.Check
+import Test.Hspec
+import Test.QuickCheck
+import Test.Hspec.QuickCheck
+import Polysemy.State
+import Data.IORef (newIORef)
+import Unsafe.Coerce (unsafeCoerce)
+
+
+spec :: Spec
+spec = do
+  prop "Pure state is equivalent to IO state" $ do
+    s0 <- arbitrary
+    pure $
+      prepropEquivalent @'[State Int] @Int
+        (runPureState s0)
+        (runIOState s0)
+        $ ((do
+            SomeAction e1 <- arbitraryAction @(State Int) @r
+            SomeAction e2 <- arbitraryAction @(State Int) @r
+            SomeAction e3 <- arbitraryAction @(State Int) @r
+            -- TODO(sandy): e3 has an existential type! GHC doesn't care, but
+            -- AFAIK, thereis no syntax to return this type, since it doesn't
+            -- exist when we bind 'a' below.
+            pure $ send e1 >> send e2 >> unsafeCoerce (send e3)
+           ) :: forall r a. Member (State Int) r => Gen (Sem r a))
+
+
+runPureState :: Int -> Sem '[State Int] a -> IO a
+runPureState s = pure . run . evalState s
+
+
+runIOState :: Int -> Sem '[State Int, Embed IO] a -> IO (a)
+runIOState s sem = do
+  ref <- newIORef s
+  runM . runStateIORef ref $ sem
+
diff --git a/test/LawSpec.hs b/test/LawSpec.hs
new file mode 100644
--- /dev/null
+++ b/test/LawSpec.hs
@@ -0,0 +1,94 @@
+{-# OPTIONS_GHC -fplugin=Polysemy.Plugin #-}
+
+module LawSpec where
+
+import Polysemy
+import Polysemy.Check
+import Test.Hspec
+import Test.QuickCheck
+import Test.Hspec.QuickCheck
+import Polysemy.State
+import Data.IORef (newIORef, readIORef)
+
+
+spec :: Spec
+spec = do
+  describe "pure state" $ do
+    prop "put >> put = put" $ do
+      s <- arbitrary
+      pure $ putPutLaw $ runPureState s
+    prop "get >>= put = pure ()" $ do
+      s <- arbitrary
+      pure $ getPutLaw $ runPureState s
+    prop "put >> get = put >> pure" $ do
+      s <- arbitrary
+      pure $ putGetLaw $ runPureState s
+
+  describe "io state" $ do
+    prop "put >> put = put" $ do
+      s <- arbitrary
+      pure $ putPutLaw $ runIOState s
+    prop "get >>= put = pure ()" $ do
+      s <- arbitrary
+      pure $ getPutLaw $ runIOState s
+    prop "put >> get = put >> pure" $ do
+      s <- arbitrary
+      pure $ putGetLaw $ runIOState s
+
+
+putPutLaw
+    :: (Arbitrary s, Member (State s) r, Eq x, Show x)
+    => (Sem r s -> IO x)
+    -> Property
+putPutLaw = prepropLaw $ do
+  s1 <- arbitrary
+  s2 <- arbitrary
+  pure
+    ( do
+        put s1
+        put s2
+        get
+    , do
+        put s2
+        get
+    )
+
+
+getPutLaw
+    :: (Arbitrary s, Member (State s) r, Eq x, Show x)
+    => (Sem r () -> IO x)
+    -> Property
+getPutLaw = prepropLaw $ do
+  pure
+    ( get >>= put
+    , pure ()
+    )
+
+
+putGetLaw
+    :: (Arbitrary s, Member (State s) r, Eq x, Show x)
+    => (Sem r s -> IO x)
+    -> Property
+putGetLaw = prepropLaw $ do
+  s <- arbitrary
+  pure
+    ( do
+        put s
+        get
+    , do
+        put s
+        pure s
+    )
+
+
+runPureState :: Int -> Sem '[State Int] a -> IO (Int, a)
+runPureState s = pure . run . runState s
+
+
+runIOState :: Int -> Sem '[State Int, Embed IO] a -> IO (Int, a)
+runIOState s sem = do
+  ref <- newIORef s
+  a <- runM . runStateIORef ref $ sem
+  r <- readIORef ref
+  pure (r, a)
+
diff --git a/test/Main.hs b/test/Main.hs
new file mode 100644
--- /dev/null
+++ b/test/Main.hs
@@ -0,0 +1,1 @@
+{-# OPTIONS_GHC -F -pgmF hspec-discover #-}