diff --git a/ChangeLog.md b/ChangeLog.md
--- a/ChangeLog.md
+++ b/ChangeLog.md
@@ -1,5 +1,44 @@
 # Changelog for polysemy-plugin
 
+## Unreleased
+
+## 0.4.5.0 (2023-04-09)
+
+### Other Changes
+
+* Support GHC 9.6
+
+## 0.4.4.0 (2022-12-27)
+
+* Support GHC 9.4
+
+## 0.4.3.1 (2022-07-11)
+
+* Add a missing pattern match that was hit by a user.
+
+## 0.4.3.0 (2021-11-23)
+
+* Support GHC 9.2.1
+* Fix a regression that prevented disambiguation in some cases.
+
+## 0.4.2.0 (2021-11-16)
+
+- Support for `polysemy-1.7.0.0`
+
+## 0.4.1.0 (2021-10-22)
+
+- The plugin can now use instances in scope to help solve ambiguous type
+    variables.
+
+## 0.4.0.0 (2021-07-12)
+
+* Support GHC 9.0.1
+
+## 0.3.0.0 (2021-03-30)
+
+### Breaking Changes
+* Dropped support for GHC 8.4
+
 ## 0.2.5.2 (2020-11-01)
 
 - Fixed crashes stemming from unused optimization passes
diff --git a/polysemy-plugin.cabal b/polysemy-plugin.cabal
--- a/polysemy-plugin.cabal
+++ b/polysemy-plugin.cabal
@@ -1,104 +1,127 @@
-cabal-version:      2.0
-name:               polysemy-plugin
-version:            0.2.5.2
-license:            BSD3
-license-file:       LICENSE
-copyright:          2019 Sandy Maguire
-maintainer:         sandy@sandymaguire.me
-author:             Sandy Maguire
-homepage:           https://github.com/isovector/polysemy#readme
-bug-reports:        https://github.com/isovector/polysemy/issues
-synopsis:           Disambiguate obvious uses of effects.
-description:
-    Please see the README on GitHub at <https://github.com/isovector/polysemy/tree/master/polysemy-plugin#readme>
+cabal-version: 2.0
 
-category:           Polysemy
-build-type:         Custom
+-- This file has been generated from package.yaml by hpack version 0.36.1.
+--
+-- see: https://github.com/sol/hpack
+
+name:           polysemy-plugin
+version:        0.4.5.3
+synopsis:       Disambiguate obvious uses of effects.
+description:    Please see the README on GitHub at <https://github.com/polysemy-research/polysemy/tree/master/polysemy-plugin#readme>
+category:       Polysemy
+homepage:       https://github.com/polysemy-research/polysemy#readme
+bug-reports:    https://github.com/polysemy-research/polysemy/issues
+author:         Sandy Maguire
+maintainer:     sandy@sandymaguire.me
+copyright:      2019 Sandy Maguire
+license:        BSD3
+license-file:   LICENSE
+build-type:     Custom
 extra-source-files:
     README.md
     ChangeLog.md
 
 source-repository head
-    type:     git
-    location: https://github.com/isovector/polysemy
+  type: git
+  location: https://github.com/polysemy-research/polysemy
 
 custom-setup
-    setup-depends:
-        Cabal >=3.0.1.0 && <3.1,
-        base >=4.9 && <5,
-        cabal-doctest >=1.0.6 && <1.1
+  setup-depends:
+      Cabal <3.13
+    , base >=4.9 && <5
+    , cabal-doctest >=1.0.6 && <1.1
 
 flag corelint
-    description: Perform the corelint tests
-    default:     False
-    manual:      True
+  description: Perform the corelint tests
+  manual: True
+  default: False
 
 library
-    exposed-modules:
-        Polysemy.Plugin
-        Polysemy.Plugin.Fundep
-        Polysemy.Plugin.Fundep.Stuff
-        Polysemy.Plugin.Fundep.Unification
-        Polysemy.Plugin.Fundep.Utils
-
-    hs-source-dirs:     src
-    other-modules:      Paths_polysemy_plugin
-    autogen-modules:    Paths_polysemy_plugin
-    default-language:   Haskell2010
-    default-extensions:
-        DataKinds DeriveFunctor FlexibleContexts GADTs LambdaCase PolyKinds
-        RankNTypes ScopedTypeVariables StandaloneDeriving TypeApplications
-        TypeOperators TypeFamilies UnicodeSyntax
-
-    build-depends:
-        base >=4.9 && <5,
-        containers >=0.5 && <0.7,
-        ghc >=8.4.4 && <9,
-        ghc-tcplugins-extra >=0.3 && <0.5,
-        polysemy >=1.3 && <1.5,
-        syb ==0.7.*,
-        transformers >=0.5.2.0 && <0.6
+  exposed-modules:
+      Polysemy.Plugin
+      Polysemy.Plugin.Fundep
+      Polysemy.Plugin.Fundep.Stuff
+      Polysemy.Plugin.Fundep.Unification
+      Polysemy.Plugin.Fundep.Utils
+  other-modules:
+      Paths_polysemy_plugin
+  autogen-modules:
+      Paths_polysemy_plugin
+  hs-source-dirs:
+      src
+  default-extensions:
+      DataKinds
+      DeriveFunctor
+      FlexibleContexts
+      GADTs
+      LambdaCase
+      PolyKinds
+      RankNTypes
+      ScopedTypeVariables
+      StandaloneDeriving
+      TypeApplications
+      TypeOperators
+      TypeFamilies
+      UnicodeSyntax
+  build-depends:
+      base >=4.9 && <5
+    , containers >=0.5 && <0.8
+    , ghc >=8.6.5 && <10
+    , ghc-tcplugins-extra >=0.3 && <0.6
+    , polysemy >=1.7
+    , syb ==0.7.*
+    , transformers >=0.5.2.0 && <0.7
+  default-language: Haskell2010
 
 test-suite polysemy-plugin-test
