singletons 3.0.3 → 3.0.4
raw patch · 6 files changed
+115/−25 lines, 6 filesdep ~base
Dependency ranges changed: base
Files
- CHANGES.md +8/−0
- singletons.cabal +5/−4
- src/Data/Singletons.hs +21/−6
- src/Data/Singletons/Sigma.hs +6/−1
- tests/ByHand.hs +56/−10
- tests/ByHand2.hs +19/−4
CHANGES.md view
@@ -1,6 +1,14 @@ Changelog for the `singletons` project ====================================== +3.0.4 [2024.12.11]+------------------+* Define `Sing` instances such that they explicitly match on their types on the+ left-hand sides (e.g., define `type instance Sing @(k1 ~> k2) = SLambda`+ instead of `type instance Sing = SLambda`. Doing so will make `singletons`+ future-proof once+ [GHC#23515](https://gitlab.haskell.org/ghc/ghc/-/issues/23515) is fixed.+ 3.0.3 [2024.05.12] ------------------ * Allow building with GHC 9.10.
singletons.cabal view
@@ -1,5 +1,5 @@ name: singletons-version: 3.0.3+version: 3.0.4 cabal-version: 1.24 synopsis: Basic singleton types and definitions homepage: http://www.github.com/goldfirere/singletons@@ -17,9 +17,10 @@ , GHC == 9.0.2 , GHC == 9.2.7 , GHC == 9.4.8- , GHC == 9.6.5+ , GHC == 9.6.6 , GHC == 9.8.2 , GHC == 9.10.1+ , GHC == 9.12.1 extra-source-files: README.md, CHANGES.md license: BSD3 license-file: LICENSE@@ -60,7 +61,7 @@ library hs-source-dirs: src- build-depends: base >= 4.9 && < 4.21+ build-depends: base >= 4.9 && < 4.22 default-language: Haskell2010 exposed-modules: Data.Singletons Data.Singletons.Decide@@ -77,5 +78,5 @@ other-modules: ByHand ByHand2 - build-depends: base >= 4.9 && < 4.21,+ build-depends: base >= 4.9 && < 4.22, singletons
src/Data/Singletons.hs view
@@ -229,11 +229,11 @@ -- @ -- -- Here, @f@ uses methods from both 'SingI' and 'SingKind'. However, the shape--- of each constraint is rather different: using 'sing' requires a 'SingI T'--- constraint, whereas using 'fromSing' requires a 'SingKind K' constraint.+-- of each constraint is rather different: using 'sing' requires a @SingI T@+-- constraint, whereas using 'fromSing' requires a @SingKind K@ constraint. -- -- If you need to satisfy this constraint with an explicit singleton, please--- see 'withSingI' or the 'Sing' pattern synonym.+-- see 'withSingI' or the v'Sing' pattern synonym. #if __GLASGOW_HASKELL__ >= 900 type SingI :: forall {k}. k -> Constraint #endif@@ -405,7 +405,12 @@ newtype SWrappedSing :: forall k (a :: k). WrappedSing a -> Type where SWrapSing :: forall k (a :: k) (ws :: WrappedSing a). { sUnwrapSing :: Sing a } -> SWrappedSing ws-type instance Sing = SWrappedSing+#if __GLASGOW_HASKELL__ >= 808+type instance Sing @(WrappedSing a) =+#else+type instance Sing =+#endif+ SWrappedSing #if __GLASGOW_HASKELL__ >= 810 type UnwrapSing :: forall k (a :: k). WrappedSing a -> Sing a@@ -591,7 +596,12 @@ -- ( forall a. SingI a => SingI (f a) -- , (ApplyTyCon :: (k1 -> k2) -> (k1 ~> k2)) ~ ApplyTyConAux1 -- ) => SingI (TyCon1 f) where-type instance Apply (TyCon f) x = ApplyTyCon f @@ x+#if __GLASGOW_HASKELL__ >= 808+type instance Apply @k1 @k3 (TyCon @k1 @k2 @(k1 ~> k3) f) x =+#else+type instance Apply (TyCon f) x =+#endif+ ApplyTyCon f @@ x -- | An \"internal\" defunctionalization symbol used primarily in the -- definition of 'ApplyTyCon', as well as the 'SingI' instances for 'TyCon1',@@ -730,7 +740,12 @@ #endif newtype SLambda (f :: k1 ~> k2) = SLambda { applySing :: forall t. Sing t -> Sing (f @@ t) }-type instance Sing = SLambda+#if __GLASGOW_HASKELL__ >= 808+type instance Sing @(k1 ~> k2) =+#else+type instance Sing =+#endif+ SLambda -- | An infix synonym for `applySing` (@@) :: forall k1 k2 (f :: k1 ~> k2) (t :: k1). Sing f -> Sing t -> Sing (f @@ t)
src/Data/Singletons/Sigma.hs view
@@ -99,7 +99,12 @@ (:%&:) :: forall s t (fst :: s) (sfst :: Sing fst) (snd :: t @@ fst). Sing ('WrapSing sfst) -> Sing snd -> SSigma (sfst ':&: snd :: Sigma s t) infixr 4 :%&:-type instance Sing = SSigma+#if __GLASGOW_HASKELL__ >= 808+type instance Sing @(Sigma s t) =+#else+type instance Sing =+#endif+ SSigma instance forall s t (fst :: s) (a :: Sing fst) (b :: t @@ fst). (SingI fst, SingI b)
tests/ByHand.hs view
@@ -98,9 +98,15 @@ data SNat :: Nat -> Type where SZero :: SNat Zero SSucc :: SNat n -> SNat (Succ n)-type instance Sing = SNat+#if __GLASGOW_HASKELL__ >= 808+type instance Sing @Nat =+#else+type instance Sing =+#endif+ SNat -#if __GLASGOW_HASKELL__ >= 810+#if _+_GLASGOW_HASKELL__ >= 810 type SuccSym0 :: Nat ~> Nat #endif data SuccSym0 :: Nat ~> Nat@@ -152,7 +158,12 @@ data SBool :: Bool -> Type where SFalse :: SBool False STrue :: SBool True-type instance Sing = SBool+#if __GLASGOW_HASKELL__ >= 808+type instance Sing @Bool =+#else+type instance Sing =+#endif+ SBool {- (&&) :: Bool -> Bool -> Bool@@ -192,7 +203,12 @@ data SMaybe :: forall k. Maybe k -> Type where SNothing :: SMaybe Nothing SJust :: forall k (a :: k). Sing a -> SMaybe (Just a)-type instance Sing = SMaybe+#if __GLASGOW_HASKELL__ >= 808+type instance Sing @(Maybe k) =+#else+type instance Sing =+#endif+ SMaybe #if __GLASGOW_HASKELL__ >= 810 type EqualsMaybe :: Maybe k -> Maybe k -> Bool@@ -242,7 +258,12 @@ data SList :: forall k. List k -> Type where SNil :: SList Nil SCons :: forall k (h :: k) (t :: List k). Sing h -> SList t -> SList (Cons h t)-type instance Sing = SList+#if __GLASGOW_HASKELL__ >= 808+type instance Sing @(List k) =+#else+type instance Sing =+#endif+ SList #if __GLASGOW_HASKELL__ >= 810 type NilSym0 :: List a@@ -315,7 +336,12 @@ data SEither :: forall k1 k2. Either k1 k2 -> Type where SLeft :: forall k1 (a :: k1). Sing a -> SEither (Left a) SRight :: forall k2 (b :: k2). Sing b -> SEither (Right b)-type instance Sing = SEither+#if __GLASGOW_HASKELL__ >= 808+type instance Sing @(Either k1 k2) =+#else+type instance Sing =+#endif+ SEither instance (SingI a) => SingI (Left (a :: k)) where sing = SLeft sing@@ -361,7 +387,12 @@ #endif data SComposite :: forall k1 k2. Composite k1 k2 -> Type where SMkComp :: forall k1 k2 (a :: Either (Maybe k1) k2). SEither a -> SComposite (MkComp a)-type instance Sing = SComposite+#if __GLASGOW_HASKELL__ >= 808+type instance Sing @(Composite k1 k2) =+#else+type instance Sing =+#endif+ SComposite instance SingI a => SingI (MkComp (a :: Either (Maybe k1) k2)) where sing = SMkComp sing@@ -393,7 +424,12 @@ #endif data SEmpty :: Empty -> Type -type instance Sing = SEmpty+#if __GLASGOW_HASKELL__ >= 808+type instance Sing @Empty =+#else+type instance Sing =+#endif+ SEmpty instance SingKind Empty where type Demote Empty = Empty fromSing = \case@@ -420,7 +456,12 @@ SNat :: SRep Nat SMaybe :: SRep a -> SRep (Maybe a) SVec :: SRep a -> SNat n -> SRep (Vec a n)-type instance Sing = SRep+#if __GLASGOW_HASKELL__ >= 808+type instance Sing @Type =+#else+type instance Sing =+#endif+ SRep instance SingI Nat where sing = SNat@@ -1039,4 +1080,9 @@ #endif data SG :: forall a. G a -> Type where SMkG :: SG MkG-type instance Sing = SG+#if __GLASGOW_HASKELL__ >= 808+type instance Sing @(G a) =+#else+type instance Sing =+#endif+ SG
tests/ByHand2.hs view
@@ -1,7 +1,7 @@ {-# LANGUAGE DataKinds, PolyKinds, TypeFamilies, GADTs, TypeOperators, DefaultSignatures, ScopedTypeVariables, InstanceSigs, MultiParamTypeClasses, FunctionalDependencies,- UndecidableInstances, CPP #-}+ UndecidableInstances, CPP, TypeApplications #-} {-# OPTIONS_GHC -Wno-missing-signatures -Wno-orphans #-} #if __GLASGOW_HASKELL__ < 806@@ -27,7 +27,12 @@ data SNat :: Nat -> Type where SZero :: SNat 'Zero SSucc :: SNat n -> SNat ('Succ n)-type instance Sing = SNat+#if __GLASGOW_HASKELL__ >= 808+type instance Sing @Nat =+#else+type instance Sing =+#endif+ SNat {- type Bool :: Type@@ -40,7 +45,12 @@ data SBool :: Bool -> Type where SFalse :: SBool 'False STrue :: SBool 'True-type instance Sing = SBool+#if __GLASGOW_HASKELL__ >= 808+type instance Sing @Bool =+#else+type instance Sing =+#endif+ SBool {- type Ordering :: Type@@ -54,7 +64,12 @@ SLT :: SOrdering 'LT SEQ :: SOrdering 'EQ SGT :: SOrdering 'GT-type instance Sing = SOrdering+#if __GLASGOW_HASKELL__ >= 808+type instance Sing @Ordering =+#else+type instance Sing =+#endif+ SOrdering {- not :: Bool -> Bool