diff --git a/ChangeLog.md b/ChangeLog.md
--- a/ChangeLog.md
+++ b/ChangeLog.md
@@ -1,5 +1,13 @@
 # Changelog for polysemy-check
 
+## v0.6.0.0 (2021-10-16)
+
+- Changed the frequencies of `Sem`'s `Arbitrary` instance, to create more
+    interesting programs.
+- Removed the program generator parameter of `prepropEquivalent`. It now just
+    uses the `Arbitrary` instance for `Sem`.
+- Added some new examples to the test suite.
+
 ## v0.5.0.0 (2021-10-14)
 
 - Flattened the module structure of `Polysemy.Check.Arbitrary`.
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.5.0.0
+version:        0.6.0.0
 synopsis:       QuickCheck for Polysemy
 description:    Please see the README on GitHub at <https://github.com/polysemy-research/polysemy-check#readme>
 category:       Polysemy
@@ -71,6 +71,7 @@
       CommutativeSpec
       CoverageSpec
       EquivSpec
+      ExampleSpec
       LawSpec
       WeirdEffectsSpec
       Paths_polysemy_check
diff --git a/src/Polysemy/Check.hs b/src/Polysemy/Check.hs
--- a/src/Polysemy/Check.hs
+++ b/src/Polysemy/Check.hs
@@ -33,7 +33,6 @@
   ) where
 
 import Control.Monad (void)
-import Data.Proxy
 import Generics.Kind (GenericK)
 import Generics.Kind.TH (deriveGenericK)
 import Polysemy
@@ -142,27 +141,27 @@
 
 
 ------------------------------------------------------------------------------
--- | 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.
+-- | Prove that two interpreters are equivalent. This property ensures that the
+-- two interpreters give the same result for every arbitrary program.
 prepropEquivalent
     :: forall effs x r1 r2 f
      . ( forall a. Show a => Show (f a)
        , forall a. Eq a => Eq (f a)
        )
