diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,6 +1,20 @@
 Changelog
 =========
 
+Version 0.3.0.0
+---------------
+
+*Feburary 2, 2020*
+
+<https://github.com/mstksg/decidable/releases/tag/v0.3.0.0>
+
+*   Update to work with *singletons-2.6*, the type family update
+*   Change `Evident` to now be a defunctionalization symbol for `Sing`, instead
+    of a type synonym with `TyPred`, to match with *singletons-2.6*.  Most code
+    in practice should be the same.
+*   Fix instances for `FProd`s: now can prove and decide any `FProd f (Wit p)`,
+    and can prove and decide and auto any `FProd f WrappedSing`.
+
 Version 0.2.1.0
 ---------------
 
diff --git a/decidable.cabal b/decidable.cabal
--- a/decidable.cabal
+++ b/decidable.cabal
@@ -4,10 +4,10 @@
 --
 -- see: https://github.com/sol/hpack
 --
--- hash: 6ed0b9a421c5cd0cbd622790a067c8e7f30ed4bda6034a6471ad2064980be446
+-- hash: d32fc68e2c0f9fc18f6d1c665774f308fc7e98fa1f9d71d0de5ffe287b57bae7
 
 name:           decidable
-version:        0.2.1.0
+version:        0.3.0.0
 synopsis:       Combinators for manipulating dependently-typed predicates.
 description:    This library provides combinators and typeclasses for working and manipulating
                 type-level predicates in Haskell, which are represented as matchable type-level
@@ -22,7 +22,7 @@
 copyright:      (c) Justin Le 2018
 license:        BSD3
 license-file:   LICENSE
-tested-with:    GHC >= 8.6
+tested-with:    GHC >= 8.8
 build-type:     Simple
 extra-source-files:
     README.md
@@ -47,9 +47,9 @@
       src
   ghc-options: -Wall -Wredundant-constraints -Wcompat -Werror=incomplete-patterns
   build-depends:
-      base >=4.11 && <5
-    , functor-products
+      base >=4.13 && <5
+    , functor-products >=0.1.1
     , microlens
-    , singletons >=2.5
+    , singletons >=2.6
     , vinyl
   default-language: Haskell2010
diff --git a/src/Data/Type/Predicate.hs b/src/Data/Type/Predicate.hs
--- a/src/Data/Type/Predicate.hs
+++ b/src/Data/Type/Predicate.hs
@@ -134,7 +134,8 @@
 -- @
 -- 'Evident' :: 'Predicate' k
 -- @
-type Evident = (TyPred Sing :: Predicate k)
+data Evident :: Predicate k
+type instance Apply Evident a = Sing a
 
 -- | The always-false predicate
 --
@@ -361,36 +362,118 @@
 instance Provable Evident where
     prove = id
 
