diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,3 +1,16 @@
+# Version 0.2
+
+* Depend on `singletons-2.2`, which means `KProxy` is gone.
+
+* Add `_Some{1,2,3,4}` prisms.
+
+* Add `Dict` instance for `Bool`.
+
+* Add `some{1,2,3,4}SingRep`.
+
+* Thanks to Sandy Maguire for having contributed to this release.
+
+
 # Version 0.1.2
 
 * Export the `Some{1,2,3,4}` constructors.
diff --git a/exinst.cabal b/exinst.cabal
--- a/exinst.cabal
+++ b/exinst.cabal
@@ -1,5 +1,5 @@
 name:                exinst
-version:             0.1.2
+version:             0.2
 author:              Renzo Carbonara
 maintainer:          renzoλcarbonara.com.ar
 copyright:           Renzo Carbonara 2015-2016
@@ -21,8 +21,9 @@
       Exinst.Singletons
       Exinst.Instances.Base
   build-depends:
-      base >=4.7 && <5.0
+      base >=4.9 && <5.0
     , constraints >=0.4 && <0.9
-    , singletons >=1.1 && <2.2
+    , profunctors >=5.0 && <6.0
+    , singletons >=2.2 && <2.3
   ghcjs-options: -Wall -O3
   ghc-options: -Wall -O2