-    => (Eq x, Show x, Inject effs r1, Inject effs r2, Members effs effs)
+    => ( Eq x
+       , Show x
+       , Inject effs r1
+       , Inject effs r2
+       , Arbitrary (Sem effs x)
+       )
     => (forall a. Sem r1 a -> IO (f 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 (f a))
        -- ^ The second interpreter to prove equivalence for.
-    -> (forall r. Proxy 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 Proxy
+prepropEquivalent int1 int2 = property $ do
+  SomeSem sem <- liftGen @effs @x
   pure $ ioProperty $ do
     a1 <- int1 sem
     a2 <- int2 sem
@@ -176,10 +175,9 @@
 
 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
+     . Arbitrary (Sem effs a)
+    => Gen (SomeSem effs a)
+liftGen = do
+  a <- arbitrary @(Sem effs a)
   pure $ SomeSem $ inject a
 
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
@@ -1,3 +1,5 @@
+{-# LANGUAGE TupleSections #-}
+
 {-# OPTIONS_GHC -Wno-orphans #-}
 
 module Polysemy.Check.Arbitrary where
@@ -85,15 +87,15 @@
      in sized $ \n ->
           case n <= 1 of
             True -> oneof terminal
-            False -> oneof $
-              [ do
+            False -> frequency $
+              [ (2,) $ do
                   SomeEffOfType e <- arbitraryActionFromRowOfType @r @r @a
                   pure $ send e
-              , do
+              , (8,) $ do
                   SomeEff e <- arbitraryActionFromRow @r @r
                   k <- liftArbitrary $ scale (`div` 2) arbitrary
                   pure $ send e >>= k
-              ] <> terminal
+              ] <> fmap (1,) terminal
 
 ------------------------------------------------------------------------------
 -- | @genEff \@e \@r \@a@ gets a generator capable of producing every
diff --git a/test/EquivSpec.hs b/test/EquivSpec.hs
--- a/test/EquivSpec.hs
+++ b/test/EquivSpec.hs
@@ -6,7 +6,6 @@
 module EquivSpec where
 
 import Data.IORef (newIORef, readIORef)
-import Data.Proxy (Proxy)
 import Polysemy
 import Polysemy.Check
 import Polysemy.State
@@ -23,11 +22,6 @@
       prepropEquivalent @'[State Int] @Int
         (runPureState s0)
         (runIOState s0)
-        $ \(_ :: Proxy r) -> do
-            SomeAction e1 <- arbitraryAction @(State Int) @r
-            SomeAction e2 <- arbitraryAction @(State Int) @r
-            e3 <- arbitraryActionOfType @(State Int) @Int @r
-            pure $ send e1 >> send e2 >> send e3
 
 
 runPureState :: Int -> Sem '[State Int] a -> IO (Int, a)
diff --git a/test/ExampleSpec.hs b/test/ExampleSpec.hs
new file mode 100644
--- /dev/null
+++ b/test/ExampleSpec.hs
@@ -0,0 +1,123 @@
+{-# OPTIONS_GHC -fplugin=Polysemy.Plugin #-}
+{-# LANGUAGE DerivingStrategies #-}
+{-# LANGUAGE DeriveGeneric #-}
+
+module ExampleSpec where
+
+import Control.Monad
+import Data.Maybe (listToMaybe)
+import Polysemy
+import Polysemy.Check
+import Polysemy.State
+import Test.Hspec
+import Test.Hspec.QuickCheck
+import Test.QuickCheck
+
+
+data Stack s m a where
+  Push      :: s -> Stack s m ()
+  Pop       :: Stack s m (Maybe s)
+  RemoveAll :: Stack s m ()
+  Size      :: Stack s m Int
+
+deriving instance Show s => Show (Stack s m a)
+deriveGenericK ''Stack
+
+makeSem ''Stack
+
+
+spec :: Spec
+spec = do
+  describe "Laws" $ do
+    let law x = prepropLaw @'[Stack Int] x $ pure . run . runStack []
+
+    prop "push >> pop is pure" $ do
+      law $ do
+        s <- arbitrary
+        pure
+          ( push s >> pop
+          , pure $ Just s
+          )
+
+    prop "pop >> push is id" $ do
+      law $
+        pure
+          ( pop >>= maybe (pure ()) push
+          , pure ()
+          )
+
+    prop "removeAll sets size to 0" $ do
+      law $
+        pure
+          ( removeAll >> size
+          , removeAll >> pure 0
+          )
+
+    prop "push increases size by 1" $ do
+      law $ do
+        s <- arbitrary
+        pure
+          ( push s >> size
+          , fmap (+1) size <* push s
+          )
+
+    prop "pop decreases size by 1" $ do
+      law $ do
+        pure
+          ( pop >> size
+          , fmap (max 0 . subtract 1) size <* pop
+          )
+
+
+  describe "Equivalence" $ do
+    let equiv b1 b2 =
+          prepropEquivalent @'[Stack Int] @Int
+            (pure . run . runStack b1)
+            (pure . run . runStack b2)
+
+    prop "All interpreters are equivalent to itself" $ do
+      bugs <- arbitrary
+      pure $ equiv bugs bugs
+
+    prop "DontRemove bug interpreter isn't equivalent to the correct version" $
+      expectFailure $ equiv [DontRemove] []
+
+    prop "PushTwice bug interpreter isn't equivalent to the correct version" $
+      expectFailure $ equiv [PushTwice] []
+
+    prop "The buggy interpreters are not equivalent to one another" $
+      expectFailure $ equiv [PushTwice] [DontRemove]
+
+
+data Bug
+  = PushTwice
+  | DontRemove
+  deriving stock (Eq, Ord, Show, Enum, Bounded)
+
+instance Arbitrary Bug where
+  arbitrary = elements [minBound..maxBound]
+
+
+hasBug :: [Bug] -> Bug -> Bool
+hasBug = flip elem
+
+
+runStack
+    :: [Bug]
+    -> Sem (Stack s ': r) a
+    -> Sem r ([s], a)
+runStack bugs =
+  (runState [] .) $ reinterpret $ \case
+    Push s -> do
+      modify (s :)
+      when (hasBug bugs PushTwice) $
+        modify (s :)
+    Pop -> do
+      r <- gets listToMaybe
+      modify (drop 1)
+      pure r
+    RemoveAll ->
+      unless (hasBug bugs DontRemove) $
+        put []
+    Size -> gets length
+