-    type:               exitcode-stdio-1.0
-    main-is:            Main.hs
-    build-tool-depends: hspec-discover:hspec-discover -any
-    hs-source-dirs:     test
-    other-modules:
-        BadSpec
-        DoctestSpec
-        ExampleSpec
-        LegitimateTypeErrorSpec
-        MultipleVarsSpec
-        PluginSpec
-        TypeErrors
-        VDQSpec
-        Paths_polysemy_plugin
-        Build_doctests
-
-    autogen-modules:    Build_doctests
-    default-language:   Haskell2010
-    default-extensions:
-        DataKinds DeriveFunctor FlexibleContexts GADTs LambdaCase PolyKinds
-        RankNTypes ScopedTypeVariables StandaloneDeriving TypeApplications
-        TypeOperators TypeFamilies UnicodeSyntax
-
-    ghc-options:
-        -threaded -rtsopts -with-rtsopts=-N -fplugin=Polysemy.Plugin
-
-    build-depends:
-        base >=4.9 && <5,
-        containers >=0.5 && <0.7,
-        doctest >=0.16.0.1 && <0.17,
-        ghc >=8.4.4 && <9,
-        ghc-tcplugins-extra >=0.3 && <0.5,
-        hspec >=2.6.0 && <3,
-        inspection-testing >=0.4.2 && <0.5,
-        polysemy >=1.3.0.0 && <1.5,
-        polysemy-plugin -any,
-        should-not-typecheck >=2.1.0 && <3,
-        syb ==0.7.*,
-        transformers >=0.5.2.0 && <0.6
-
-    if flag(corelint)
-        ghc-options: -dcore-lint -dsuppress-all
+  type: exitcode-stdio-1.0
+  main-is: Main.hs
+  other-modules:
+      AmbiguousSpec
+      DoctestSpec
+      ExampleSpec
+      InsertSpec
+      LegitimateTypeErrorSpec
+      MultipleVarsSpec
+      PluginSpec
+      TypeErrors
+      VDQSpec
+      Paths_polysemy_plugin
+      Build_doctests
+  autogen-modules:
+      Paths_polysemy_plugin
+      Build_doctests
+  hs-source-dirs:
+      test
+  default-extensions:
+      DataKinds
+      DeriveFunctor
+      FlexibleContexts
+      GADTs
+      LambdaCase
+      PolyKinds
+      RankNTypes
+      ScopedTypeVariables
+      StandaloneDeriving
+      TypeApplications
+      TypeOperators
+      TypeFamilies
+      UnicodeSyntax
+  ghc-options: -threaded -rtsopts -with-rtsopts=-N -fplugin=Polysemy.Plugin
+  build-depends:
+      base >=4.9 && <5
+    , containers >=0.5 && <0.8
+    , doctest >=0.16.0.1 && <0.25
+    , ghc >=8.6.5 && <10
+    , ghc-tcplugins-extra >=0.3 && <0.6
+    , hspec >=2.6.0 && <3
+    , hspec-discover
+    , inspection-testing >=0.4.2 && <0.7
+    , polysemy >=1.3.0.0
+    , polysemy-plugin
+    , should-not-typecheck >=2.1.0 && <3
+    , syb ==0.7.*
+    , transformers >=0.5.2.0 && <0.7
+  default-language: Haskell2010
+  if flag(corelint)
+    ghc-options: -dcore-lint -dsuppress-all
diff --git a/src/Polysemy/Plugin.hs b/src/Polysemy/Plugin.hs
--- a/src/Polysemy/Plugin.hs
+++ b/src/Polysemy/Plugin.hs
@@ -63,7 +63,11 @@
 
 import Polysemy.Plugin.Fundep
 
+#if __GLASGOW_HASKELL__ >= 900
+import GHC.Plugins
+#else
 import GhcPlugins