--- | @since 2.0.0
-instance Provable (TyPred (Rec Sing)) where
-    prove = singProd
--- | @since 2.0.0
-instance Decidable (TyPred (Rec Sing))
--- | @since 2.0.0
-instance Provable (TyPred (PMaybe Sing)) where
-    prove = singProd
--- | @since 2.0.0
-instance Decidable (TyPred (PMaybe Sing))
--- | @since 2.0.0
-instance Provable (TyPred (NERec Sing)) where
-    prove = singProd
--- | @since 2.0.0
-instance Decidable (TyPred (NERec Sing))
--- | @since 2.0.0
-instance Provable (TyPred (PIdentity Sing)) where
-    prove = singProd
--- | @since 2.0.0
-instance Decidable (TyPred (PIdentity Sing))
--- | @since 2.0.0
-instance Provable (TyPred (PEither Sing)) where
-    prove = singProd
--- | @since 2.0.0
-instance Decidable (TyPred (PEither Sing))
--- | @since 2.0.0
-instance Provable (TyPred (PTup Sing)) where
-    prove = singProd
--- | @since 2.0.0
-instance Decidable (TyPred (PTup Sing))
+-- | @since 3.0.0
+instance Decidable (TyPred WrappedSing)
+-- | @since 3.0.0
+instance Provable (TyPred WrappedSing) where
+    prove = WrapSing
+    
+
+-- | @since 3.0.0
+instance Provable p => Provable (TyPred (Rec (Wit p))) where
+    prove = mapProd (Wit . prove @p) . singProd
+-- | @since 3.0.0
+instance Decidable p => Decidable (TyPred (Rec (Wit p))) where
+    decide = \case
+      SNil         -> Proved RNil
+      x `SCons` xs -> case decide @p x of
+        Proved p -> case decideTC xs of
+          Proved ps -> Proved $ Wit p :& ps
+          Disproved vs -> Disproved $ \case
+            _ :& ps -> vs ps
+        Disproved v -> Disproved $ \case
+          Wit p :& _ -> v p
+
+-- | @since 3.0.0
+instance Provable (TyPred (Rec WrappedSing)) where
+    prove = mapProd WrapSing . singProd
+-- | @since 3.0.0
+instance Decidable (TyPred (Rec WrappedSing))
+
+-- | @since 3.0.0
+instance Provable p => Provable (TyPred (PMaybe (Wit p))) where
+    prove = mapProd (Wit . prove @p) . singProd
+-- | @since 3.0.0
+instance Decidable p => Decidable (TyPred (PMaybe (Wit p))) where
+    decide = \case
+      SNothing -> Proved PNothing
+      SJust x  -> mapDecision (PJust . Wit) (\case PJust (Wit p) -> p)
+                . decide @p
+                $ x
+
+-- | @since 3.0.0
+instance Provable (TyPred (PMaybe WrappedSing)) where
+    prove = mapProd WrapSing . singProd
+-- | @since 3.0.0
+instance Decidable (TyPred (PMaybe WrappedSing))
+
+-- | @since 3.0.0
+instance Provable p => Provable (TyPred (NERec (Wit p))) where
+    prove = mapProd (Wit . prove @p) . singProd
+-- | @since 3.0.0
+instance Decidable p => Decidable (TyPred (NERec (Wit p))) where
+    decide = \case
+      x NE.:%| xs -> case decide @p x of
+        Proved p -> case decideTC xs of
+          Proved ps -> Proved $ Wit p :&| ps
+          Disproved vs -> Disproved $ \case
+            _ :&| ps -> vs ps
+        Disproved v -> Disproved $ \case
+          Wit p :&| _ -> v p
+
+-- | @since 3.0.0
+instance Provable (TyPred (NERec WrappedSing)) where
+    prove = mapProd WrapSing . singProd
+-- | @since 3.0.0
+instance Decidable (TyPred (NERec WrappedSing))
+
+-- | @since 3.0.0
+instance Provable p => Provable (TyPred (PIdentity (Wit p))) where
+    prove = mapProd (Wit . prove @p) . singProd
+-- | @since 3.0.0
+instance Decidable p => Decidable (TyPred (PIdentity (Wit p))) where
+    decide = \case
+      SIdentity x -> mapDecision (PIdentity . Wit) (\case PIdentity (Wit p) -> p)
+                   . decide @p
+                   $ x
+
+-- | @since 3.0.0
+instance Provable (TyPred (PIdentity WrappedSing)) where
+    prove = mapProd WrapSing . singProd
+-- | @since 3.0.0
+instance Decidable (TyPred (PIdentity WrappedSing))
+
+-- | @since 3.0.0
+instance Provable p => Provable (TyPred (PEither (Wit p))) where
+    prove = mapProd (Wit . prove @p) . singProd
+-- | @since 3.0.0
+instance Decidable p => Decidable (TyPred (PEither (Wit p))) where
+    decide = \case
+      SLeft  x -> Proved $ PLeft x
+      SRight y -> mapDecision (PRight . Wit) (\case PRight (Wit p) -> p)
+                . decide @p
+                $ y
+
+-- | @since 3.0.0
+instance Provable (TyPred (PEither WrappedSing)) where
+    prove = mapProd WrapSing . singProd
+-- | @since 3.0.0
+instance Decidable (TyPred (PEither WrappedSing))
+
+-- | @since 3.0.0
+instance Provable p => Provable (TyPred (PTup (Wit p))) where
+    prove = mapProd (Wit . prove @p) . singProd
+-- | @since 3.0.0
+instance Decidable p => Decidable (TyPred (PTup (Wit p))) where
+    decide (STuple2 x y) = mapDecision (PTup x . Wit) (\case PTup _ (Wit p) -> p)
+                         . decide @p
+                         $ y
+
+-- | @since 3.0.0
+instance Provable (TyPred (PTup WrappedSing)) where
+    prove = mapProd WrapSing . singProd
+-- | @since 3.0.0
+instance Decidable (TyPred (PTup WrappedSing))
 
 instance (Decidable p, SingI f) => Decidable (PMap f p) where
     decide = decide @p . applySing (sing :: Sing f)
diff --git a/src/Data/Type/Predicate/Auto.hs b/src/Data/Type/Predicate/Auto.hs
--- a/src/Data/Type/Predicate/Auto.hs
+++ b/src/Data/Type/Predicate/Auto.hs
@@ -180,7 +180,7 @@
     autoElem = IId
 
 instance AutoElem f as a => Auto (In f as) a where
-    auto = autoElem @f @as @a
+    auto = autoElem @_ @f @as @a
 
 -- | Helper class for deriving 'Auto' instances for 'All' predicates; each
 -- 'Universe' instance is expected to implement these if possible, to get
