exinst 0.1.2 → 0.2

raw patch · 4 files changed

+246/−123 lines, 4 filesdep +profunctorsdep ~basedep ~singletonsPVP ok

version bump matches the API change (PVP)

Dependencies added: profunctors

Dependency ranges changed: base, singletons

API changes (from Hackage documentation)

Files

• CHANGELOG.md +13/−0
• exinst.cabal +4/−3
• src/lib/Exinst/Instances/Base.hs +88/−82
• src/lib/Exinst/Singletons.hs +141/−38

@@ -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.

@@ -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

@@ -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

@@ -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' #-}