diff --git a/ChangeLog.md b/ChangeLog.md
--- a/ChangeLog.md
+++ b/ChangeLog.md
@@ -1,5 +1,10 @@
 # Changelog for polysemy-plugin
 
+## 0.2.1.0 (2019-06-14)
+
+- Greatly improved the plugin's ability to unify polymorphic types when running
+    interpreters.
+
 ## 0.2.0.3 (2019-06-13)
 
 - Fixed a bug where the plugin could (incorrectly) loop indefinitely attempting
diff --git a/polysemy-plugin.cabal b/polysemy-plugin.cabal
--- a/polysemy-plugin.cabal
+++ b/polysemy-plugin.cabal
@@ -4,10 +4,10 @@
 --
 -- see: https://github.com/sol/hpack
 --
--- hash: 65e9d7abb09d631f2fc5d94e0710c5770b02658b1e699b39a00e2f673c81beb1
+-- hash: e4dc8b1a6c6d69287ad57b504d173944aea70ea24df70dab669ea1f70715c3b0
 
 name:           polysemy-plugin
-version:        0.2.0.3
+version:        0.2.1.0
 synopsis:       Disambiguate obvious uses of effects.
 description:    Please see the README on GitHub at <https://github.com/isovector/polysemy/tree/master/polysemy-plugin#readme>
 category:       Polysemy
diff --git a/src/Polysemy/Plugin/Fundep.hs b/src/Polysemy/Plugin/Fundep.hs
--- a/src/Polysemy/Plugin/Fundep.hs
+++ b/src/Polysemy/Plugin/Fundep.hs
@@ -34,8 +34,10 @@
 
 import           Class
 import           CoAxiom
+import           Control.Applicative
 import           Control.Monad
 import           Data.Bifunctor
+import           Data.Bool
 import           Data.Function (on)
 import           Data.IORef
 import           Data.List
@@ -89,34 +91,63 @@
 getEffName t = fst $ splitAppTys t
 
 
-canUnify :: Type -> Type -> Bool
-canUnify wanted given =
-  let (w, ws) = splitAppTys wanted
-      (g, gs) = splitAppTys given
-   in (&& eqType w g) . flip all (zip ws gs) $ \(wt, gt) ->
-     or [ isTyVarTy wt
-        , eqType wt gt
-        , canUnify wt gt
-        ]
+canUnifyRecursive :: SolveContext -> Type -> Type -> Bool
+canUnifyRecursive solve_ctx = go True
+  where
+    -- It's only OK to solve a polymorphic "given" if we're in the context of
+    -- an interpreter, because it's not really a given!
+    poly_given_ok :: Bool
+    poly_given_ok =
+      case solve_ctx of
+        InterpreterUse _ -> True
+        FunctionDef      -> False
 
+    -- On the first go around, we don't want to unify effects with tyvars, but
+    -- we _do_ want to unify their arguments, thus 'is_first'.
+    go :: Bool -> Type -> Type -> Bool
+    go is_first wanted given =
+      let (w, ws) = splitAppTys wanted
+          (g, gs) = splitAppTys given
+       in (&& bool (canUnify poly_given_ok) eqType is_first w g)
+        . flip all (zip ws gs)
+        $ \(wt, gt) -> canUnify poly_given_ok wt gt || go False wt gt
 
+
+canUnify :: Bool -> Type -> Type -> Bool
+canUnify poly_given_ok wt gt =
+  or [ isTyVarTy wt
+     , isTyVarTy gt && poly_given_ok
+     , eqType wt gt
+     ]
+
+
+------------------------------------------------------------------------------
+-- | Like 'Control.Monad.when', but in the context of an 'Alternative'.
+whenA
+    :: (Monad m, Alternative z)
+    => Bool
+    -> m a
+    -> m (z a)
+whenA False _ = pure empty
+whenA True ma = fmap pure ma
+
+
 mkWanted
-    :: Bool
+    :: SolveContext
     -> CtLoc
     -> Type
     -> Type
     -> TcPluginM (Maybe ( (OrdType, OrdType)  -- the types we want to unify
                         , Ct                  -- the constraint
                         ))
-mkWanted must_unify loc wanted given =
-  if (not must_unify || canUnify wanted given)
-     then do
-       (ev, _) <- unsafeTcPluginTcM $ runTcSDeriveds $ newWantedEq loc Nominal wanted given
-       pure $ Just ( (OrdType wanted, OrdType given)
-                   , CNonCanonical ev
-                   )
-     else
-       pure Nothing
+mkWanted solve_ctx loc wanted given =
+  whenA (not (mustUnify solve_ctx) || canUnifyRecursive solve_ctx wanted given) $ do
+    (ev, _) <- unsafeTcPluginTcM
+             . runTcSDeriveds
+             $ newWantedEq loc Nominal wanted given
+    pure ( (OrdType wanted, OrdType given)
+         , CNonCanonical ev
+         )
 
 thd :: (a, b, c) -> c
 thd (_, _, c) = c
@@ -142,7 +173,22 @@
   compare = nonDetCmpType `on` getOrdType
 
 
+------------------------------------------------------------------------------
+-- | The context in which we're attempting to solve a constraint.
+data SolveContext
+  = -- | In the context of a function definition.
+    FunctionDef
+    -- | In the context of running an interpreter. The 'Bool' corresponds to
+    -- whether we are only trying to solve a single 'Member' constraint right
+    -- now. If so, we *must* produce a unification wanted.
+  | InterpreterUse Bool
+  deriving (Eq, Ord, Show)
 
+mustUnify :: SolveContext -> Bool
+mustUnify FunctionDef = True
+mustUnify (InterpreterUse b) = b
+
+
 solveFundep
     :: (IORef (S.Set (OrdType, OrdType)), Class)
     -> [Ct]
@@ -162,9 +208,9 @@
       case findMatchingEffectIfSingular e givenEffs of
         Nothing -> do
           case splitAppTys r of
-            (_, [_, eff', _]) -> mkWanted (must_unify r) loc eff eff'
+            (_, [_, eff', _]) -> mkWanted (InterpreterUse $ must_unify r) loc eff eff'
             _                 -> pure Nothing
-        Just eff' -> mkWanted True loc eff eff'
+        Just eff' -> mkWanted FunctionDef loc eff eff'
 
     already_emitted <- tcPluginIO $ readIORef ref
     let new_wanteds = filter (not . flip S.member already_emitted . fst)
diff --git a/test/PluginSpec.hs b/test/PluginSpec.hs
--- a/test/PluginSpec.hs
+++ b/test/PluginSpec.hs
@@ -132,9 +132,8 @@
       flipShouldBe (Right @Bool (10 :: Float, True))  . run $ runError $ runState 0 errState
 
   describe "Output effect" $ do
-    it "should unify recursively" $ do
-      -- TODO(sandy): This should unify even without the type app. Bug #95
-      flipShouldBe 11 . sum @[] . fst . run . runFoldMapOutput id $ do
+    it "should unify recursively with tyvars" $ do
+      flipShouldBe 11 . sum . fst . run . runFoldMapOutput id $ do
         output [1]
         output $ replicate 2 5