exinst 0.7 → 0.8
raw patch · 8 files changed
+111/−107 lines, 8 filesdep ~singletonssetup-changed
Dependency ranges changed: singletons
Files
- CHANGELOG.md +4/−0
- Setup.hs +0/−2
- exinst.cabal +4/−4
- lib/Exinst/Base.hs +43/−44
- lib/Exinst/Binary.hs +4/−4
- lib/Exinst/DeepSeq.hs +4/−4
- lib/Exinst/Hashable.hs +4/−4
- lib/Exinst/Internal.hs +48/−45
CHANGELOG.md view
@@ -1,3 +1,7 @@+# Version 0.8++* Builds with GHC 8.10 and `singletons-2.7`.+ # Version 0.7 * BACKWARDS COMPATIBLE COMPILER ASSISTED CHANGE: All of the cabal flags
− Setup.hs
@@ -1,2 +0,0 @@-import Distribution.Simple-main = defaultMain
exinst.cabal view
@@ -1,8 +1,8 @@ name: exinst-version: 0.7+version: 0.8 author: Renzo Carbonara-maintainer: renzoλcarbonara.com.ar-copyright: Renzo Carbonara 2015-2018+maintainer: renλren!zone+copyright: Renzo Carbonara 2015 license: BSD3 license-file: LICENSE.txt extra-source-files: README.md CHANGELOG.md@@ -35,7 +35,7 @@ , deepseq , hashable , profunctors >=5.0- , singletons >=2.3.1+ , singletons >=2.6 , QuickCheck ghcjs-options: -Wall -O3 ghc-options: -Wall -O2
lib/Exinst/Base.hs view
@@ -23,11 +23,10 @@ import Data.Kind (Type) import Data.Singletons import Data.Singletons.Prelude.Enum (PEnum(EnumFromTo), PBounded(MinBound, MaxBound))-import Data.Singletons.Prelude.Bool (Sing(STrue,SFalse))+import Data.Singletons.Prelude.Bool (SBool(STrue, SFalse)) import qualified Data.Singletons.Prelude.List as List import Data.Singletons.Prelude.Tuple (Tuple2Sym1) import Data.Singletons.Decide-import Data.Type.Equality import qualified GHC.Generics as G import Prelude import qualified Text.Read as Read@@ -45,7 +44,7 @@ data Some3'Show r3 r2 r1 x = Some3 r3 r2 r1 x deriving (Show) data Some4'Show r4 r3 r2 r1 x = Some4 r4 r3 r2 r1 x deriving (Show) -instance forall (f :: k1 -> Type)+instance forall k1 (f :: k1 -> Type) . ( SingKind k1 , Show (Demote k1) , Dict1 Show f@@ -56,7 +55,7 @@ case dict1 sa1 :: Dict (Show (f a1)) of Dict -> showsPrec n (Some1 (fromSing sa1) x) -instance forall (f :: k2 -> k1 -> Type)+instance forall k2 k1 (f :: k2 -> k1 -> Type) . ( SingKind k2 , SingKind k1 , Show (Demote k2)@@ -69,7 +68,7 @@ case dict2 sa2 sa1 :: Dict (Show (f a2 a1)) of Dict -> showsPrec n (Some2 (fromSing sa2) (fromSing sa1) x) -instance forall (f :: k3 -> k2 -> k1 -> Type)+instance forall k3 k2 k1 (f :: k3 -> k2 -> k1 -> Type) . ( SingKind k3 , SingKind k2 , SingKind k1@@ -84,7 +83,7 @@ case dict3 sa3 sa2 sa1 :: Dict (Show (f a3 a2 a1)) of Dict -> showsPrec n (Some3 (fromSing sa3) (fromSing sa2) (fromSing sa1) x) -instance forall (f :: k4 -> k3 -> k2 -> k1 -> Type)+instance forall k4 k3 k2 k1 (f :: k4 -> k3 -> k2 -> k1 -> Type) . ( SingKind k4 , SingKind k3 , SingKind k2@@ -105,7 +104,7 @@ -------------------------------------------------------------------------------- -- Read -instance forall (f :: k1 -> Type)+instance forall k1 (f :: k1 -> Type) . ( SingKind k1 , Read (Demote k1) , Dict1 Read f@@ -121,7 +120,7 @@ x :: f a1 <- Read.readPrec pure (Exinst.Some1 sa1 x) -instance forall (f :: k2 -> k1 -> Type)+instance forall k2 k1 (f :: k2 -> k1 -> Type) . ( SingKind k2 , SingKind k1 , Read (Demote k2)@@ -141,7 +140,7 @@ x :: f a2 a1 <- Read.readPrec pure (Exinst.Some2 sa2 sa1 x) -instance forall (f :: k3 -> k2 -> k1 -> Type)+instance forall k3 k2 k1 (f :: k3 -> k2 -> k1 -> Type) . ( SingKind k3 , SingKind k2 , SingKind k1@@ -165,7 +164,7 @@ x :: f a3 a2 a1 <- Read.readPrec pure (Exinst.Some3 sa3 sa2 sa1 x) -instance forall (f :: k4 -> k3 -> k2 -> k1 -> Type)+instance forall k4 k3 k2 k1 (f :: k4 -> k3 -> k2 -> k1 -> Type) . ( SingKind k4 , SingKind k3 , SingKind k2@@ -196,7 +195,7 @@ -------------------------------------------------------------------------------- -- Eq -instance forall (f :: k1 -> Type).+instance forall k1 (f :: k1 -> Type). ( SDecide k1 , Dict1 Eq f ) => Eq (Exinst.Some1 f)@@ -206,11 +205,11 @@ withSome1Sing som1x $ \sa1x (x :: f a1x) -> withSome1Sing som1y $ \sa1y (y :: f a1y) -> maybe False id $ do- Refl <- testEquality sa1x sa1y+ Refl <- decideEquality sa1x sa1y case dict1 sa1x :: Dict (Eq (f a1x)) of Dict -> Just (x == y) -instance forall (f :: k2 -> k1 -> Type)+instance forall k2 k1 (f :: k2 -> k1 -> Type) . ( SDecide k2 , SDecide k1 , Dict2 Eq f@@ -221,12 +220,12 @@ withSome2Sing som2x $ \sa2x sa1x (x :: f a2x a1x) -> withSome2Sing som2y $ \sa2y sa1y (y :: f a2y a1y) -> maybe False id $ do- Refl <- testEquality sa2x sa2y- Refl <- testEquality sa1x sa1y+ Refl <- decideEquality sa2x sa2y+ Refl <- decideEquality sa1x sa1y case dict2 sa2x sa1x :: Dict (Eq (f a2x a1x)) of Dict -> Just (x == y) -instance forall (f :: k3 -> k2 -> k1 -> Type)+instance forall k3 k2 k1 (f :: k3 -> k2 -> k1 -> Type) . ( SDecide k3 , SDecide k2 , SDecide k1@@ -238,13 +237,13 @@ withSome3Sing som3x $ \sa3x sa2x sa1x (x :: f a3x a2x a1x) -> withSome3Sing som3y $ \sa3y sa2y sa1y (y :: f a3y a2y a1y) -> maybe False id $ do- Refl <- testEquality sa3x sa3y- Refl <- testEquality sa2x sa2y- Refl <- testEquality sa1x sa1y+ Refl <- decideEquality sa3x sa3y+ Refl <- decideEquality sa2x sa2y+ Refl <- decideEquality sa1x sa1y case dict3 sa3x sa2x sa1x :: Dict (Eq (f a3x a2x a1x)) of Dict -> Just (x == y) -instance forall (f :: k4 -> k3 -> k2 -> k1 -> Type)+instance forall k4 k3 k2 k1 (f :: k4 -> k3 -> k2 -> k1 -> Type) . ( SDecide k4 , SDecide k3 , SDecide k2@@ -257,17 +256,17 @@ withSome4Sing som4x $ \sa4x sa3x sa2x sa1x (x :: f a4x a3x a2x a1x) -> withSome4Sing som4y $ \sa4y sa3y sa2y sa1y (y :: f a4y a3y a2y a1y) -> maybe False id $ do- Refl <- testEquality sa4x sa4y- Refl <- testEquality sa3x sa3y- Refl <- testEquality sa2x sa2y- Refl <- testEquality sa1x sa1y+ Refl <- decideEquality sa4x sa4y+ Refl <- decideEquality sa3x sa3y+ Refl <- decideEquality sa2x sa2y+ Refl <- decideEquality sa1x sa1y case dict4 sa4x sa3x sa2x sa1x :: Dict (Eq (f a4x a3x a2x a1x)) of Dict -> Just (x == y) -------------------------------------------------------------------------------- -- Ord -instance forall (f :: k1 -> Type)+instance forall k1 (f :: k1 -> Type) . ( SingKind k1 , SDecide k1 , Ord (Demote k1)@@ -281,11 +280,11 @@ withSome1Sing som1y $ \sa1y (y :: f a1y) -> let termCompare = compare (fromSing sa1x) (fromSing sa1y) in maybe termCompare id $ do- Refl <- testEquality sa1x sa1y+ Refl <- decideEquality sa1x sa1y case dict1 sa1x :: Dict (Ord (f a1x)) of Dict -> Just (compare x y) -instance forall (f :: k2 -> k1 -> Type)+instance forall k2 k1 (f :: k2 -> k1 -> Type) . ( SingKind k2 , SingKind k1 , SDecide k2@@ -303,12 +302,12 @@ let termCompare = compare (fromSing sa2x, fromSing sa1x) (fromSing sa2y, fromSing sa1y) in maybe termCompare id $ do- Refl <- testEquality sa2x sa2y- Refl <- testEquality sa1x sa1y+ Refl <- decideEquality sa2x sa2y+ Refl <- decideEquality sa1x sa1y case dict2 sa2x sa1x :: Dict (Ord (f a2x a1x)) of Dict -> Just (compare x y) -instance forall (f :: k3 -> k2 -> k1 -> Type)+instance forall k3 k2 k1 (f :: k3 -> k2 -> k1 -> Type) . ( SingKind k3 , SingKind k2 , SingKind k1@@ -330,13 +329,13 @@ (fromSing sa3x, fromSing sa2x, fromSing sa1x) (fromSing sa3y, fromSing sa2y, fromSing sa1y) in maybe termCompare id $ do- Refl <- testEquality sa3x sa3y- Refl <- testEquality sa2x sa2y- Refl <- testEquality sa1x sa1y+ Refl <- decideEquality sa3x sa3y+ Refl <- decideEquality sa2x sa2y+ Refl <- decideEquality sa1x sa1y case dict3 sa3x sa2x sa1x :: Dict (Ord (f a3x a2x a1x)) of Dict -> Just (compare x y) -instance forall (f :: k4 -> k3 -> k2 -> k1 -> Type)+instance forall k4 k3 k2 k1 (f :: k4 -> k3 -> k2 -> k1 -> Type) . ( SingKind k4 , SingKind k3 , SingKind k2@@ -361,10 +360,10 @@ (fromSing sa4x, fromSing sa3x, fromSing sa2x, fromSing sa1x) (fromSing sa4y, fromSing sa3y, fromSing sa2y, fromSing sa1y) in maybe termCompare id $ do- Refl <- testEquality sa4x sa4y- Refl <- testEquality sa3x sa3y- Refl <- testEquality sa2x sa2y- Refl <- testEquality sa1x sa1y+ Refl <- decideEquality sa4x sa4y+ Refl <- decideEquality sa3x sa3y+ Refl <- decideEquality sa2x sa2y+ Refl <- decideEquality sa1x sa1y case dict4 sa4x sa3x sa2x sa1x :: Dict (Ord (f a4x a3x a2x a1x)) of Dict -> Just (compare x y) @@ -523,7 +522,7 @@ , Cartesian4 xs4 xs3 xs2 xs1 ] -instance forall k3 k2 k1 (f :: k4 -> k3 -> k2 -> k1 -> Type)+instance forall k4 k3 k2 k1 (f :: k4 -> k3 -> k2 -> k1 -> Type) . ( SingKind k4 , SingKind k3 , SingKind k2@@ -566,31 +565,31 @@ -------------------------------------------------------------------------------- -- Out of the box 'DictX' instances for some @base@ types -instance+instance forall c. (c 'False, c 'True ) => Dict0 (c :: Bool -> Constraint) where {-# INLINABLE dict0 #-} dict0 = \case { SFalse -> Dict; STrue -> Dict } -instance+instance forall k0 c f. ( c (f 'False), c (f 'True) ) => Dict1 c (f :: Bool -> k0) where {-# INLINABLE dict1 #-} dict1 = \case { SFalse -> Dict; STrue -> Dict } -instance+instance forall k1 k0 c f. ( Dict1 c (f 'False), Dict1 c (f 'True) ) => Dict2 c (f :: Bool -> k1 -> k0) where {-# INLINABLE dict2 #-} dict2 = \x -> case x of { SFalse -> dict1; STrue -> dict1 } -instance+instance forall k2 k1 k0 c f. ( Dict2 c (f 'False), Dict2 c (f 'True) ) => Dict3 c (f :: Bool -> k2 -> k1 -> k0) where {-# INLINABLE dict3 #-} dict3 = \x -> case x of { SFalse -> dict2; STrue -> dict2 } -instance+instance forall k3 k2 k1 k0 c f. ( Dict3 c (f 'False), Dict3 c (f 'True) ) => Dict4 c (f :: Bool -> k3 -> k2 -> k1 -> k0) where {-# INLINABLE dict4 #-}
lib/Exinst/Binary.hs view
@@ -29,7 +29,7 @@ -- | Compatible with the 'Data.Bytes.Serial.Serial' instance and -- 'Data.Serialize.Serialize' instance, provided all of the 'Demote's and the -- fully applied @f@ instances are compatible as well.-instance forall (f :: k1 -> Type).+instance forall k1 (f :: k1 -> Type). ( SingKind k1 , Bin.Binary (Demote k1) , Dict1 Bin.Binary f@@ -53,7 +53,7 @@ -- | Compatible with the 'Data.Bytes.Serial.Serial' instance and -- 'Data.Serialize.Serialize' instance, provided all of the 'Demote's and the -- fully applied @f@ instances are compatible as well.-instance forall (f :: k2 -> k1 -> Type).+instance forall k2 k1 (f :: k2 -> k1 -> Type). ( SingKind k2 , SingKind k1 , Bin.Binary (Demote k2)@@ -80,7 +80,7 @@ -- | Compatible with the 'Data.Bytes.Serial.Serial' instance and -- 'Data.Serialize.Serialize' instance, provided all of the 'Demote's and the -- fully applied @f@ instances are compatible as well.-instance forall (f :: k3 -> k2 -> k1 -> Type).+instance forall k3 k2 k1 (f :: k3 -> k2 -> k1 -> Type). ( SingKind k3 , SingKind k2 , SingKind k1@@ -110,7 +110,7 @@ -- | Compatible with the 'Data.Bytes.Serial.Serial' instance and -- 'Data.Serialize.Serialize' instance, provided all of the 'Demote's and the -- fully applied @f@ instances are compatible as well.-instance forall (f :: k4 -> k3 -> k2 -> k1 -> Type).+instance forall k4 k3 k2 k1 (f :: k4 -> k3 -> k2 -> k1 -> Type). ( SingKind k4 , SingKind k3 , SingKind k2
lib/Exinst/DeepSeq.hs view
@@ -24,7 +24,7 @@ -------------------------------------------------------------------------------- -instance forall (f :: k1 -> *).+instance forall k1 (f :: k1 -> *). ( Dict1 NFData f ) => NFData (Some1 f) where {-# INLINABLE rnf #-}@@ -33,7 +33,7 @@ case dict1 sa1 :: Dict (NFData (f a1)) of Dict -> rnf x `seq` () -instance forall (f :: k2 -> k1 -> *).+instance forall k2 k1 (f :: k2 -> k1 -> *). ( Dict2 NFData f ) => NFData (Some2 f) where {-# INLINABLE rnf #-}@@ -42,7 +42,7 @@ case dict2 sa2 sa1 :: Dict (NFData (f a2 a1)) of Dict -> rnf x `seq` () -instance forall (f :: k3 -> k2 -> k1 -> *).+instance forall k3 k2 k1 (f :: k3 -> k2 -> k1 -> *). ( Dict3 NFData f ) => NFData (Some3 f) where {-# INLINABLE rnf #-}@@ -51,7 +51,7 @@ case dict3 sa3 sa2 sa1 :: Dict (NFData (f a3 a2 a1)) of Dict -> rnf x `seq` () -instance forall (f :: k4 -> k3 -> k2 -> k1 -> *).+instance forall k4 k3 k2 k1 (f :: k4 -> k3 -> k2 -> k1 -> *). ( Dict4 NFData f ) => NFData (Some4 f) where {-# INLINABLE rnf #-}
lib/Exinst/Hashable.hs view
@@ -32,7 +32,7 @@ -------------------------------------------------------------------------------- -instance forall (f :: k1 -> Type)+instance forall k1 (f :: k1 -> Type) . ( SingKind k1 , Hashable (Demote k1) , Dict1 Hashable f@@ -45,7 +45,7 @@ `hashWithSalt` fromSing sa1 `hashWithSalt` x -instance forall (f :: k2 -> k1 -> Type)+instance forall k2 k1 (f :: k2 -> k1 -> Type) . ( SingKind k2 , SingKind k1 , Hashable (Demote k2)@@ -61,7 +61,7 @@ `hashWithSalt` fromSing sa1 `hashWithSalt` x -instance forall (f :: k3 -> k2 -> k1 -> Type)+instance forall k3 k2 k1 (f :: k3 -> k2 -> k1 -> Type) . ( SingKind k3 , SingKind k2 , SingKind k1@@ -80,7 +80,7 @@ `hashWithSalt` fromSing sa1 `hashWithSalt` x -instance forall (f :: k4 -> k3 -> k2 -> k1 -> Type)+instance forall k4 k3 k2 k1 (f :: k4 -> k3 -> k2 -> k1 -> Type) . ( SingKind k4 , SingKind k3 , SingKind k2
lib/Exinst/Internal.hs view
@@ -63,7 +63,6 @@ import Data.Profunctor (dimap, Choice(right')) import Data.Singletons import Data.Singletons.Decide-import Data.Type.Equality import Prelude --------------------------------------------------------------------------------@@ -83,7 +82,7 @@ -------------------------------------------------------------------------------- some1- :: forall (f1 :: k1 -> Type) a1+ :: forall k1 (f1 :: k1 -> Type) a1 . SingI a1 => f1 a1 -> Some1 f1 -- ^@@ -91,7 +90,7 @@ {-# INLINE some1 #-} some2- :: forall (f2 :: k2 -> k1 -> Type) a2 a1+ :: forall k2 k1 (f2 :: k2 -> k1 -> Type) a2 a1 . (SingI a2, SingI a1) => f2 a2 a1 -> Some2 f2 -- ^@@ -99,7 +98,7 @@ {-# INLINE some2 #-} some3- :: forall (f3 :: k3 -> k2 -> k1 -> Type) a3 a2 a1+ :: forall k3 k2 k1 (f3 :: k3 -> k2 -> k1 -> Type) a3 a2 a1 . (SingI a3, SingI a2, SingI a1) => f3 a3 a2 a1 -> Some3 f3 -- ^@@ -107,7 +106,7 @@ {-# INLINE some3 #-} some4- :: forall (f4 :: k4 -> k3 -> k2 -> k1 -> Type) a4 a3 a2 a1+ :: forall k4 k3 k2 k1 (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 -- ^@@ -118,7 +117,7 @@ -------------------------------------------------------------------------------- withSome1- :: forall (f1 :: k1 -> Type) (r :: Type)+ :: forall k1 (f1 :: k1 -> Type) (r :: Type) . Some1 f1 -> (forall a1. SingI a1 => f1 a1 -> r) -> r -- ^@@ -126,7 +125,7 @@ {-# INLINABLE withSome1 #-} withSome2- :: forall (f2 :: k2 -> k1 -> Type) (r :: Type)+ :: forall k2 k1 (f2 :: k2 -> k1 -> Type) (r :: Type) . Some2 f2 -> (forall a2 a1. (SingI a2, SingI a1) => f2 a2 a1 -> r) -> r -- ^@@ -134,7 +133,7 @@ {-# INLINABLE withSome2 #-} withSome3- :: forall (f3 :: k3 -> k2 -> k1 -> Type) (r :: Type)+ :: forall k3 k2 k1 (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 -- ^@@ -142,7 +141,7 @@ {-# INLINABLE withSome3 #-} withSome4- :: forall (f4 :: k4 -> k3 -> k2 -> k1 -> Type) (r :: Type)+ :: forall k4 k3 k2 k1 (f4 :: k4 -> k3 -> k2 -> k1 -> Type) (r :: Type) . Some4 f4 -> (forall a4 a3 a2 a1 . (SingI a4, SingI a3, SingI a2, SingI a1)@@ -155,7 +154,7 @@ -- | Like 'withSome1', but takes an explicit 'Sing' besides the 'SingI' instance. withSome1Sing- :: forall (f1 :: k1 -> Type) (r :: Type)+ :: forall k1 (f1 :: k1 -> Type) (r :: Type) . Some1 f1 -> (forall a1. (SingI a1) => Sing a1 -> f1 a1 -> r) -> r -- ^@@ -164,7 +163,7 @@ -- | Like 'withSome2', but takes explicit 'Sing's besides the 'SingI' instances. withSome2Sing- :: forall (f2 :: k2 -> k1 -> Type) (r :: Type)+ :: forall k2 k1 (f2 :: k2 -> k1 -> Type) (r :: Type) . Some2 f2 -> (forall a2 a1. (SingI a2, SingI a1) => Sing a2 -> Sing a1 -> f2 a2 a1 -> r) -> r -- ^@@ -173,7 +172,7 @@ -- | Like 'withSome3', but takes explicit 'Sing's besides the 'SingI' instances. withSome3Sing- :: forall (f3 :: k3 -> k2 -> k1 -> Type) (r :: Type)+ :: forall k3 k2 k1 (f3 :: k3 -> k2 -> k1 -> Type) (r :: Type) . Some3 f3 -> (forall a3 a2 a1 . (SingI a3, SingI a2, SingI a1)@@ -185,7 +184,7 @@ -- | Like 'withSome4', but takes explicit 'Sing's besides the 'SingI' instances. withSome4Sing- :: forall (f4 :: k4 -> k3 -> k2 -> k1 -> Type) (r :: Type)+ :: forall k4 k3 k2 k1 (f4 :: k4 -> k3 -> k2 -> k1 -> Type) (r :: Type) . Some4 f4 -> (forall a4 a3 a2 a1 . (SingI a4, SingI a3, SingI a2, SingI a1)@@ -199,43 +198,43 @@ -------------------------------------------------------------------------------- fromSome1- :: forall (f1 :: k1 -> Type) a1+ :: forall k1 (f1 :: k1 -> Type) a1 . (SingI a1, SDecide k1) => Some1 f1 -> Maybe (f1 a1) -- ^ fromSome1 = \(Some1 sa1' x) -> do- Refl <- testEquality sa1' (sing :: Sing a1)+ Refl <- decideEquality sa1' (sing :: Sing a1) return x {-# INLINABLE fromSome1 #-} fromSome2- :: forall (f2 :: k2 -> k1 -> Type) a2 a1+ :: forall k2 k1 (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- Refl <- testEquality sa2' (sing :: Sing a2)- Refl <- testEquality sa1' (sing :: Sing a1)+ Refl <- decideEquality sa2' (sing :: Sing a2)+ Refl <- decideEquality sa1' (sing :: Sing a1) return x {-# INLINABLE fromSome2 #-} fromSome3- :: forall (f3 :: k3 -> k2 -> k1 -> Type) a3 a2 a1+ :: forall k3 k2 k1 (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- Refl <- testEquality sa3' (sing :: Sing a3)- Refl <- testEquality sa2' (sing :: Sing a2)- Refl <- testEquality sa1' (sing :: Sing a1)+ Refl <- decideEquality sa3' (sing :: Sing a3)+ Refl <- decideEquality sa2' (sing :: Sing a2)+ Refl <- decideEquality sa1' (sing :: Sing a1) return x {-# INLINABLE fromSome3 #-} fromSome4- :: forall (f4 :: k4 -> k3 -> k2 -> k1 -> Type) a4 a3 a2 a1+ :: forall k4 k3 k2 k1 (f4 :: k4 -> k3 -> k2 -> k1 -> Type) a4 a3 a2 a1 . ( SingI a4, SDecide k4 , SingI a3, SDecide k3 , SingI a2, SDecide k2@@ -243,10 +242,10 @@ => Some4 f4 -> Maybe (f4 a4 a3 a2 a1) -- ^ fromSome4 = \(Some4 sa4' sa3' sa2' sa1' x) -> do- Refl <- testEquality sa4' (sing :: Sing a4)- Refl <- testEquality sa3' (sing :: Sing a3)- Refl <- testEquality sa2' (sing :: Sing a2)- Refl <- testEquality sa1' (sing :: Sing a1)+ Refl <- decideEquality sa4' (sing :: Sing a4)+ Refl <- decideEquality sa3' (sing :: Sing a3)+ Refl <- decideEquality sa2' (sing :: Sing a2)+ Refl <- decideEquality sa1' (sing :: Sing a1) return x {-# INLINABLE fromSome4 #-} @@ -254,7 +253,7 @@ -- A @lens@-compatible 'Prism'' for constructing and deconstructing a 'Some1'. _Some1- :: forall (f1 :: k1 -> Type) a1+ :: forall k1 (f1 :: k1 -> Type) a1 . (SingI a1, SDecide k1) => Prism' (Some1 f1) (f1 a1) _Some1 = prism' some1 fromSome1@@ -262,7 +261,7 @@ -- A @lens@-compatible 'Prism'' for constructing and deconstructing a 'Some2'. _Some2- :: forall (f2 :: k2 -> k1 -> Type) a2 a1+ :: forall k2 k1 (f2 :: k2 -> k1 -> Type) a2 a1 . ( SingI a2, SDecide k2 , SingI a1, SDecide k1 ) => Prism' (Some2 f2) (f2 a2 a1)@@ -271,7 +270,7 @@ -- A @lens@-compatible 'Prism'' for constructing and deconstructing a 'Some3'. _Some3- :: forall (f3 :: k3 -> k2 -> k1 -> Type) a3 a2 a1+ :: forall k3 k2 k1 (f3 :: k3 -> k2 -> k1 -> Type) a3 a2 a1 . ( SingI a3, SDecide k3 , SingI a2, SDecide k2 , SingI a1, SDecide k1 )@@ -281,7 +280,7 @@ -- A @lens@-compatible 'Prism'' for constructing and deconstructing a 'Some4'. _Some4- :: forall (f4 :: k4 -> k3 -> k2 -> k1 -> Type) a4 a3 a2 a1+ :: forall k4 k3 k2 k1 (f4 :: k4 -> k3 -> k2 -> k1 -> Type) a4 a3 a2 a1 . ( SingI a4, SDecide k4 , SingI a3, SDecide k3 , SingI a2, SDecide k2@@ -330,7 +329,8 @@ -- Hint: @'same1' ('some1' . 'Exinst.P1') :: 'Some1' f -> 'Some1' g -> 'Some1' ('Exinst.P1' f g)@ {-# INLINABLE same1 #-} same1- :: SDecide k1+ :: forall k1 f g x+ . SDecide k1 => (forall a1. SingI a1 => f a1 -> g a1 -> x) -> Some1 (f :: k1 -> Type) -> Some1 (g :: k1 -> Type)@@ -338,7 +338,7 @@ same1 z = \s1f s1g -> withSome1Sing s1f $ \sa1 f -> withSome1Sing s1g $ \sa1' g -> do- Refl <- testEquality sa1 sa1'+ Refl <- decideEquality sa1 sa1' pure (z f g) -- | @'same2' x a b@ applies @x@ to the contents of @a@ and @b@ if their type@@ -347,7 +347,8 @@ -- Hint: @'same2' ('some2' . 'Exinst.P2') :: 'Some2' f -> 'Some2' g -> 'Some2' ('Exinst.P2' f g)@ {-# INLINABLE same2 #-} same2- :: (SDecide k2, SDecide k1)+ :: forall k2 k1 f g x+ . (SDecide k2, SDecide k1) => (forall a2 a1. SingI a1 => f a2 a1 -> g a2 a1 -> x) -> Some2 (f :: k2 -> k1 -> Type) -> Some2 (g :: k2 -> k1 -> Type)@@ -355,8 +356,8 @@ same2 z = \s2l s2g -> withSome2Sing s2l $ \sa2 sa1 f -> withSome2Sing s2g $ \sa2' sa1' g -> do- Refl <- testEquality sa2 sa2'- Refl <- testEquality sa1 sa1'+ Refl <- decideEquality sa2 sa2'+ Refl <- decideEquality sa1 sa1' pure (z f g) -- | @'same3' x a b@ applies @x@ to the contents of @a@ and @b@ if their type@@ -365,7 +366,8 @@ -- Hint: @'same3' ('some3' . 'Exinst.P3') :: 'Some3' f -> 'Some3' g -> 'Some3' ('Exinst.P3' f g)@ {-# INLINABLE same3 #-} same3- :: (SDecide k3, SDecide k2, SDecide k1)+ :: forall k3 k2 k1 f g x+ . (SDecide k3, SDecide k2, SDecide k1) => (forall a3 a2 a1. (SingI a3, SingI a2, SingI a1) => f a3 a2 a1 -> g a3 a2 a1 -> x) -> Some3 (f :: k3 -> k2 -> k1 -> Type)@@ -374,9 +376,9 @@ same3 z = \s3l s3g -> withSome3Sing s3l $ \sa3 sa2 sa1 f -> withSome3Sing s3g $ \sa3' sa2' sa1' g -> do- Refl <- testEquality sa3 sa3'- Refl <- testEquality sa2 sa2'- Refl <- testEquality sa1 sa1'+ Refl <- decideEquality sa3 sa3'+ Refl <- decideEquality sa2 sa2'+ Refl <- decideEquality sa1 sa1' pure (z f g) -- | @'same4' x a b@ applies @x@ to the contents of @a@ and @b@ if their type@@ -385,7 +387,8 @@ -- Hint: @'same4' ('some4' . 'Exinst.P4') :: 'Some4' f -> 'Some4' g -> 'Some4' ('Exinst.P4' f g)@ {-# INLINABLE same4 #-} same4- :: (SDecide k4, SDecide k3, SDecide k2, SDecide k1)+ :: forall k4 k3 k2 k1 f g x+ . (SDecide k4, SDecide k3, SDecide k2, SDecide k1) => (forall a4 a3 a2 a1. (SingI a4, SingI a3, SingI a2, SingI a1) => f a4 a3 a2 a1 -> g a4 a3 a2 a1 -> x) -> Some4 (f :: k4 -> k3 -> k2 -> k1 -> Type)@@ -394,10 +397,10 @@ same4 z = \s4l s4g -> withSome4Sing s4l $ \sa4 sa3 sa2 sa1 f -> withSome4Sing s4g $ \sa4' sa3' sa2' sa1' g -> do- Refl <- testEquality sa4 sa4'- Refl <- testEquality sa3 sa3'- Refl <- testEquality sa2 sa2'- Refl <- testEquality sa1 sa1'+ Refl <- decideEquality sa4 sa4'+ Refl <- decideEquality sa3 sa3'+ Refl <- decideEquality sa2 sa2'+ Refl <- decideEquality sa1 sa1' pure (z f g) --------------------------------------------------------------------------------