diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,3 +1,13 @@ +# Version 0.1.1 + +* Relax upper bound on `singletons` dependency. + +* `withSome{1,2,3,4}Sing` brings `SingI` instances to scope. + +* Generalized the `(* -> Constraint)` parameter in `Dict{1,2,3,4}` + to `(k -> Constraint)`. + + # Version 0.1 * Initial release. diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -554,7 +554,7 @@ [`instant-hashable`](https://hackage.haskell.org/package/instant-hashable), [`instant-bytes`](https://hackage.haskell.org/package/instant-bytes) and [`instant-deepseq`](https://hackage.haskell.org/package/instant-deepseq)) -with [`exinst-generics`](https://hackage.haskell.org/package/exinst-generics) (and +with [`exinst`](https://hackage.haskell.org/package/exinst) (and [`exinst-aeson`](https://hackage.haskell.org/package/exinst-aeson), [`exinst-hashable`](https://hackage.haskell.org/package/exinst-hashable), [`exinst-bytes`](https://hackage.haskell.org/package/exinst-bytes) and diff --git a/exinst.cabal b/exinst.cabal --- a/exinst.cabal +++ b/exinst.cabal @@ -1,5 +1,5 @@ name: exinst -version: 0.1 +version: 0.1.1 author: Renzo Carbonara maintainer: renzoλcarbonara.com.ar copyright: Renzo Carbonara 2015 @@ -12,8 +12,8 @@ synopsis: Derive instances for your existential types. homepage: https://github.com/k0001/exinst bug-reports: https://github.com/k0001/exinst/issues - + library hs-source-dirs: src/lib default-language: Haskell2010 @@ -25,6 +25,6 @@ build-depends: base >=4.7 && <4.9 , constraints >=0.4 && <0.5 - , singletons >=1.1 && <1.2 + , singletons >=1.1 && <2.1 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 @@ -16,7 +16,7 @@ import Data.Constraint import Data.Singletons import Data.Singletons.Decide -import Data.Singletons.Types +import Data.Type.Equality import Exinst.Singletons import Prelude @@ -101,9 +101,9 @@ ) => Eq (Some1 f1) where {-# INLINABLE (==) #-} - (==) = \som1x som1y -> - withSome1Sing som1x $ \sa1x (x :: f1 a1x) -> - withSome1Sing som1y $ \sa1y (y :: f1 a1y) -> + (==) = \som1x som1y -> + withSome1Sing som1x $ \sa1x (x :: f1 a1x) -> + withSome1Sing som1y $ \sa1y (y :: f1 a1y) -> maybe False id $ do Refl <- testEquality sa1x sa1y case dict1 sa1x :: Dict (Eq (f1 a1x)) of @@ -118,9 +118,9 @@ ) => Eq (Some2 f2) where {-# INLINABLE (==) #-} - (==) = \som2x som2y -> - withSome2Sing som2x $ \sa2x sa1x (x :: f2 a2x a1x) -> - withSome2Sing som2y $ \sa2y sa1y (y :: f2 a2y a1y) -> + (==) = \som2x som2y -> + withSome2Sing som2x $ \sa2x sa1x (x :: f2 a2x a1x) -> + withSome2Sing som2y $ \sa2y sa1y (y :: f2 a2y a1y) -> maybe False id $ do Refl <- testEquality sa2x sa2y Refl <- testEquality sa1x sa1y @@ -138,9 +138,9 @@ ) => Eq (Some3 f3) where {-# INLINABLE (==) #-} - (==) = \som3x som3y -> - withSome3Sing som3x $ \sa3x sa2x sa1x (x :: f3 a3x a2x a1x) -> - withSome3Sing som3y $ \sa3y sa2y sa1y (y :: f3 a3y a2y a1y) -> + (==) = \som3x som3y -> + withSome3Sing som3x $ \sa3x sa2x sa1x (x :: f3 a3x a2x a1x) -> + withSome3Sing som3y $ \sa3y sa2y sa1y (y :: f3 a3y a2y a1y) -> maybe False id $ do Refl <- testEquality sa3x sa3y Refl <- testEquality sa2x sa2y @@ -161,9 +161,9 @@ ) => Eq (Some4 f4) where {-# INLINABLE (==) #-} - (==) = \som4x som4y -> - withSome4Sing som4x $ \sa4x sa3x sa2x sa1x (x :: f4 a4x a3x a2x a1x) -> - withSome4Sing som4y $ \sa4y sa3y sa2y sa1y (y :: f4 a4y a3y a2y a1y) -> + (==) = \som4x som4y -> + withSome4Sing som4x $ \sa4x sa3x sa2x sa1x (x :: f4 a4x a3x a2x a1x) -> + withSome4Sing som4y $ \sa4y sa3y sa2y sa1y (y :: f4 a4y a3y a2y a1y) -> maybe False id $ do Refl <- testEquality sa4x sa4y Refl <- testEquality sa3x sa3y @@ -184,9 +184,9 @@ ) => Ord (Some1 f1) where {-# INLINABLE compare #-} - compare = \som1x som1y -> - withSome1Sing som1x $ \sa1x (x :: f1 a1x) -> - withSome1Sing som1y $ \sa1y (y :: f1 a1y) -> + compare = \som1x som1y -> + withSome1Sing som1x $ \sa1x (x :: f1 a1x) -> + withSome1Sing som1y $ \sa1y (y :: f1 a1y) -> let termCompare = compare (fromSing sa1x) (fromSing sa1y) in maybe termCompare id $ do Refl <- testEquality sa1x sa1y @@ -205,9 +205,9 @@ ) => Ord (Some2 f2) where {-# INLINABLE compare #-} - compare = \som2x som2y -> - withSome2Sing som2x $ \sa2x sa1x (x :: f2 a2x a1x) -> - withSome2Sing som2y $ \sa2y sa1y (y :: f2 a2y a1y) -> + compare = \som2x som2y -> + withSome2Sing som2x $ \sa2x sa1x (x :: f2 a2x a1x) -> + withSome2Sing som2y $ \sa2y sa1y (y :: f2 a2y a1y) -> let termCompare = compare (fromSing sa2x, fromSing sa1x) (fromSing sa2y, fromSing sa1y) in maybe termCompare id $ do @@ -231,9 +231,9 @@ ) => Ord (Some3 f3) where {-# INLINABLE compare #-} - compare = \som3x som3y -> - withSome3Sing som3x $ \sa3x sa2x sa1x (x :: f3 a3x a2x a1x) -> - withSome3Sing som3y $ \sa3y sa2y sa1y (y :: f3 a3y a2y a1y) -> + compare = \som3x som3y -> + withSome3Sing som3x $ \sa3x sa2x sa1x (x :: f3 a3x a2x a1x) -> + withSome3Sing som3y $ \sa3y sa2y sa1y (y :: f3 a3y a2y a1y) -> let termCompare = compare (fromSing sa3x, fromSing sa2x, fromSing sa1x) (fromSing sa3y, fromSing sa2y, fromSing sa1y) @@ -262,9 +262,9 @@ ) => Ord (Some4 f4) where {-# INLINABLE compare #-} - compare = \som4x som4y -> - withSome4Sing som4x $ \sa4x sa3x sa2x sa1x (x :: f4 a4x a3x a2x a1x) -> - withSome4Sing som4y $ \sa4y sa3y sa2y sa1y (y :: f4 a4y a3y a2y a1y) -> + compare = \som4x som4y -> + withSome4Sing som4x $ \sa4x sa3x sa2x sa1x (x :: f4 a4x a3x a2x a1x) -> + withSome4Sing som4y $ \sa4y sa3y sa2y sa1y (y :: f4 a4y a3y a2y a1y) -> let termCompare = compare (fromSing sa4x, fromSing sa3x, fromSing sa2x, fromSing sa1x) (fromSing sa4y, fromSing sa3y, fromSing sa2y, fromSing sa1y) @@ -275,4 +275,3 @@ Refl <- testEquality sa1x sa1y case dict4 sa4x sa3x sa2x sa1x :: Dict (Ord (f4 a4x a3x a2x a1x)) of Dict -> Just (compare x y) - 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 @@ -45,7 +45,7 @@ import Data.Constraint import Data.Singletons import Data.Singletons.Decide -import Data.Singletons.Types +import Data.Type.Equality import Prelude import Exinst.Singletons.Internal @@ -82,7 +82,7 @@ => f4 a4 a3 a2 a1 -> Some4 f4 -- ^ some4 = Some4 (sing :: Sing a4) (sing :: Sing a3) - (sing :: Sing a2) (sing :: Sing a1) + (sing :: Sing a2) (sing :: Sing a1) {-# INLINE some4 #-} -------------------------------------------------------------------------------- @@ -92,7 +92,7 @@ . Some1 f1 -> (forall a1. SingI a1 => f1 a1 -> r) -> r -- ^ -withSome1 (Some1 sa1 x) g = withSingI sa1 (g x) +withSome1 s1 g = withSome1Sing s1 (\_ -> g) {-# INLINABLE withSome1 #-} withSome2 @@ -100,7 +100,7 @@ . Some2 f2 -> (forall a2 a1. (SingI a2, SingI a1) => f2 a2 a1 -> r) -> r -- ^ -withSome2 (Some2 sa2 sa1 x) g = withSingI sa2 (withSingI sa1 (g x)) +withSome2 s2 g = withSome2Sing s2 (\_ _ -> g) {-# INLINABLE withSome2 #-} withSome3 @@ -108,8 +108,7 @@ . Some3 f3 -> (forall a3 a2 a1. (SingI a3, SingI a2, SingI a1) => f3 a3 a2 a1 -> r) -> r -- ^ -withSome3 (Some3 sa3 sa2 sa1 x) g = - withSingI sa3 (withSingI sa2 (withSingI sa1 (g x))) +withSome3 s3 g = withSome3Sing s3 (\_ _ _ -> g) {-# INLINABLE withSome3 #-} withSome4 @@ -119,47 +118,52 @@ . (SingI a4, SingI a3, SingI a2, SingI a1) => f4 a4 a3 a2 a1 -> r) -> r -- ^ -withSome4 (Some4 sa4 sa3 sa2 sa1 x) g = - withSingI sa4 (withSingI sa3 (withSingI sa2 (withSingI sa1 (g x)))) +withSome4 s4 g = withSome4Sing s4 (\_ _ _ _ -> g) {-# INLINABLE withSome4 #-} -------------------------------------------------------------------------------- --- | Like 'withSome1', but takes an explicit 'Sing' instead of a 'SingI' instance. +-- | Like 'withSome1', but takes an explicit 'Sing' besides the 'SingI' instance. withSome1Sing :: forall (f1 :: k1 -> *) (r :: *) . Some1 f1 - -> (forall a1. Sing a1 -> f1 a1 -> r) + -> (forall a1. (SingI a1) => Sing a1 -> f1 a1 -> r) -> r -- ^ -withSome1Sing (Some1 sa1 x) g = g sa1 x +withSome1Sing (Some1 sa1 x) g = withSingI sa1 (g sa1 x) {-# INLINABLE withSome1Sing #-} --- | Like 'withSome2', but takes explicit 'Sing's instead of 'SingI' instances. +-- | Like 'withSome2', but takes explicit 'Sing's besides the 'SingI' instances. withSome2Sing :: forall (f2 :: k2 -> k1 -> *) (r :: *) . Some2 f2 - -> (forall a2 a1. Sing a2 -> Sing a1 -> f2 a2 a1 -> r) + -> (forall a2 a1. (SingI a2, SingI a1) => Sing a2 -> Sing a1 -> f2 a2 a1 -> r) -> r -- ^ -withSome2Sing (Some2 sa2 sa1 x) g = g sa2 sa1 x +withSome2Sing (Some2 sa2 sa1 x) g = withSingI sa2 (withSingI sa1 (g sa2 sa1 x)) {-# INLINABLE withSome2Sing #-} --- | Like 'withSome3', but takes explicit 'Sing's instead of 'SingI' instances. +-- | Like 'withSome3', but takes explicit 'Sing's besides the 'SingI' instances. withSome3Sing :: forall (f3 :: k3 -> k2 -> k1 -> *) (r :: *) . Some3 f3 - -> (forall a3 a2 a1. Sing a3 -> Sing a2 -> Sing a1 -> f3 a3 a2 a1 -> r) + -> (forall a3 a2 a1 + . (SingI a3, SingI a2, SingI a1) + => Sing a3 -> Sing a2 -> Sing a1 -> f3 a3 a2 a1 -> r) -> r -- ^ -withSome3Sing (Some3 sa3 sa2 sa1 x) g = g sa3 sa2 sa1 x +withSome3Sing (Some3 sa3 sa2 sa1 x) g = + withSingI sa3 (withSingI sa2 (withSingI sa1 (g sa3 sa2 sa1 x))) {-# INLINABLE withSome3Sing #-} --- | Like 'withSome4', but takes explicit 'Sing's instead of 'SingI' instances. +-- | Like 'withSome4', but takes explicit 'Sing's besides the 'SingI' instances. withSome4Sing :: forall (f4 :: k4 -> k3 -> k2 -> k1 -> *) (r :: *) . Some4 f4 -> (forall a4 a3 a2 a1 - . Sing a4 -> Sing a3 -> Sing a2 -> Sing a1 -> f4 a4 a3 a2 a1 -> r) + . (SingI a4, SingI a3, SingI a2, SingI a1) + => Sing a4 -> Sing a3 -> Sing a2 -> Sing a1 -> f4 a4 a3 a2 a1 -> r) -> r -- ^ -withSome4Sing (Some4 sa4 sa3 sa2 sa1 x) g = g sa4 sa3 sa2 sa1 x +withSome4Sing (Some4 sa4 sa3 sa2 sa1 x) g = + withSingI sa4 (withSingI sa3 (withSingI sa2 (withSingI sa1 + (g sa4 sa3 sa2 sa1 x)))) {-# INLINABLE withSome4Sing #-} -------------------------------------------------------------------------------- @@ -218,14 +222,14 @@ -------------------------------------------------------------------------------- -class Dict1 (c :: * -> Constraint) (f1 :: k1 -> *) where +class Dict1 (c :: k0 -> Constraint) (f1 :: k1 -> k0) where dict1 :: Sing a1 -> Dict (c (f1 a1)) -class Dict2 (c :: * -> Constraint) (f2 :: k2 -> k1 -> *) where +class Dict2 (c :: k0 -> Constraint) (f2 :: k2 -> k1 -> k0) where dict2 :: Sing a2 -> Sing a1 -> Dict (c (f2 a2 a1)) -class Dict3 (c :: * -> Constraint) (f3 :: k3 -> k2 -> k1 -> *) where +class Dict3 (c :: k0 -> Constraint) (f3 :: k3 -> k2 -> k1 -> k0) where dict3 :: Sing a3 -> Sing a2 -> Sing a1 -> Dict (c (f3 a3 a2 a1)) -class Dict4 (c :: * -> Constraint) (f4 :: k4 -> k3 -> k2 -> k1 -> *) where +class Dict4 (c :: k0 -> Constraint) (f4 :: k4 -> k3 -> k2 -> k1 -> k0) where dict4 :: Sing a4 -> Sing a3 -> Sing a2 -> Sing a1 -> Dict (c (f4 a4 a3 a2 a1))