+#endif
 
 ------------------------------------------------------------------------------
 plugin :: Plugin
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
@@ -1,6 +1,8 @@
+{-# LANGUAGE CPP                        #-}
+{-# LANGUAGE DerivingStrategies         #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE RecordWildCards            #-}
 {-# LANGUAGE ViewPatterns               #-}
-{-# LANGUAGE CPP                        #-}
 
 ------------------------------------------------------------------------------
 -- The MIT License (MIT)
@@ -35,25 +37,68 @@
 module Polysemy.Plugin.Fundep (fundepPlugin) where
 
 import           Control.Monad
+import           Control.Monad.Trans.Class (lift)
+import           Control.Monad.Trans.State
 import           Data.Bifunctor
 import           Data.Coerce
+import           Data.Function (on)
 import           Data.IORef
 import qualified Data.Map as M
 import           Data.Maybe
+import           Data.Set (Set)
 import qualified Data.Set as S
+import           Data.Traversable (for)
 import           Polysemy.Plugin.Fundep.Stuff
 import           Polysemy.Plugin.Fundep.Unification
 import           Polysemy.Plugin.Fundep.Utils
-import           TcEvidence
-import           TcPluginM (TcPluginM, tcPluginIO)
-import           TcRnTypes
+
+#if __GLASGOW_HASKELL__ >= 906
+#define SUBST Subst
+#define GET_TYVAR getTyVar_maybe
+import           GHC.Core.TyCo.Subst (SUBST)
+import           GHC.Core.TyCo.Compare (eqType, nonDetCmpType)
+#else
+#define SUBST TCvSubst
+#define GET_TYVAR tcGetTyVar_maybe
+#endif
+
+#if __GLASGOW_HASKELL__ >= 912
+import           GHC.Tc.Types.CtLoc
+#endif
+
+#if __GLASGOW_HASKELL__ >= 900
+import           GHC.Builtin.Types.Prim (alphaTys)
+import           GHC.Plugins (idType, tyConClass_maybe, ppr, Outputable, sep, text, (<+>), parens, emptyUFM)
+import           GHC.Tc.Types.Evidence
+import           GHC.Tc.Plugin (TcPluginM, tcPluginIO)
+import           GHC.Tc.Types
+import           GHC.Tc.Types.Constraint
+import           GHC.Tc.Utils.Env (tcGetInstEnvs)
+import           GHC.Tc.Utils.TcType (tcSplitPhiTy, tcSplitTyConApp, GET_TYVAR, tcSplitAppTy_maybe)
+import           GHC.Tc.Solver.Monad hiding (tcLookupClass)
+import           GHC.Core.Class (classTyCon)
+import           GHC.Core.InstEnv (lookupInstEnv, is_dfun)
+import           GHC.Core.Type
+import           GHC.Utils.Monad (allM, anyM)
+
+#else
 #if __GLASGOW_HASKELL__ >= 810
 import           Constraint
 #endif
+
+import           Class (classTyCon)
+import           GhcPlugins (idType, tyConClass_maybe, ppr, Outputable, sep, text, (<+>), parens)
+import           Inst (tcGetInstEnvs)
+import           InstEnv (lookupInstEnv, is_dfun)
+import           MonadUtils (allM, anyM)
+import           TcEvidence
+import           TcPluginM (tcPluginIO)
+import           TcRnTypes
+import           TcType (tcSplitPhiTy, tcSplitTyConApp, GET_TYVAR, tcSplitAppTy_maybe)
 import           TcSMonad hiding (tcLookupClass)
 import           Type
-
-
+import           TysPrim (alphaTys)
+#endif
 
 fundepPlugin :: TcPlugin
 fundepPlugin = TcPlugin
@@ -62,10 +107,25 @@
           <*> polysemyStuff
   , tcPluginSolve = solveFundep
   , tcPluginStop = const $ pure ()
+#if __GLASGOW_HASKELL__ >= 904
+  , tcPluginRewrite = \ _ -> emptyUFM
+#endif
   }
 
 
 ------------------------------------------------------------------------------
+-- | Like 'PredType', but has an 'Ord' instance.
+newtype PredType' = PredType' { getPredType :: PredType }
+  deriving newtype Outputable
+
+instance Eq PredType' where
+  (==) = ((== EQ) .) . compare
+
+instance Ord PredType' where
+  compare = nonDetCmpType `on` getPredType
+
+
+------------------------------------------------------------------------------
 -- | Corresponds to a 'Polysemy.Internal.Union.Find' constraint. For example,
 -- given @Member (State s) r@, we would get:
 data FindConstraint = FindConstraint
@@ -75,12 +135,23 @@
   , fcRow        :: Type  -- ^ @r@
   }
 
+instance Outputable FindConstraint where
+  ppr FindConstraint{..} = parens $ sep
+    [ text "effect name = " <+> ppr fcEffectName
+    , text "effect = " <+> ppr fcEffect
+    , text "row = " <+> ppr fcRow
+    ]
 
+
 ------------------------------------------------------------------------------
 -- | Given a list of constraints, filter out the 'FindConstraint's.
 getFindConstraints :: PolysemyStuff 'Things -> [Ct] -> [FindConstraint]
 getFindConstraints (findClass -> cls) cts = do
-  cd@CDictCan{cc_class = cls', cc_tyargs = [_, eff, r]} <- cts
+#if MIN_VERSION_GLASGOW_HASKELL(9,8,0,0)
+  cd@(CDictCan(DictCt{di_cls = cls', di_tys = [eff, r]})) <- cts
+#else
+  cd@CDictCan{cc_class = cls', cc_tyargs = [eff, r]} <- cts
+#endif
   guard $ cls == cls'
   pure $ FindConstraint
     { fcLoc = ctLoc cd
@@ -91,21 +162,69 @@
 
 
 ------------------------------------------------------------------------------
--- | If there's only a single @Member@ in the same @r@ whose effect name
--- matches and could possibly unify, return its effect (including tyvars.)
+-- | Get evidence in scope that aren't the 'FindConstraint's.
+getExtraEvidence :: PolysemyStuff 'Things -> [Ct] -> [PredType]
+getExtraEvidence things cts = do
+#if MIN_VERSION_GLASGOW_HASKELL(9,8,0,0)
+  CDictCan(DictCt{di_cls = cls, di_tys = as}) <- cts
+#else
+  CDictCan{cc_class = cls, cc_tyargs = as} <- cts
+#endif
+  guard $ cls /= findClass things
+  pure $ mkAppTys (mkTyConTy $ classTyCon cls) as
+
+
+------------------------------------------------------------------------------
+-- | If there's a unique given @Member@ that would cause the program to
+-- typecheck, use it.
 findMatchingEffectIfSingular
-    :: FindConstraint
-    -> [FindConstraint]
-    -> Maybe Type
-findMatchingEffectIfSingular (FindConstraint _ eff_name wanted r) ts =
-  singleListToJust $ do
-    FindConstraint _ eff_name' eff' r' <- ts
-    guard $ eqType eff_name eff_name'
-    guard $ eqType r r'
-    guard $ canUnifyRecursive FunctionDef wanted eff'
-    pure eff'
+    :: [PredType]        -- ^ Extra wanteds
+    -> Set PredType'     -- ^ Extra givens
+    -> FindConstraint    -- ^ Goal
+    -> [FindConstraint]  -- ^ Member constraints
+    -> TcM (Maybe Type)
+findMatchingEffectIfSingular
+    extra_wanted
+    extra_given
+    (FindConstraint _ eff_name wanted r)
+    ts =
+  let skolems = S.fromList $ foldMap (tyCoVarsOfTypeWellScoped . fcEffect) ts
+      -- Which members unify with our current goal?
+      results = do
+        FindConstraint _ eff_name' eff' r' <- ts
+        guard $ eqType eff_name eff_name'
+        guard $ eqType r r'
+        subst <- maybeToList $ unify (FunctionDef skolems) wanted eff'
+        pure (eff', subst)
+   in case results of
+        [] -> pure Nothing
+        -- If there is a unique member which unifies, return it.
+        [(a, _)] -> pure $ Just a
+        _ ->
+          -- Otherwise, check if the extra wanteds give us enough information
+          -- to make a unique choice.
+          --
+          -- For example, if we're trying to solve @Member (State a) r@, with
+          -- candidates @Members (State Int, State String) r@ and can prove
+          -- that @Num a@, then we can uniquely choose @State Int@.
+          fmap (singleListToJust . join) $ for results $ \(eff, subst) ->
+            fmap maybeToList $
+              anyM (checkExtraEvidence extra_given subst) extra_wanted >>= \case
+                True -> pure $ Just eff
+                False -> pure Nothing
 
+------------------------------------------------------------------------------
+-- | @checkExtraEvidence givens subst c@ returns 'True' iff we can prove that
+-- the constraint @c@ holds under the substitution @subst@ in the context of
+-- @givens@.
+checkExtraEvidence ::
+  Set PredType' ->
+  SUBST ->
+  PredType ->
+  TcM Bool
+checkExtraEvidence givens subst = flip evalStateT givens . getInstance . substTy subst
 
+
 ------------------------------------------------------------------------------
 -- | Given an effect, compute its effect name.
 getEffName :: Type -> Type
@@ -120,16 +239,35 @@
   -> Type
   -> TcPluginM (Unification, Ct)
 mkWantedForce fc given = do
+#if __GLASGOW_HASKELL__ >= 904
+  ((ev, _), _) <- unsafeTcPluginTcM
+           . runTcS
+           $ newWantedEq (fcLoc fc) emptyRewriterSet Nominal wanted given
+#else
   (ev, _) <- unsafeTcPluginTcM
            . runTcSDeriveds
            $ newWantedEq (fcLoc fc) Nominal wanted given
+#endif
   pure ( Unification (OrdType wanted) (OrdType given)
        , CNonCanonical ev
        )
   where
     wanted = fcEffect fc
 
+
 ------------------------------------------------------------------------------
+-- | It's very important that we don't try to unify entire effects when we're
+-- in interpreter mode. It's OK to unify @T x ~ T y@, but never @e ~ T y@. This
+-- function takes then "given" of an interpreter, and produces a singleton
+-- skolem set iff the outermost effect to be unified is a tyvar.
+skolemsForInterpreter :: Type -> Set TyVar
+skolemsForInterpreter ty =
+  case tcSplitAppTy_maybe ty of
+    Just (GET_TYVAR -> Just skolem, _) -> S.singleton skolem
+    _ -> maybe mempty S.singleton $ GET_TYVAR ty
+
+
+------------------------------------------------------------------------------
 -- | Generate a wanted unification for the effect described by the
 -- 'FindConstraint' and the given effect --- if they can be unified in this
 -- context.
@@ -138,51 +276,14 @@
     -> SolveContext
     -> Type  -- ^ The given effect.
     -> TcPluginM (Maybe (Unification, Ct))
-mkWanted fc solve_ctx given =
-  whenA (not (mustUnify solve_ctx) || canUnifyRecursive solve_ctx wanted given) $
+mkWanted fc solve_ctx given = do
+  whenA (not (mustUnify solve_ctx) || isJust (unify solve_ctx wanted given)) $
     mkWantedForce fc given
   where
     wanted = fcEffect fc
 
 
 ------------------------------------------------------------------------------
--- | Given a list of 'Ct's, find any that are of the form
--- @[Irred] Sem r a ~ Something@, and return their @r@s.
-getBogusRs :: PolysemyStuff 'Things -> [Ct] -> [Type]
-getBogusRs stuff wanteds = do
-  CIrredCan ct _ <- wanteds
-  (_, [_, _, a, b]) <- pure . splitAppTys $ ctev_pred ct
-  maybeToList (extractRowFromSem stuff a)
-    ++ maybeToList (extractRowFromSem stuff b)
-
-
-------------------------------------------------------------------------------
--- | Take the @r@ out of @Sem r a@.
-extractRowFromSem :: PolysemyStuff 'Things -> Type -> Maybe Type
-extractRowFromSem (semTyCon -> sem) ty = do
-  (tycon, [r, _]) <- splitTyConApp_maybe ty
-  guard $ tycon == sem
-  pure r
-
-
-------------------------------------------------------------------------------
--- | Given a list of bogus @r@s, and the wanted constraints, produce bogus
--- evidence terms that will prevent @IfStuck (LocateEffect _ r) _ _@ error messsages.
-solveBogusError :: PolysemyStuff 'Things -> [Ct] -> [(EvTerm, Ct)]
-solveBogusError stuff wanteds = do
-  let splitTyConApp_list = maybeToList  . splitTyConApp_maybe
-
-  let bogus = getBogusRs stuff wanteds
-  ct@(CIrredCan ce _) <- wanteds
-  (stuck, [_, _, expr, _, _]) <- splitTyConApp_list $ ctev_pred ce
-  guard $ stuck == ifStuckTyCon stuff
-  (idx, [_, _, r]) <- splitTyConApp_list expr
-  guard $ idx == locateEffectTyCon stuff
-  guard $ elem @[] (OrdType r) $ coerce bogus
-  pure (error "bogus proof for stuck type family", ct)
-
-
-------------------------------------------------------------------------------
 -- | Determine if there is exactly one wanted find for the @r@ in question.
 exactlyOneWantedForR
     :: [FindConstraint]  -- ^ Wanted finds
@@ -202,22 +303,70 @@
                $ OrdType . fcRow <$> wanteds
 
 
+------------------------------------------------------------------------------
+-- | Returns 'True' if we can prove the given 'PredType' has a (fully
+-- instantiated) instance. Uses 'StateT' to cache the results of any instances
+-- it needs to prove in service of the original goal.
+getInstance :: PredType -> StateT (Set PredType') TcM Bool
+getInstance predty = do
+  givens <- get
+  case S.member (PredType' predty) givens of
+    True -> pure True
+    False ->
+      let (con, apps) = tcSplitTyConApp predty
+      in case tyConClass_maybe con of
+        Nothing -> pure False
+        Just cls -> do
+          env <- lift tcGetInstEnvs
+          let (mres, _, _) = lookupInstEnv False env cls apps
+          case mres of
+            ((inst, mapps) : _) -> do
+              -- Get the instantiated type of the dictionary
+              let df = piResultTys (idType $ is_dfun inst)
+                    $ zipWith fromMaybe alphaTys mapps
+              -- pull off its resulting arguments
+              let (theta, _) = tcSplitPhiTy df
+              allM getInstance theta >>= \case
+                True -> do
+                  -- Record that we can solve this instance, in case it's used
+                  -- elsewhere
+                  modify $ S.insert $ coerce predty
+                  pure True
+                False -> pure False
+            _ -> pure False
+
+
 solveFundep
     :: ( IORef (S.Set Unification)
        , PolysemyStuff 'Things
        )
+#if __GLASGOW_HASKELL__ >= 904
+    -> EvBindsVar
     -> [Ct]
     -> [Ct]
+    -> TcPluginM TcPluginSolveResult
+#else
     -> [Ct]
+    -> [Ct]
+    -> [Ct]
     -> TcPluginM TcPluginResult
+#endif
 solveFundep _ _ _ [] = pure $ TcPluginOk [] []
+#if __GLASGOW_HASKELL__ >= 904
+solveFundep (ref, stuff) _ given wanted = do
+#else
 solveFundep (ref, stuff) given _ wanted = do
+#endif
   let wanted_finds = getFindConstraints stuff wanted
       given_finds  = getFindConstraints stuff given
+      extra_wanted = getExtraEvidence stuff wanted
+      extra_given = S.fromList $ coerce $ getExtraEvidence stuff given
 
   eqs <- forM wanted_finds $ \fc -> do
     let r  = fcRow fc
-    case findMatchingEffectIfSingular fc given_finds of
+    res <- unsafeTcPluginTcM
+         $ findMatchingEffectIfSingular extra_wanted extra_given fc given_finds
+    case res of
       -- We found a real given, therefore we are in the context of a function
       -- with an explicit @Member e r@ constraint. We also know it can
       -- be unified (although it may generate unsatisfiable constraints).
@@ -230,8 +379,10 @@
         case splitAppTys r of
           (_, [_, eff', _]) ->
             mkWanted fc
-                     (InterpreterUse $ exactlyOneWantedForR wanted_finds r)
-                     eff'
+              (InterpreterUse
+                (exactlyOneWantedForR wanted_finds r)
+                (skolemsForInterpreter eff'))
+              eff'
           _ -> pure Nothing
 
   -- We only want to emit a unification wanted once, otherwise a type error can
@@ -240,4 +391,5 @@
   let (unifications, new_wanteds) = unzipNewWanteds already_emitted $ catMaybes eqs
   tcPluginIO $ modifyIORef ref $ S.union $ S.fromList unifications
 
-  pure $ TcPluginOk (solveBogusError stuff wanted) new_wanteds
+  pure $ TcPluginOk [] new_wanteds
+
diff --git a/src/Polysemy/Plugin/Fundep/Stuff.hs b/src/Polysemy/Plugin/Fundep/Stuff.hs
--- a/src/Polysemy/Plugin/Fundep/Stuff.hs
+++ b/src/Polysemy/Plugin/Fundep/Stuff.hs
@@ -7,14 +7,34 @@
   ) where
 
 import Data.Kind (Type)
-import FastString (fsLit)
 import GHC (Name, Class, TyCon, mkModuleName)
 import GHC.TcPluginM.Extra (lookupModule, lookupName)
+#if __GLASGOW_HASKELL__ >= 900
+import GHC.Data.FastString (fsLit)
+import GHC.Types.Name.Occurrence (mkTcOcc)
+import GHC.Tc.Plugin (TcPluginM, tcLookupClass, tcLookupTyCon, unsafeTcPluginTcM)
+import GHC.Plugins (getDynFlags)
+import GHC.Unit.State (lookupModuleWithSuggestions, LookupResult (..), UnitState)
+import GHC.Utils.Outputable (text, (<+>), ($$))
+#if __GLASGOW_HASKELL__ >= 902
+import GHC.Tc.Plugin (getTopEnv)
+import GHC.Utils.Panic (pprPanic)
+import GHC.Driver.Env (hsc_units)
+#if __GLASGOW_HASKELL__ >= 904
+import GHC.Types.PkgQual (PkgQual(NoPkgQual))
+#endif
+#else
+import GHC.Plugins (unitState)
+import GHC.Utils.Outputable(pprPanic)
+#endif
+#else
+import FastString (fsLit)
 import OccName (mkTcOcc)
 import TcPluginM (TcPluginM, tcLookupClass, tcLookupTyCon, unsafeTcPluginTcM)
 import GhcPlugins (getDynFlags)
 import Packages (lookupModuleWithSuggestions, LookupResult (..))
-import Outputable (pprPanic, empty, text, (<+>), ($$))
+import Outputable (pprPanic, text, (<+>), ($$))
+#endif
 
 
 
@@ -25,8 +45,6 @@
 data PolysemyStuff (l :: LookupState) = PolysemyStuff
   { findClass         :: ThingOf l Class
   , semTyCon          :: ThingOf l TyCon
-  , ifStuckTyCon      :: ThingOf l TyCon
-  , locateEffectTyCon :: ThingOf l TyCon
   }
 
 
@@ -34,19 +52,33 @@
 -- | All of the things we need to lookup.
 polysemyStuffLocations :: PolysemyStuff 'Locations
 polysemyStuffLocations = PolysemyStuff
-  { findClass         = ("Polysemy.Internal.Union",                  "Find")
-  , semTyCon          = ("Polysemy.Internal",                        "Sem")
-  , ifStuckTyCon      = ("Polysemy.Internal.CustomErrors.Redefined", "IfStuck")
-  , locateEffectTyCon = ("Polysemy.Internal.Union",                  "LocateEffect")
+  { findClass = ("Polysemy.Internal.Union", "Member")
+  , semTyCon  = ("Polysemy.Internal",       "Sem")
   }
 
+#if __GLASGOW_HASKELL__ >= 900
+------------------------------------------------------------------------------
+-- | GHC-version-dependent access of the UnitState
+getUnitState :: TcPluginM UnitState
+getUnitState = do
+#if __GLASGOW_HASKELL__ >= 902
+  topState <- getTopEnv
+  return (hsc_units topState)
+#else
+  dflags <- unsafeTcPluginTcM getDynFlags
+  return (unitState dflags)
+#endif
+#endif
 
 ------------------------------------------------------------------------------
 -- | Lookup all of the 'PolysemyStuff'.
 polysemyStuff :: TcPluginM (PolysemyStuff 'Things)
 polysemyStuff = do
+#if __GLASGOW_HASKELL__ >= 900
+  theUnitState <- getUnitState
+#else
   dflags <- unsafeTcPluginTcM getDynFlags
-
+#endif
   let error_msg = pprPanic "polysemy-plugin"
           $ text ""
          $$ text "--------------------------------------------------------------------------------"
@@ -55,7 +87,19 @@
          $$ text "Probable fix: add `polysemy` to your cabal `build-depends`"
          $$ text "--------------------------------------------------------------------------------"
          $$ text ""
-  case lookupModuleWithSuggestions dflags (mkModuleName "Polysemy") Nothing of
+  case lookupModuleWithSuggestions
+#if __GLASGOW_HASKELL__ >= 900
+    theUnitState
+#else
+    dflags
+#endif
+    (mkModuleName "Polysemy")
+#if __GLASGOW_HASKELL__ >= 904    
+    NoPkgQual
+#else
+    Nothing 
+#endif
+    of
     LookupHidden _ _ -> error_msg
     LookupNotFound _ -> error_msg
 #if __GLASGOW_HASKELL__ >= 806
@@ -63,11 +107,9 @@
 #endif
     _                -> pure ()
 
-  let PolysemyStuff a b c d = polysemyStuffLocations
+  let PolysemyStuff a b = polysemyStuffLocations
   PolysemyStuff <$> doLookup a
                 <*> doLookup b
-                <*> doLookup c
-                <*> doLookup d
 
 
 ------------------------------------------------------------------------------
diff --git a/src/Polysemy/Plugin/Fundep/Unification.hs b/src/Polysemy/Plugin/Fundep/Unification.hs
--- a/src/Polysemy/Plugin/Fundep/Unification.hs
+++ b/src/Polysemy/Plugin/Fundep/Unification.hs
@@ -1,111 +1,102 @@
-{-# LANGUAGE CPP                       #-}
+{-# LANGUAGE CPP #-}
 
 module Polysemy.Plugin.Fundep.Unification where
 
 import           Data.Bool
 import           Data.Function (on)
+import           Data.Set (Set)
 import qualified Data.Set as S
-#if __GLASGOW_HASKELL__ >= 810
+
+#if __GLASGOW_HASKELL__ >= 900
+import           GHC.Tc.Types.Constraint
+#elif __GLASGOW_HASKELL__ >= 810
 import           Constraint
 #else
 import           TcRnTypes
 #endif
 
+#if __GLASGOW_HASKELL__ >= 900
+import           GHC.Core.Type
+import           GHC.Core.Unify
+import           GHC.Plugins (Outputable, ppr, parens, text, (<+>))
+#else
 import           Type
+import           Unify
+import           GhcPlugins (Outputable, ppr, parens, text, (<+>))
+#endif
 
+#if __GLASGOW_HASKELL__ >= 906
+#define SUBST Subst
+import           GHC.Core.TyCo.Subst (SUBST)
+import           GHC.Core.TyCo.Compare (eqType, nonDetCmpType)
+#else
+#define SUBST TCvSubst
+#endif
 
+
 ------------------------------------------------------------------------------
 -- | 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 a function definition. The @Set TyVar@ is all of the
+    -- skolems that exist in the [G] constraints for this function.
+    FunctionDef (Set TyVar)
     -- | 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)
+  | InterpreterUse Bool (Set TyVar)
+  deriving (Eq, Ord)
 
+instance Outputable SolveContext where
+  ppr (FunctionDef s) = parens $ text "FunctionDef" <+> ppr s
+  ppr (InterpreterUse s ty) = parens $ text "InterpreterUse" <+> ppr s <+> ppr ty
 
+
 ------------------------------------------------------------------------------
 -- | Depending on the context in which we're solving a constraint, we may or
 -- may not want to force a unification of effects. For example, when defining
 -- user code whose type is @Member (State Int) r => ...@, if we see @get :: Sem
 -- r s@, we should unify @s ~ Int@.
 mustUnify :: SolveContext -> Bool
-mustUnify FunctionDef = True
-mustUnify (InterpreterUse b) = b
+mustUnify (FunctionDef _) = True
+mustUnify (InterpreterUse b _) = b
 
 
 ------------------------------------------------------------------------------
--- | Determine whether or not two effects are unifiable. This is nuanced.
---
--- There are several cases:
---
--- 1. [W] ∀ e1. e1   [G] ∀ e2. e2
---    Always fails, because we never want to unify two effects if effect names
---    are polymorphic.
---
--- 2. [W] State s    [G] State Int
---    Always succeeds. It's safe to take our given as a fundep annotation.
---
--- 3. [W] State Int  [G] State s
---        (when the [G] is a given that comes from a type signature)
---
---    This should fail, because it means we wrote the type signature @Member
---    (State s) r => ...@, but are trying to use @s@ as an @Int@. Clearly
---    bogus!
---
--- 4. [W] State Int  [G] State s
---        (when the [G] was generated by running an interpreter)
---
---    Sometimes OK, but only if the [G] is the only thing we're trying to solve
---    right now. Consider the case:
---
---      runState 5 $ pure @(Sem (State Int ': r)) ()
---
---    Here we have  [G] forall a. Num a => State a  and  [W] State Int. Clearly
---    the typechecking should flow "backwards" here, out of the row and into
---    the type of 'runState'.
+-- | Determine whether or not two effects are unifiable.
 --
---    What happens if there are multiple [G]s in scope for the same @r@? Then
---    we'd emit multiple unification constraints for the same effect but with
---    different polymorphic variables, which would unify a bunch of effects
---    that shouldn't be!
-canUnifyRecursive
+-- All free variables in [W] constraints are considered skolems, and thus are
+-- not allowed to unify with anything but themselves. This properly handles all
+-- cases in which we are unifying ambiguous [W] constraints (which are true
+-- type variables) against [G] constraints.
+unify
     :: SolveContext
     -> Type  -- ^ wanted
     -> Type  -- ^ given
-    -> Bool
-canUnifyRecursive solve_ctx = go True
+    -> Maybe SUBST
+unify solve_ctx = tryUnifyUnivarsButNotSkolems skolems
   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 =
+    skolems :: Set TyVar
+    skolems =
       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
-
+        InterpreterUse _ s -> s
+        FunctionDef s      -> s
 
-------------------------------------------------------------------------------
--- | A non-recursive version of 'canUnifyRecursive'.
-canUnify :: Bool -> Type -> Type -> Bool
-canUnify poly_given_ok wt gt =
-  or [ isTyVarTy wt
-     , isTyVarTy gt && poly_given_ok
-     , eqType wt gt
-     ]
+#if __GLASGOW_HASKELL__ >= 902
+#define BINDME (const BindMe)
+#define APART (const Apart)
+#else
+#define BINDME BindMe
+#define APART Skolem
+#endif
 
+tryUnifyUnivarsButNotSkolems :: Set TyVar -> Type -> Type -> Maybe SUBST
+tryUnifyUnivarsButNotSkolems skolems goal inst =
+  case tcUnifyTysFG
+         (bool BINDME APART . flip S.member skolems)
+         [inst]
+         [goal] of
+    Unifiable subst -> pure subst
+    _               -> Nothing
 
 ------------------------------------------------------------------------------
 -- | A wrapper for two types that we want to say have been unified.
diff --git a/test/AmbiguousSpec.hs b/test/AmbiguousSpec.hs
new file mode 100644
--- /dev/null
+++ b/test/AmbiguousSpec.hs
@@ -0,0 +1,67 @@
+{-# LANGUAGE AllowAmbiguousTypes   #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+
+module AmbiguousSpec where
+
+import Control.Monad.IO.Class (liftIO)
+import Data.Functor.Identity
+import Data.Monoid
+import Polysemy
+import Polysemy.Embed (runEmbedded)
+import Polysemy.Error (Error, runError)
+import Polysemy.State
+import Polysemy.Tagged (Tagged, tag)
+import Test.Hspec
+import Test.ShouldNotTypecheck
+
+class MPTC a b where
+  mptc :: a -> b
+
+instance MPTC Bool Int where
+  mptc _ = 1000
+
+
+uniquelyInt :: Members '[State Int , State String] r => Sem r ()
+uniquelyInt = put 10
+
+uniquelyA :: forall a b r. (Num a, Members '[State a, State b] r) => Sem r ()
+uniquelyA = put 10
+
+uniquelyString :: Members '[State Int , State String] r => Sem r ()
+uniquelyString = put mempty
+
+uniquelyB :: (MPTC Bool b, Members '[State String, State b] r) => Sem r ()
+uniquelyB = put $ mptc False
+
+uniquelyIO :: Members '[Embed IO, Embed Identity] r => Sem r ()
+uniquelyIO = embed $ liftIO $ pure ()
+
+uniquelyState' :: ∀ r . Members [Error (), State ()] r => Sem r ()
+uniquelyState' = pure ()
+
+uniquelyState :: ∀ r . Member (Tagged () (State ())) r => Sem r (Either () ())
+uniquelyState = runError (tag @() uniquelyState')
+-- uniquelyState = runError (tag @() (uniquelyState' @(State () : Error () : r)))
+
+spec :: Spec
+spec = describe "example" $ do
+  it "should run uniquelyInt" $ do
+    let z = run . runState 0 . runState "hello" $ uniquelyInt
+    z `shouldBe` (10, ("hello", ()))
+
+  it "should run uniquelyA" $ do
+    let z = run . runState 0 . runState "hello" $ uniquelyA @Int @String
+    z `shouldBe` (10, ("hello", ()))
+
+  it "should run uniquelyB" $ do
+    let z = run . runState 0 . runState "hello" $ uniquelyB @Int
+    z `shouldBe` (1000, ("hello", ()))
+
+  it "should run uniquelyString" $ do
+    let z = run . runState 0 . runState "hello" $ uniquelyString
+    z `shouldBe` (0, ("", ()))
+
+  it "should run uniquelyIO" $ do
+    z <- runM . runEmbedded @Identity (pure . runIdentity) $ uniquelyIO
+    z `shouldBe` ()
+
diff --git a/test/BadSpec.hs b/test/BadSpec.hs
deleted file mode 100644
--- a/test/BadSpec.hs
+++ /dev/null
@@ -1,38 +0,0 @@
-{-# LANGUAGE TemplateHaskell #-}
-
-{-# OPTIONS_GHC -fdefer-type-errors -fno-warn-deferred-type-errors #-}
-
-module BadSpec where
-
-import Polysemy
-import Polysemy.State
-import Test.Hspec
-import Test.ShouldNotTypecheck
-
-data KVStore k v m a where
-  GetKV :: k -> KVStore k v m (Maybe v)
-
-makeSem ''KVStore
-
-positivePos :: Member (KVStore k v) r => Sem r (Maybe v)
-positivePos = do
-  getKV "hello"
-
-negativePos :: Member (KVStore String v) r => Sem r (Maybe Bool)
-negativePos = do
-  getKV "hello"
-
-badState :: Member (State a) r => Sem r ()
-badState = put ()
-
-
-spec :: Spec
-spec = do
-  describe "incorrectly polymorphic constraint" $ do
-    it "should not typecheck in positive position" $ do
-      shouldNotTypecheck positivePos
-    it "should not typecheck in negative position" $ do
-      shouldNotTypecheck negativePos
-    it "should not typecheck badly polymorphic State" $ do
-      shouldNotTypecheck badState
-
diff --git a/test/ExampleSpec.hs b/test/ExampleSpec.hs
--- a/test/ExampleSpec.hs
+++ b/test/ExampleSpec.hs
@@ -1,5 +1,4 @@
 {-# LANGUAGE TemplateHaskell #-}
-{-# OPTIONS_GHC -fplugin=Polysemy.Plugin #-}
 
 module ExampleSpec where
 
diff --git a/test/InsertSpec.hs b/test/InsertSpec.hs
new file mode 100644
--- /dev/null
+++ b/test/InsertSpec.hs
@@ -0,0 +1,22 @@
+module InsertSpec where
+
+import Polysemy.State (State)
+import Polysemy.Reader (Reader)
+import Polysemy.Internal (insertAt)
+import Polysemy
+import Test.Hspec
+
+insertAtWithIndex :: Sem (e1 : e2 : e3 : e4 : r) a -> Sem (e1 : e2 : Reader i : e3 : e4 : r) a
+insertAtWithIndex = insertAt @2
+
+insertAtAndRaiseUnder :: Sem (e1 : r) a -> Sem (e1 : e2 : State s : e3 : Reader i : e4 : r) a
+insertAtAndRaiseUnder = raise2Under . insertAt @2 . raiseUnder
+
+insertAtEmpty :: Sem (e1 : e2 : r) a -> Sem (e1 : e2 : r) a
+insertAtEmpty = insertAt @2
+
+spec :: Spec
+spec = parallel $ do
+  describe "insert" $ do
+    it "insert" $ do
+      1 `shouldBe` 1
diff --git a/test/TypeErrors.hs b/test/TypeErrors.hs
--- a/test/TypeErrors.hs
+++ b/test/TypeErrors.hs
@@ -1,4 +1,5 @@
 {-# OPTIONS_GHC -fno-warn-missing-signatures #-}
+{-# LANGUAGE CPP #-}
 
 module TypeErrors where
 
@@ -9,6 +10,7 @@
 -- >>> :set -fplugin=Polysemy.Plugin
 -- >>> :m +Polysemy
 -- >>> :m +Polysemy.State
+-- >>> :m +Polysemy.Reader
 -- >>> :m +Data.Maybe
 
 
@@ -21,8 +23,59 @@
 -- ...
 -- ... Couldn't match expected type ...Sem r Bool... with actual type ...Bool...
 -- ...
--- ... Couldn't match expected type ...Maybe a0...
--- ... with actual type ...Sem r0 s0...
+-- ... Couldn't match expected type...Maybe a0...
+-- ... with actual type...Sem r0 s0...
 -- ...
 missingFmap = ()
 
+--------------------------------------------------------------------------------
+-- |
+-- >>> :{
+-- insertSome :: ∀ e1 e2 s r a . Sem (e1 ': e2 ': r) a -> Sem (e1 ': e2 ': State s ': r) a
+-- insertSome = insertAt
+-- :}
+-- ...
+-- ... insertAt: You must provide the index ...
+-- ...
+insertAtUnprovidedIndex = ()
+
+#if __GLASGOW_HASKELL__ < 902
+
+--------------------------------------------------------------------------------
+-- |
+-- >>> :{
+-- insertSome :: Sem (e1 : e2 : e3 : e4 : r) a -> Sem (e1 : e2 : Reader i : e3 : e4 : r) a
+-- insertSome = insertAt @1
+-- :}
+-- ...
+-- ...insertAt: Failed to insert effects at index 1
+-- ...
+-- ... before ...
+-- ...'[e1]
+-- ... after ...
+-- ...e2 : e3 : e4 : r
+-- ...Actual ...
+-- ...e1 : e2 : Reader i : e3 : e4 : r
+-- ...
+insertAtWrongIndex = ()
+
+--------------------------------------------------------------------------------
+-- |
+-- Note: The /Actual/ row doesn't match the return type because of the 'raiseUnder'.
+-- >>> :{
+-- insertSome :: Sem (e1 : r) a -> Sem (e1 : e2 : State s : e3 : Reader i : e4 : r) a
+-- insertSome = raiseUnder . insertAt @2 . raise2Under
+-- :}
+-- ...
+-- ...insertAt: Failed to insert effects at index 2
+-- ...
+-- ... before ...
+-- ...'[e1, State s]
+-- ... after ...
+-- ...e30 : r0
+-- ...Actual ...
+-- ...e1 : State s : e3 : Reader i : e4 : r
+-- ...
+insertAtAndRaiseWrongIndex = ()
+
+#endif