@@ -200,7 +200,7 @@
 instance (Auto p a, AutoAll [] p as) => AutoAll [] p (a ': as) where
     autoAll = WitAll $ \case
         IZ   -> auto @_ @p @a
-        IS i -> runWitAll (autoAll @[] @p @as) i
+        IS i -> runWitAll (autoAll @_ @[] @p @as) i
 
 instance AutoAll Maybe p 'Nothing where
     autoAll = WitAll $ \case {}
@@ -217,7 +217,7 @@
 instance (Auto p a, AutoAll [] p as) => AutoAll NonEmpty p (a ':| as) where
     autoAll = WitAll $ \case
         NEHead   -> auto @_ @p @a
-        NETail i -> runWitAll (autoAll @[] @p @as) i
+        NETail i -> runWitAll (autoAll @_ @[] @p @as) i
 
 instance Auto p a => AutoAll ((,) j) p '(w, a) where
     autoAll = WitAll $ \case ISnd -> auto @_ @p @a
@@ -227,7 +227,7 @@
 
 -- | @since 0.1.2.0
 instance AutoAll f p as => Auto (All f p) as where
-    auto = autoAll @f @p @as
+    auto = autoAll @_ @f @p @as
 
 -- | @since 0.1.2.0
 instance SingI a => Auto (NotNull []) (a ': as) where
@@ -301,7 +301,7 @@
 
 -- | @since 0.1.2.0
 instance (SingI as, AutoAll f (Not p) as) => Auto (Not (Any f p)) as where
-    auto = allNotNone sing $ autoAll @f @(Not p) @as
+    auto = allNotNone sing $ autoAll @_ @f @(Not p) @as
 
 -- | Helper function to generate a @'Not' ('All' f p)@ if you can pick out
 -- a specific @a@ in @as@ where the predicate is disprovable at compile-time.
@@ -321,21 +321,40 @@
     auto = mapRefuted (\(s :&: WitAny i p) -> WitAny i (s :&: p))
          $ auto @_ @(Not (Any f (Found p))) @as
 
--- | @since 2.0.0
-instance SingI as => Auto (TyPred (Rec Sing)) as where
-    auto = singProd sing
--- | @since 2.0.0
-instance SingI as => Auto (TyPred (PMaybe Sing)) as where
-    auto = singProd sing
--- | @since 2.0.0
-instance SingI as => Auto (TyPred (NERec Sing)) as where
-    auto = singProd sing
--- | @since 2.0.0
-instance SingI as => Auto (TyPred (PEither Sing)) as where
-    auto = singProd sing
--- | @since 2.0.0
-instance SingI as => Auto (TyPred (PTup Sing)) as where
-    auto = singProd sing
--- | @since 2.0.0
-instance SingI as => Auto (TyPred (PIdentity Sing)) as where
-    auto = singProd sing
+-- | @since 3.0.0
+instance SingI as => Auto (TyPred (Rec WrappedSing)) as where
+    auto = proveTC sing
+-- | @since 3.0.0
+instance SingI as => Auto (TyPred (PMaybe WrappedSing)) as where
+    auto = proveTC sing
+-- | @since 3.0.0
+instance SingI as => Auto (TyPred (NERec WrappedSing)) as where
+    auto = proveTC sing
+-- | @since 3.0.0
+instance SingI as => Auto (TyPred (PEither WrappedSing)) as where
+    auto = proveTC sing
+-- | @since 3.0.0
+instance SingI as => Auto (TyPred (PTup WrappedSing)) as where
+    auto = proveTC sing
+-- | @since 3.0.0
+instance SingI as => Auto (TyPred (PIdentity WrappedSing)) as where
+    auto = proveTC sing
+
+-- | @since 3.0.0
+instance (SingI as, Provable p) => Auto (TyPred (Rec (Wit p))) as where
+    auto = proveTC sing
+-- | @since 3.0.0
+instance (SingI as, Provable p) => Auto (TyPred (PMaybe (Wit p))) as where
+    auto = proveTC sing
+-- | @since 3.0.0
+instance (SingI as, Provable p) => Auto (TyPred (NERec (Wit p))) as where
+    auto = proveTC sing
+-- | @since 3.0.0
+instance (SingI as, Provable p) => Auto (TyPred (PEither (Wit p))) as where
+    auto = proveTC sing
+-- | @since 3.0.0
+instance (SingI as, Provable p) => Auto (TyPred (PTup (Wit p))) as where
+    auto = proveTC sing
+-- | @since 3.0.0
+instance (SingI as, Provable p) => Auto (TyPred (PIdentity (Wit p))) as where
+    auto = proveTC sing
diff --git a/src/Data/Type/Predicate/Logic.hs b/src/Data/Type/Predicate/Logic.hs
--- a/src/Data/Type/Predicate/Logic.hs
+++ b/src/Data/Type/Predicate/Logic.hs
@@ -42,7 +42,6 @@
 
 import           Data.Singletons
 import           Data.Singletons.Decide
-import           Data.Singletons.Prelude.Bool (Sing(..))
 import           Data.Type.Predicate
 import           Data.Void