diff --git a/src/lib/Exinst/Instances/Base.hs b/src/lib/Exinst/Instances/Base.hs
--- a/src/lib/Exinst/Instances/Base.hs
+++ b/src/lib/Exinst/Instances/Base.hs
@@ -1,7 +1,12 @@
+{-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
 {-# LANGUAGE UndecidableInstances #-}
 
 {-# OPTIONS_GHC -fno-warn-orphans #-}
@@ -14,7 +19,9 @@
 module Exinst.Instances.Base () where
 
 import Data.Constraint
+import Data.Kind (Type)
 import Data.Singletons
+import Data.Singletons.Prelude.Bool (Sing(STrue,SFalse))
 import Data.Singletons.Decide
 import Data.Type.Equality
 import Exinst.Singletons
@@ -33,9 +40,9 @@
 --------------------------------------------------------------------------------
 -- Show
 
-instance forall (f1 :: k1 -> *)
-  . ( SingKind ('KProxy :: KProxy k1)
-    , Show (DemoteRep ('KProxy :: KProxy k1))
+instance forall (f1 :: k1 -> Type)
+  . ( SingKind k1
+    , Show (DemoteRep k1)
     , Dict1 Show f1
     ) => Show (Exinst.Some1 f1)
   where
@@ -44,11 +51,11 @@
        case dict1 sa1 :: Dict (Show (f1 a1)) of
           Dict -> showsPrec n (Some1 (fromSing sa1) x)
 
-instance forall (f2 :: k2 -> k1 -> *)
-  . ( SingKind ('KProxy :: KProxy k2)
-    , SingKind ('KProxy :: KProxy k1)
-    , Show (DemoteRep ('KProxy :: KProxy k2))
-    , Show (DemoteRep ('KProxy :: KProxy k1))
+instance forall (f2 :: k2 -> k1 -> Type)
+  . ( SingKind k2
+    , SingKind k1
+    , Show (DemoteRep k2)
+    , Show (DemoteRep k1)
     , Dict2 Show f2
     ) => Show (Exinst.Some2 f2)
   where
@@ -57,13 +64,13 @@
        case dict2 sa2 sa1 :: Dict (Show (f2 a2 a1)) of
           Dict -> showsPrec n (Some2 (fromSing sa2) (fromSing sa1) x)
 
-instance forall (f3 :: k3 -> k2 -> k1 -> *)
-  . ( SingKind ('KProxy :: KProxy k3)
-    , SingKind ('KProxy :: KProxy k2)
-    , SingKind ('KProxy :: KProxy k1)
-    , Show (DemoteRep ('KProxy :: KProxy k3))
-    , Show (DemoteRep ('KProxy :: KProxy k2))
-    , Show (DemoteRep ('KProxy :: KProxy k1))
+instance forall (f3 :: k3 -> k2 -> k1 -> Type)
+  . ( SingKind k3
+    , SingKind k2
+    , SingKind k1
+    , Show (DemoteRep k3)
+    , Show (DemoteRep k2)
+    , Show (DemoteRep k1)
     , Dict3 Show f3
     ) => Show (Exinst.Some3 f3)
   where
@@ -72,15 +79,15 @@
        case dict3 sa3 sa2 sa1 :: Dict (Show (f3 a3 a2 a1)) of
           Dict -> showsPrec n (Some3 (fromSing sa3) (fromSing sa2) (fromSing sa1) x)
 
-instance forall (f4 :: k4 -> k3 -> k2 -> k1 -> *)
-  . ( SingKind ('KProxy :: KProxy k4)
-    , SingKind ('KProxy :: KProxy k3)
-    , SingKind ('KProxy :: KProxy k2)
-    , SingKind ('KProxy :: KProxy k1)
-    , Show (DemoteRep ('KProxy :: KProxy k4))
-    , Show (DemoteRep ('KProxy :: KProxy k3))
-    , Show (DemoteRep ('KProxy :: KProxy k2))
-    , Show (DemoteRep ('KProxy :: KProxy k1))
+instance forall (f4 :: k4 -> k3 -> k2 -> k1 -> Type)
+  . ( SingKind k4
+    , SingKind k3
+    , SingKind k2
+    , SingKind k1
+    , Show (DemoteRep k4)
+    , Show (DemoteRep k3)
+    , Show (DemoteRep k2)
+    , Show (DemoteRep k1)
     , Dict4 Show f4
     ) => Show (Exinst.Some4 f4)
   where
@@ -96,9 +103,8 @@
 --------------------------------------------------------------------------------
 -- Eq
 
-instance forall (f1 :: k1 -> *)
-  . ( SingKind ('KProxy :: KProxy k1)
-    , SDecide ('KProxy :: KProxy k1)
+instance forall (f1 :: k1 -> Type)
+  . ( SDecide k1
     , Dict1 Eq f1
     ) => Eq (Exinst.Some1 f1)
   where
@@ -111,11 +117,9 @@
                 case dict1 sa1x :: Dict (Eq (f1 a1x)) of
                    Dict -> Just (x == y)
 
-instance forall (f2 :: k2 -> k1 -> *)
-  . ( SingKind ('KProxy :: KProxy k2)
-    , SingKind ('KProxy :: KProxy k1)
-    , SDecide ('KProxy :: KProxy k2)
-    , SDecide ('KProxy :: KProxy k1)
+instance forall (f2 :: k2 -> k1 -> Type)
+  . ( SDecide k2
+    , SDecide k1
     , Dict2 Eq f2
     ) => Eq (Exinst.Some2 f2)
   where
@@ -129,13 +133,10 @@
                 case dict2 sa2x sa1x :: Dict (Eq (f2 a2x a1x)) of
                    Dict -> Just (x == y)
 
-instance forall (f3 :: k3 -> k2 -> k1 -> *)
-  . ( SingKind ('KProxy :: KProxy k3)
-    , SingKind ('KProxy :: KProxy k2)
-    , SingKind ('KProxy :: KProxy k1)
-    , SDecide ('KProxy :: KProxy k3)
-    , SDecide ('KProxy :: KProxy k2)
-    , SDecide ('KProxy :: KProxy k1)
+instance forall (f3 :: k3 -> k2 -> k1 -> Type)
+  . ( SDecide k3
+    , SDecide k2
+    , SDecide k1
     , Dict3 Eq f3
     ) => Eq (Exinst.Some3 f3)
   where
@@ -150,15 +151,11 @@
                 case dict3 sa3x sa2x sa1x :: Dict (Eq (f3 a3x a2x a1x)) of
                    Dict -> Just (x == y)
 
-instance forall (f4 :: k4 -> k3 -> k2 -> k1 -> *)
-  . ( SingKind ('KProxy :: KProxy k4)
-    , SingKind ('KProxy :: KProxy k3)
-    , SingKind ('KProxy :: KProxy k2)
-    , SingKind ('KProxy :: KProxy k1)
-    , SDecide ('KProxy :: KProxy k4)
-    , SDecide ('KProxy :: KProxy k3)
-    , SDecide ('KProxy :: KProxy k2)
-    , SDecide ('KProxy :: KProxy k1)
+instance forall (f4 :: k4 -> k3 -> k2 -> k1 -> Type)
+  . ( SDecide k4
+    , SDecide k3
+    , SDecide k2
+    , SDecide k1
     , Dict4 Eq f4
     ) => Eq (Exinst.Some4 f4)
   where
@@ -177,10 +174,10 @@
 --------------------------------------------------------------------------------
 -- Ord
 
-instance forall (f1 :: k1 -> *)
-  . ( SingKind ('KProxy :: KProxy k1)
-    , SDecide ('KProxy :: KProxy k1)
-    , Ord (DemoteRep ('KProxy :: KProxy k1))
+instance forall (f1 :: k1 -> Type)
+  . ( SingKind k1
+    , SDecide k1
+    , Ord (DemoteRep k1)
     , Dict1 Ord f1
     , Eq (Exinst.Some1 f1)
     ) => Ord (Exinst.Some1 f1)
@@ -195,13 +192,13 @@
                   case dict1 sa1x :: Dict (Ord (f1 a1x)) of
                      Dict -> Just (compare x y)
 
-instance forall (f2 :: k2 -> k1 -> *)
-  . ( SingKind ('KProxy :: KProxy k2)
-    , SingKind ('KProxy :: KProxy k1)
-    , SDecide ('KProxy :: KProxy k2)
-    , SDecide ('KProxy :: KProxy k1)
-    , Ord (DemoteRep ('KProxy :: KProxy k2))
-    , Ord (DemoteRep ('KProxy :: KProxy k1))
+instance forall (f2 :: k2 -> k1 -> Type)
+  . ( SingKind k2
+    , SingKind k1
+    , SDecide k2
+    , SDecide k1
+    , Ord (DemoteRep k2)
+    , Ord (DemoteRep k1)
     , Dict2 Ord f2
     , Eq (Exinst.Some2 f2)
     ) => Ord (Exinst.Some2 f2)
@@ -218,16 +215,16 @@
                    case dict2 sa2x sa1x :: Dict (Ord (f2 a2x a1x)) of
                       Dict -> Just (compare x y)
 
-instance forall (f3 :: k3 -> k2 -> k1 -> *)
-  . ( SingKind ('KProxy :: KProxy k3)
-    , SingKind ('KProxy :: KProxy k2)
-    , SingKind ('KProxy :: KProxy k1)
-    , SDecide ('KProxy :: KProxy k3)
-    , SDecide ('KProxy :: KProxy k2)
-    , SDecide ('KProxy :: KProxy k1)
-    , Ord (DemoteRep ('KProxy :: KProxy k3))
-    , Ord (DemoteRep ('KProxy :: KProxy k2))
-    , Ord (DemoteRep ('KProxy :: KProxy k1))
+instance forall (f3 :: k3 -> k2 -> k1 -> Type)
+  . ( SingKind k3
+    , SingKind k2
+    , SingKind k1
+    , SDecide k3
+    , SDecide k2
+    , SDecide k1
+    , Ord (DemoteRep k3)
+    , Ord (DemoteRep k2)
+    , Ord (DemoteRep k1)
     , Dict3 Ord f3
     , Eq (Exinst.Some3 f3)
     ) => Ord (Exinst.Some3 f3)
@@ -246,19 +243,19 @@
                   case dict3 sa3x sa2x sa1x :: Dict (Ord (f3 a3x a2x a1x)) of
                      Dict -> Just (compare x y)
 
-instance forall (f4 :: k4 -> k3 -> k2 -> k1 -> *)
-  . ( SingKind ('KProxy :: KProxy k4)
-    , SingKind ('KProxy :: KProxy k3)
-    , SingKind ('KProxy :: KProxy k2)
-    , SingKind ('KProxy :: KProxy k1)
-    , SDecide ('KProxy :: KProxy k4)
-    , SDecide ('KProxy :: KProxy k3)
-    , SDecide ('KProxy :: KProxy k2)
-    , SDecide ('KProxy :: KProxy k1)
-    , Ord (DemoteRep ('KProxy :: KProxy k4))
-    , Ord (DemoteRep ('KProxy :: KProxy k3))
-    , Ord (DemoteRep ('KProxy :: KProxy k2))
-    , Ord (DemoteRep ('KProxy :: KProxy k1))
+instance forall (f4 :: k4 -> k3 -> k2 -> k1 -> Type)
+  . ( SingKind k4
+    , SingKind k3
+    , SingKind k2
+    , SingKind k1
+    , SDecide k4
+    , SDecide k3
+    , SDecide k2
+    , SDecide k1
+    , Ord (DemoteRep k4)
+    , Ord (DemoteRep k3)
+    , Ord (DemoteRep k2)
+    , Ord (DemoteRep k1)
     , Dict4 Ord f4
     , Eq (Exinst.Some4 f4)
     ) => Ord (Exinst.Some4 f4)
@@ -277,3 +274,12 @@
                   Refl <- testEquality sa1x sa1y
                   case dict4 sa4x sa3x sa2x sa1x :: Dict (Ord (f4 a4x a3x a2x a1x)) of
                      Dict -> Just (compare x y)
+
+--------------------------------------------------------------------------------
+--------------------------------------------------------------------------------
+-- Out of the box 'Dict1' instances for some @base@ types
+
+instance (c (f 'True), c (f 'False)) => Dict1 c (f :: Bool -> k0) where
+  dict1 = \case
+    STrue -> Dict
+    SFalse -> Dict
diff --git a/src/lib/Exinst/Singletons.hs b/src/lib/Exinst/Singletons.hs
--- a/src/lib/Exinst/Singletons.hs
+++ b/src/lib/Exinst/Singletons.hs
@@ -6,39 +6,48 @@
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
 
 -- | See the README file for documentation: https://hackage.haskell.org/package/exinst#readme
 module Exinst.Singletons
  ( -- * 1 type index
    Some1(Some1)
  , some1
- , withSome1Sing
- , withSome1
  , fromSome1
+ , _Some1
+ , withSome1
+ , withSome1Sing
+ , some1SingRep
  , Dict1(dict1)
 
    -- * 2 type indexes
  , Some2(Some2)
  , some2
- , withSome2Sing
- , withSome2
  , fromSome2
+ , _Some2
+ , withSome2
+ , withSome2Sing
+ , some2SingRep
  , Dict2(dict2)
 
    -- * 3 type indexes
  , Some3(Some3)
  , some3
- , withSome3Sing
- , withSome3
  , fromSome3
+ , _Some3
+ , withSome3
+ , withSome3Sing
+ , some3SingRep
  , Dict3(dict3)
 
    -- * 4 type indexes
  , Some4(Some4)
  , some4
- , withSome4Sing
- , withSome4
  , fromSome4
+ , _Some4
+ , withSome4
+ , withSome4Sing
+ , some4SingRep
  , Dict4(dict4)
 
    -- * Re-exports
@@ -46,6 +55,8 @@
  ) where
 
 import Data.Constraint
+import Data.Kind (Type)
+import Data.Profunctor (dimap, Choice(right'))
 import Data.Singletons
 import Data.Singletons.Decide
 import Data.Type.Equality
@@ -53,22 +64,22 @@
 
 --------------------------------------------------------------------------------
 
-data Some1 (f1 :: k1 -> *) = forall a1.
+data Some1 (f1 :: k1 -> Type) = forall a1.
   Some1 !(Sing a1) !(f1 a1)
 
-data Some2 (f2 :: k2 -> k1 -> *) = forall a2 a1.
+data Some2 (f2 :: k2 -> k1 -> Type) = forall a2 a1.
   Some2 !(Sing a2) !(Sing a1) !(f2 a2 a1)
 
-data Some3 (f3 :: k3 -> k2 -> k1 -> *) = forall a3 a2 a1.
+data Some3 (f3 :: k3 -> k2 -> k1 -> Type) = forall a3 a2 a1.
   Some3 !(Sing a3) !(Sing a2) !(Sing a1) !(f3 a3 a2 a1)
 
-data Some4 (f4 :: k4 -> k3 -> k2 -> k1 -> *) = forall a4 a3 a2 a1.
+data Some4 (f4 :: k4 -> k3 -> k2 -> k1 -> Type) = forall a4 a3 a2 a1.
   Some4 !(Sing a4) !(Sing a3) !(Sing a2) !(Sing a1) !(f4 a4 a3 a2 a1)
 
 --------------------------------------------------------------------------------
 
 some1
-  :: forall (f1 :: k1 -> *) a1
+  :: forall (f1 :: k1 -> Type) a1
   .  SingI a1
   => f1 a1
   -> Some1 f1 -- ^
@@ -76,7 +87,7 @@
 {-# INLINE some1 #-}
 
 some2
-  :: forall (f2 :: k2 -> k1 -> *) a2 a1
+  :: forall (f2 :: k2 -> k1 -> Type) a2 a1
   .  (SingI a2, SingI a1)
   => f2 a2 a1
   -> Some2 f2 -- ^
@@ -84,7 +95,7 @@
 {-# INLINE some2 #-}
 
 some3
-  :: forall (f3 :: k3 -> k2 -> k1 -> *) a3 a2 a1
+  :: forall (f3 :: k3 -> k2 -> k1 -> Type) a3 a2 a1
   .  (SingI a3, SingI a2, SingI a1)
   => f3 a3 a2 a1
   -> Some3 f3 -- ^
@@ -92,7 +103,7 @@
 {-# INLINE some3 #-}
 
 some4
-  :: forall (f4 :: k4 -> k3 -> k2 -> k1 -> *) a4 a3 a2 a1
+  :: forall (f4 :: k4 -> k3 -> k2 -> k1 -> Type) a4 a3 a2 a1
   .  (SingI a4, SingI a3, SingI a2, SingI a1)
   => f4 a4 a3 a2 a1
   -> Some4 f4 -- ^
@@ -103,7 +114,7 @@
 --------------------------------------------------------------------------------
 
 withSome1
-  :: forall (f1 :: k1 -> *) (r :: *)
+  :: forall (f1 :: k1 -> Type) (r :: Type)
    . Some1 f1
   -> (forall a1. SingI a1 => f1 a1 -> r)
   -> r -- ^
@@ -111,7 +122,7 @@
 {-# INLINABLE withSome1 #-}
 
 withSome2
-  :: forall (f2 :: k2 -> k1 -> *) (r :: *)
+  :: forall (f2 :: k2 -> k1 -> Type) (r :: Type)
   .  Some2 f2
   -> (forall a2 a1. (SingI a2, SingI a1) => f2 a2 a1 -> r)
   -> r -- ^
@@ -119,7 +130,7 @@
 {-# INLINABLE withSome2 #-}
 
 withSome3
-  :: forall (f3 :: k3 -> k2 -> k1 -> *) (r :: *)
+  :: forall (f3 :: k3 -> k2 -> k1 -> Type) (r :: Type)
   .  Some3 f3
   -> (forall a3 a2 a1. (SingI a3, SingI a2, SingI a1) => f3 a3 a2 a1 -> r)
   -> r -- ^
@@ -127,7 +138,7 @@
 {-# INLINABLE withSome3 #-}
 
 withSome4
-  :: forall (f4 :: k4 -> k3 -> k2 -> k1 -> *) (r :: *)
+  :: forall (f4 :: k4 -> k3 -> k2 -> k1 -> Type) (r :: Type)
   .  Some4 f4
   -> (forall a4 a3 a2 a1
         .  (SingI a4, SingI a3, SingI a2, SingI a1)
@@ -140,7 +151,7 @@
 
 -- | Like 'withSome1', but takes an explicit 'Sing' besides the 'SingI' instance.
 withSome1Sing
-  :: forall (f1 :: k1 -> *) (r :: *)
+  :: forall (f1 :: k1 -> Type) (r :: Type)
    . Some1 f1
   -> (forall a1. (SingI a1) => Sing a1 -> f1 a1 -> r)
   -> r -- ^
@@ -149,7 +160,7 @@
 
 -- | Like 'withSome2', but takes explicit 'Sing's besides the 'SingI' instances.
 withSome2Sing
-  :: forall (f2 :: k2 -> k1 -> *) (r :: *)
+  :: forall (f2 :: k2 -> k1 -> Type) (r :: Type)
   .  Some2 f2
   -> (forall a2 a1. (SingI a2, SingI a1) => Sing a2 -> Sing a1 -> f2 a2 a1 -> r)
   -> r -- ^
@@ -158,7 +169,7 @@
 
 -- | Like 'withSome3', but takes explicit 'Sing's besides the 'SingI' instances.
 withSome3Sing
-  :: forall (f3 :: k3 -> k2 -> k1 -> *) (r :: *)
+  :: forall (f3 :: k3 -> k2 -> k1 -> Type) (r :: Type)
   .  Some3 f3
   -> (forall a3 a2 a1
          .  (SingI a3, SingI a2, SingI a1)
@@ -170,7 +181,7 @@
 
 -- | Like 'withSome4', but takes explicit 'Sing's besides the 'SingI' instances.
 withSome4Sing
-  :: forall (f4 :: k4 -> k3 -> k2 -> k1 -> *) (r :: *)
+  :: forall (f4 :: k4 -> k3 -> k2 -> k1 -> Type) (r :: Type)
   .  Some4 f4
   -> (forall a4 a3 a2 a1
         .  (SingI a4, SingI a3, SingI a2, SingI a1)
@@ -184,8 +195,8 @@
 --------------------------------------------------------------------------------
 
 fromSome1
-   :: forall (f1 :: k1 -> *) a1
-    . (SingI a1, SDecide ('KProxy :: KProxy k1))
+   :: forall (f1 :: k1 -> Type) a1
+    . (SingI a1, SDecide k1)
    => Some1 f1
    -> Maybe (f1 a1) -- ^
 fromSome1 = \(Some1 sa1' x) -> do
@@ -194,9 +205,9 @@
 {-# INLINABLE fromSome1 #-}
 
 fromSome2
-   :: forall (f2 :: k2 -> k1 -> *) a2 a1
-    . ( SingI a2, SDecide ('KProxy :: KProxy k2)
-      , SingI a1, SDecide ('KProxy :: KProxy k1))
+   :: forall (f2 :: k2 -> k1 -> Type) a2 a1
+    . ( SingI a2, SDecide k2
+      , SingI a1, SDecide k1 )
    => Some2 f2
    -> Maybe (f2 a2 a1) -- ^
 fromSome2 = \(Some2 sa2' sa1' x) -> do
@@ -206,10 +217,10 @@
 {-# INLINABLE fromSome2 #-}
 
 fromSome3
-   :: forall (f3 :: k3 -> k2 -> k1 -> *) a3 a2 a1
-    . ( SingI a3, SDecide ('KProxy :: KProxy k3)
-      , SingI a2, SDecide ('KProxy :: KProxy k2)
-      , SingI a1, SDecide ('KProxy :: KProxy k1))
+   :: forall (f3 :: k3 -> k2 -> k1 -> Type) a3 a2 a1
+    . ( SingI a3, SDecide k3
+      , SingI a2, SDecide k2
+      , SingI a1, SDecide k1 )
    => Some3 f3
    -> Maybe (f3 a3 a2 a1) -- ^
 fromSome3 = \(Some3 sa3' sa2' sa1' x) -> do
@@ -220,11 +231,11 @@
 {-# INLINABLE fromSome3 #-}
 
 fromSome4
-   :: forall (f4 :: k4 -> k3 -> k2 -> k1 -> *) a4 a3 a2 a1
-    . ( SingI a4, SDecide ('KProxy :: KProxy k4)
-      , SingI a3, SDecide ('KProxy :: KProxy k3)
-      , SingI a2, SDecide ('KProxy :: KProxy k2)
-      , SingI a1, SDecide ('KProxy :: KProxy k1))
+   :: forall (f4 :: k4 -> k3 -> k2 -> k1 -> Type) a4 a3 a2 a1
+    . ( SingI a4, SDecide k4
+      , SingI a3, SDecide k3
+      , SingI a2, SDecide k2
+      , SingI a1, SDecide k1 )
    => Some4 f4
    -> Maybe (f4 a4 a3 a2 a1) -- ^
 fromSome4 = \(Some4 sa4' sa3' sa2' sa1' x) -> do
@@ -237,14 +248,106 @@
 
 --------------------------------------------------------------------------------
 
+-- A @lens@-compatible 'Prism'' for constructing and deconstructing a 'Some1'.
+_Some1
+  :: forall (f1 :: k1 -> Type) a1
+  .  (SingI a1, SDecide k1)
+  => Prism' (Some1 f1) (f1 a1)
+_Some1 = prism' some1 fromSome1
+{-# INLINE _Some1 #-}
+
+-- A @lens@-compatible 'Prism'' for constructing and deconstructing a 'Some2'.
+_Some2
+  :: forall (f2 :: k2 -> k1 -> Type) a2 a1
+  .  ( SingI a2, SDecide k2
+     , SingI a1, SDecide k1 )
+  => Prism' (Some2 f2) (f2 a2 a1)
+_Some2 = prism' some2 fromSome2
+{-# INLINE _Some2 #-}
+
+-- A @lens@-compatible 'Prism'' for constructing and deconstructing a 'Some3'.
+_Some3
+  :: forall (f3 :: k3 -> k2 -> k1 -> Type) a3 a2 a1
+  .  ( SingI a3, SDecide k3
+     , SingI a2, SDecide k2
+     , SingI a1, SDecide k1 )
+  => Prism' (Some3 f3) (f3 a3 a2 a1)
+_Some3 = prism' some3 fromSome3
+{-# INLINE _Some3 #-}
+
+-- A @lens@-compatible 'Prism'' for constructing and deconstructing a 'Some4'.
+_Some4
+  :: forall (f4 :: k4 -> k3 -> k2 -> k1 -> Type) a4 a3 a2 a1
+  .  ( SingI a4, SDecide k4
+     , SingI a3, SDecide k3
+     , SingI a2, SDecide k2
+     , SingI a1, SDecide k1 )
+  => Prism' (Some4 f4) (f4 a4 a3 a2 a1)
+_Some4 = prism' some4 fromSome4
+{-# INLINE _Some4 #-}
+
+--------------------------------------------------------------------------------
+
+some1SingRep
+  :: SingKind k1
+  => Some1 (f1 :: k1 -> Type)
+  -> DemoteRep k1 -- ^
+some1SingRep = \(Some1 sa1 _) -> fromSing sa1
+{-# INLINE some1SingRep #-}
+
+some2SingRep
+  :: (SingKind k2, SingKind k1)
+  => Some2 (f2 :: k2 -> k1 -> Type)
+  -> (DemoteRep k2, DemoteRep k1) -- ^
+some2SingRep = \(Some2 sa2 sa1 _) -> (fromSing sa2, fromSing sa1)
+{-# INLINE some2SingRep #-}
+
+some3SingRep
+  :: (SingKind k3, SingKind k2, SingKind k1)
+  => Some3 (f3 :: k3 -> k2 -> k1 -> Type)
+  -> (DemoteRep k3, DemoteRep k2, DemoteRep k1) -- ^
+some3SingRep = \(Some3 sa3 sa2 sa1 _) ->
+  (fromSing sa3, fromSing sa2, fromSing sa1)
+{-# INLINE some3SingRep #-}
+
+some4SingRep
+  :: (SingKind k4, SingKind k3, SingKind k2, SingKind k1)
+  => Some4 (f4 :: k4 -> k3 -> k2 -> k1 -> Type)
+  -> (DemoteRep k4, DemoteRep k3, DemoteRep k2, DemoteRep k1) -- ^
+some4SingRep = \(Some4 sa4 sa3 sa2 sa1 _) ->
+  (fromSing sa4, fromSing sa3, fromSing sa2, fromSing sa1)
+{-# INLINE some4SingRep #-}
+
+--------------------------------------------------------------------------------
+
 class Dict1 (c :: k0 -> Constraint) (f1 :: k1 -> k0) where
+  -- | Runtime lookup of the @c (f1 a1)@ instance.
   dict1 :: Sing a1 -> Dict (c (f1 a1))
 
 class Dict2 (c :: k0 -> Constraint) (f2 :: k2 -> k1 -> k0) where
+  -- Runtime lookup of the @c (f2 a2 a1)@ instance.
   dict2 :: Sing a2 -> Sing a1 -> Dict (c (f2 a2 a1))
 
 class Dict3 (c :: k0 -> Constraint) (f3 :: k3 -> k2 -> k1 -> k0) where
+  -- Runtime lookup of the @c (f3 a3 a2 a1)@ instance.
   dict3 :: Sing a3 -> Sing a2 -> Sing a1 -> Dict (c (f3 a3 a2 a1))
 
 class Dict4 (c :: k0 -> Constraint) (f4 :: k4 -> k3 -> k2 -> k1 -> k0) where
+  -- Runtime lookup of the @c (f4 a4 a3 a2 a1)@ instance.
   dict4 :: Sing a4 -> Sing a3 -> Sing a2 -> Sing a1 -> Dict (c (f4 a4 a3 a2 a1))
+
+--------------------------------------------------------------------------------
+-- Miscelaneous @lens@-compatible stuff.
+
+type Prism s t a b
+  = forall p f. (Choice p, Applicative f) => p a (f b) -> p s (f t)
+
+type Prism' s a = Prism s s a a
+
+prism :: (b -> t) -> (s -> Either t a) -> Prism s t a b
+prism bt seta = dimap seta (either pure (fmap bt)) . right'
+{-# INLINE prism #-}
+
+prism' :: (b -> s) -> (s -> Maybe a) -> Prism s s a b
+prism' bs sma = prism bs (\s -> maybe (Left s) Right (sma s))
+{-# INLINE prism' #-}