typelits-witnesses 0.4.0.1 → 0.4.1.0
raw patch · 5 files changed
+266/−206 lines, 5 filesdep ~dependent-sumsetup-changedPVP: major bump suggested
API removals or changes: PVP suggests a major version bump
Dependency ranges changed: dependent-sum
API changes (from Hackage documentation)
- GHC.TypeLits.Witnesses: data Natural
+ GHC.TypeLits.Witnesses: data () => Natural
- GHC.TypeLits.Witnesses: data SomeNat
+ GHC.TypeLits.Witnesses: data () => SomeNat
- GHC.TypeLits.Witnesses: data SomeSymbol
+ GHC.TypeLits.Witnesses: data () => SomeSymbol
Files
- CHANGELOG.md +9/−0
- Setup.hs +1/−0
- src/GHC/TypeLits/Compare.hs +86/−78
- src/GHC/TypeLits/Witnesses.hs +127/−90
- typelits-witnesses.cabal +43/−38
CHANGELOG.md view
@@ -1,6 +1,15 @@ Changelog ========= +Version 0.4.1.0+---------------++<https://github.com/mstksg/typelits-witnesses/releases/tag/v0.4.1.0>++*July 24, 2024*++* Use the `SSymbol` and `SNat` from *base* on GHC 9.8++ Version 0.4.0.1 ---------------
Setup.hs view
@@ -1,2 +1,3 @@ import Distribution.Simple+ main = defaultMain
src/GHC/TypeLits/Compare.hs view
@@ -1,15 +1,14 @@-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE KindSignatures #-}-{-# LANGUAGE LambdaCase #-}-{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TypeInType #-}-{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE TypeOperators #-} -- | -- Module : GHC.TypeLits.Compare--- Copyright : (c) Justin Le 2016+-- Copyright : (c) Justin Le 2024 -- License : MIT -- Maintainer : justin@jle.im -- Stability : unstable@@ -74,96 +73,105 @@ -- -- This module is useful for helping bridge between libraries that use -- different 'Nat'-based comparison systems in their type constraints.-module GHC.TypeLits.Compare- ( -- * '<=' and '<=?'- (:<=?)(..)- , (%<=?)- -- ** Convenience functions- , isLE- , isNLE- -- * 'CmpNat'- , SCmpNat(..)- , GHC.TypeLits.Compare.cmpNat- -- ** Manipulating witnesses- , flipCmpNat- , cmpNatEq- , eqCmpNat- , reflCmpNat- , cmpNatLE- , cmpNatGOrdering- )- where+module GHC.TypeLits.Compare (+ -- * '<=' and '<=?'+ (:<=?) (..),+ (%<=?), -import Data.Kind-import Data.Type.Equality-import GHC.TypeLits ( Nat, KnownNat, CmpNat- , type (<=?)- , natVal )-import Unsafe.Coerce-import Data.GADT.Compare+ -- ** Convenience functions+ isLE,+ isNLE, + -- * 'CmpNat'+ SCmpNat (..),+ GHC.TypeLits.Compare.cmpNat,++ -- ** Manipulating witnesses+ flipCmpNat,+ cmpNatEq,+ eqCmpNat,+ reflCmpNat,+ cmpNatLE,+ cmpNatGOrdering,+)+where++import Data.GADT.Compare+import Data.Kind+import Data.Type.Equality+import GHC.TypeLits (+ CmpNat,+ KnownNat,+ Nat,+ natVal,+ type (<=?),+ )+import Unsafe.Coerce+ -- | Simplified version of '%<=?': check if @m@ is less than or equal to to -- @n@. If it is, match on @'Just' 'Refl'@ to get GHC to believe it, -- within the body of the pattern match.-isLE- :: (KnownNat m, KnownNat n)- => p m- -> q n- -> Maybe ((m <=? n) :~: 'True)+isLE ::+ (KnownNat m, KnownNat n) =>+ p m ->+ q n ->+ Maybe ((m <=? n) :~: 'True) isLE m n = case m %<=? n of- LE Refl -> Just Refl- NLE _ _ -> Nothing+ LE Refl -> Just Refl+ NLE _ _ -> Nothing -- | Simplified version of '%<=?': check if @m@ is not less than or equal -- to to @n@. If it is, match on @'Just' 'Refl'@ to get GHC to believe it, -- within the body of the pattern match.-isNLE- :: (KnownNat m, KnownNat n)- => p m- -> q n- -> Maybe ((m <=? n) :~: 'False)+isNLE ::+ (KnownNat m, KnownNat n) =>+ p m ->+ q n ->+ Maybe ((m <=? n) :~: 'False) isNLE m n = case m %<=? n of- NLE Refl Refl -> Just Refl- LE _ -> Nothing+ NLE Refl Refl -> Just Refl+ LE _ -> Nothing -- | Two possible ordered relationships between two natural numbers. data (:<=?) :: Nat -> Nat -> Type where- LE :: ((m <=? n) :~: 'True) -> (m :<=? n)- NLE :: ((m <=? n) :~: 'False) -> ((n <=? m) :~: 'True) -> (m :<=? n)+ LE :: ((m <=? n) :~: 'True) -> m :<=? n+ NLE :: ((m <=? n) :~: 'False) -> ((n <=? m) :~: 'True) -> m :<=? n -- | Compare @m@ and @n@, classifying their relationship into some -- constructor of ':<=?'.-(%<=?)- :: (KnownNat m, KnownNat n)- => p m- -> q n- -> (m :<=? n)-m %<=? n | natVal m <= natVal n = LE (unsafeCoerce Refl)- | otherwise = NLE (unsafeCoerce Refl) (unsafeCoerce Refl)+(%<=?) ::+ (KnownNat m, KnownNat n) =>+ p m ->+ q n ->+ (m :<=? n)+m %<=? n+ | natVal m <= natVal n = LE (unsafeCoerce Refl)+ | otherwise = NLE (unsafeCoerce Refl) (unsafeCoerce Refl) -- | Three possible ordered relationships between two natural numbers. data SCmpNat :: Nat -> Nat -> Type where- CLT :: (CmpNat m n :~: 'LT) -> SCmpNat m n- CEQ :: (CmpNat m n :~: 'EQ) -> (m :~: n) -> SCmpNat m n- CGT :: (CmpNat m n :~: 'GT) -> SCmpNat m n+ CLT :: (CmpNat m n :~: 'LT) -> SCmpNat m n+ CEQ :: (CmpNat m n :~: 'EQ) -> (m :~: n) -> SCmpNat m n+ CGT :: (CmpNat m n :~: 'GT) -> SCmpNat m n -- | Compare @m@ and @n@, classifying their relationship into some -- constructor of 'SCmpNat'.-cmpNat- :: (KnownNat m, KnownNat n)- => p m- -> q n- -> SCmpNat m n+cmpNat ::+ (KnownNat m, KnownNat n) =>+ p m ->+ q n ->+ SCmpNat m n cmpNat m n = case compare (natVal m) (natVal n) of- LT -> CLT (unsafeCoerce Refl)- EQ -> CEQ (unsafeCoerce Refl) (unsafeCoerce Refl)- GT -> CGT (unsafeCoerce Refl)+ LT -> CLT (unsafeCoerce Refl)+ EQ -> CEQ (unsafeCoerce Refl) (unsafeCoerce Refl)+ GT -> CGT (unsafeCoerce Refl) -- | Flip an inequality. flipCmpNat :: SCmpNat m n -> SCmpNat n m-flipCmpNat = \case CLT Refl -> CGT (unsafeCoerce Refl)- CEQ Refl Refl -> CEQ (unsafeCoerce Refl) Refl- CGT Refl -> CLT (unsafeCoerce Refl)+flipCmpNat = \case+ CLT Refl -> CGT (unsafeCoerce Refl)+ CEQ Refl Refl -> CEQ (unsafeCoerce Refl) Refl+ CGT Refl -> CLT (unsafeCoerce Refl) -- | @'CmpNat' m n@ being 'EQ' implies that @m@ is equal to @n@. cmpNatEq :: (CmpNat m n :~: 'EQ) -> (m :~: n)@@ -179,16 +187,16 @@ -- | Convert to ':<=?' cmpNatLE :: SCmpNat m n -> (m :<=? n)-cmpNatLE = \case CLT Refl -> LE (unsafeCoerce Refl)- CEQ Refl Refl -> LE (unsafeCoerce Refl)- CGT Refl -> NLE (unsafeCoerce Refl) (unsafeCoerce Refl)+cmpNatLE = \case+ CLT Refl -> LE (unsafeCoerce Refl)+ CEQ Refl Refl -> LE (unsafeCoerce Refl)+ CGT Refl -> NLE (unsafeCoerce Refl) (unsafeCoerce Refl) -- | Convert to 'GOrdering' -- -- @since 0.4.0.0 cmpNatGOrdering :: SCmpNat n m -> GOrdering n m cmpNatGOrdering = \case- CLT Refl -> GLT- CEQ Refl Refl -> GEQ- CGT Refl -> GGT-+ CLT Refl -> GLT+ CEQ Refl Refl -> GEQ+ CGT Refl -> GGT
src/GHC/TypeLits/Witnesses.hs view
@@ -1,20 +1,21 @@-{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE DataKinds #-} {-# LANGUAGE ExistentialQuantification #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE LambdaCase #-}-{-# LANGUAGE PatternSynonyms #-}-{-# LANGUAGE RankNTypes #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE StandaloneDeriving #-}-{-# LANGUAGE NoStarIsType #-}-{-# LANGUAGE TypeInType #-}-{-# LANGUAGE TypeOperators #-}-{-# LANGUAGE ViewPatterns #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE ViewPatterns #-}+{-# LANGUAGE NoStarIsType #-} -- | -- Module : GHC.TypeLits.Witnesses--- Copyright : (c) Justin Le 2016+-- Copyright : (c) Justin Le 2024 -- License : MIT -- Maintainer : justin@jle.im -- Stability : unstable@@ -84,50 +85,72 @@ -- not just 'Natural' and 'String'. module GHC.TypeLits.Witnesses ( -- * Nats- SNat(..)- , SomeNat(SomeNat_)- , Natural(FromSNat)- , fromSNat- , withKnownNat- , withSomeNat- , toSomeNat+ SNat (SNat),+ SomeNat (SomeNat_),+ Natural (FromSNat),+ fromSNat,+ withKnownNat,+ withSomeNat,+ toSomeNat,+ -- ** Operations- , (%+)- , (%-)- , minusSNat- , minusSNat_- , (%*)- , (%^)+ (%+),+ (%-),+ minusSNat,+ minusSNat_,+ (%*),+ (%^),+ -- ** Compare- , (%<=?)- , sCmpNat+ (%<=?),+ sCmpNat,+ -- ** Unsafe- , unsafeLiftNatOp1- , unsafeLiftNatOp2+ unsafeLiftNatOp1,+ unsafeLiftNatOp2,+ -- * Symbols- , SSymbol(..)- , SomeSymbol(SomeSymbol_)- , pattern FromSSymbol- , fromSSymbol- , withKnownSymbol- , withSomeSymbol- , toSomeSymbol- ) where+ SSymbol (SSymbol),+ SomeSymbol (SomeSymbol_),+ pattern FromSSymbol,+ fromSSymbol,+ withKnownSymbol,+ withSomeSymbol,+ toSomeSymbol,+) where -import Data.GADT.Compare-import Data.GADT.Show-import Data.Proxy-import Data.Type.Equality-import GHC.Natural-import GHC.TypeLits ( KnownSymbol, SomeSymbol(..)- , symbolVal, someSymbolVal, sameSymbol )-import GHC.TypeLits.Compare hiding ((%<=?))-import GHC.TypeNats ( KnownNat, SomeNat(..), CmpNat- , type (+), type (-), type (*), type (^)- , natVal, someNatVal, sameNat )-import Unsafe.Coerce-import qualified GHC.TypeLits.Compare as Comp+import Data.Proxy+import Data.Type.Equality+import GHC.Natural+import GHC.TypeLits (KnownSymbol, SomeSymbol (..), someSymbolVal, symbolVal)+import GHC.TypeLits.Compare hiding ((%<=?))+import qualified GHC.TypeLits.Compare as Comp+import GHC.TypeNats (+ CmpNat,+ KnownNat,+ SomeNat (..),+ natVal,+ someNatVal,+ type (*),+ type (+),+ type (-),+ type (^),+ )+import Unsafe.Coerce +#if MIN_VERSION_base(4,20,0)+import GHC.TypeLits (SSymbol, pattern SSymbol)+import GHC.TypeNats (SNat, pattern SNat)+#else+import Data.GADT.Compare+import Data.GADT.Show+import GHC.TypeLits (sameSymbol)+import GHC.TypeNats (sameNat)+#endif++{-# ANN module "HLint: ignore Use fewer imports" #-}++#if !MIN_VERSION_base(4,20,0) -- | An @'SNat' n@ is a witness for @'KnownNat' n@. -- -- This means that if you pattern match on the 'SNat' constructor, in that@@ -140,28 +163,32 @@ -- -- This is essentially a singleton for 'Nat', and stands in for the -- /singletons/ 'SNat' and 'Data.Singleton.Sing' types.+--+-- Note that this type exists in base as of base 4.18.0 (GHC 9.6) data SNat n = KnownNat n => SNat deriving instance Eq (SNat n) deriving instance Ord (SNat n) instance Show (SNat n) where- showsPrec d x@SNat = showParen (d > 10) $+ showsPrec d x@SNat =+ showParen (d > 10) $ showString "SNat @" . showsPrec 11 (fromSNat x) instance GShow SNat where- gshowsPrec = showsPrec+ gshowsPrec = showsPrec instance TestEquality SNat where- testEquality (SNat :: SNat n) (SNat :: SNat m) =- flip fmap (sameNat (Proxy :: Proxy n) (Proxy :: Proxy m)) $ \case- Refl -> Refl+ testEquality (SNat :: SNat n) (SNat :: SNat m) =+ flip fmap (sameNat (Proxy :: Proxy n) (Proxy :: Proxy m)) $ \case+ Refl -> Refl instance GEq SNat where- geq = testEquality+ geq = testEquality instance GCompare SNat where- gcompare x = cmpNatGOrdering . sCmpNat x+ gcompare x = cmpNatGOrdering . sCmpNat x+#endif data SomeNat__ = forall n. SomeNat__ (SNat n) @@ -174,9 +201,10 @@ -- -- This stands in for the /singletons/ 'Data.Singleton.SomeSing' constructor. pattern SomeNat_ :: SNat n -> SomeNat-pattern SomeNat_ x <- ((\case SomeNat (Proxy :: Proxy n) -> SomeNat__ (SNat :: SNat n)) -> SomeNat__ x)+pattern SomeNat_ x <- (\case SomeNat (Proxy :: Proxy n) -> SomeNat__ (SNat :: SNat n) -> SomeNat__ x) where SomeNat_ (SNat :: SNat n) = SomeNat (Proxy :: Proxy n)+ {-# COMPLETE SomeNat_ #-} -- | A useful pattern synonym for matching on a 'Natural' as if it "were"@@ -192,9 +220,10 @@ -- -- This stands in for the /singletons/ 'Data.Singleton.FromSing' pattern synonym. pattern FromSNat :: SNat n -> Natural-pattern FromSNat x <- ((\i -> withSomeNat i SomeNat_) -> SomeNat_ x)+pattern FromSNat x <- ((`withSomeNat` SomeNat_) -> SomeNat_ x) where FromSNat = fromSNat+ {-# COMPLETE FromSNat #-} -- | Given an @'SNat' n@ and a value that would require a @'KnownNat' n@@@ -211,7 +240,7 @@ -- -- This stands in the /singletons/ 'Data.Singleton.withSomeSing' function. withSomeNat :: Natural -> (forall n. SNat n -> r) -> r-withSomeNat (someNatVal->SomeNat (Proxy :: Proxy n)) x = x (SNat :: SNat n)+withSomeNat (someNatVal -> SomeNat (Proxy :: Proxy n)) x = x (SNat :: SNat n) -- | Promote ("reify") a 'Natural' to an @'SNat' n@ existentially hidden -- inside a 'SomeNat'. To use it, pattern match using 'SomeNat_'.@@ -239,10 +268,10 @@ -- -- The correctness of the relationship is not checked, so be aware that -- this can cause programs to break.-unsafeLiftNatOp1- :: (Natural -> Natural)- -> SNat n- -> SNat m+unsafeLiftNatOp1 ::+ (Natural -> Natural) ->+ SNat n ->+ SNat m unsafeLiftNatOp1 f x = withSomeNat (f (fromSNat x)) unsafeCoerce -- | Lift a binary operation to act on an @'SNat' n@ and @'SNat' m@ that@@ -258,11 +287,11 @@ -- -- The correctness of the relationship is not checked, so be aware that -- this can cause programs to break.-unsafeLiftNatOp2- :: (Natural -> Natural -> Natural)- -> SNat n- -> SNat m- -> SNat o+unsafeLiftNatOp2 ::+ (Natural -> Natural -> Natural) ->+ SNat n ->+ SNat m ->+ SNat o unsafeLiftNatOp2 f x y = withSomeNat (f (fromSNat x) (fromSNat y)) unsafeCoerce -- | Addition of 'SNat's.@@ -290,13 +319,13 @@ -- | A safe version of '%-': it will return 'Left' if @n@ is less than @m@ -- (with a witness that it is), or else return the subtracted 'SNat' in -- 'Right' in a way that is guarunteed to not have runtime underflow.-minusSNat- :: SNat n- -> SNat m- -> Either (CmpNat n m :~: 'LT) (SNat (n - m))-minusSNat (fromSNat->x) (fromSNat->y) = case minusNaturalMaybe x y of- Nothing -> Left (unsafeCoerce Refl)- Just z -> withSomeNat z (Right . unsafeCoerce)+minusSNat ::+ SNat n ->+ SNat m ->+ Either (CmpNat n m :~: 'LT) (SNat (n - m))+minusSNat (fromSNat -> x) (fromSNat -> y) = case minusNaturalMaybe x y of+ Nothing -> Left (unsafeCoerce Refl)+ Just z -> withSomeNat z (Right . unsafeCoerce) -- | A version of 'minusSNat' that just returns a 'Maybe'. minusSNat_ :: SNat n -> SNat m -> Maybe (SNat (n - m))@@ -332,6 +361,7 @@ sCmpNat :: SNat n -> SNat m -> SCmpNat n m sCmpNat x@SNat y@SNat = GHC.TypeLits.Compare.cmpNat x y +#if !MIN_VERSION_base(4,20,0) -- | An @'SSymbol' n@ is a witness for @'KnownSymbol' n@. -- -- This means that if you pattern match on the 'SSymbol' constructor, in that@@ -344,31 +374,35 @@ -- -- This is essentially a singleton for 'Symbol', and stands in for the -- /singletons/ 'SSymbol' and 'Data.Singleton.Sing' types.+--+-- Note that this type exists in base as of base 4.18.0 (GHC 9.6) data SSymbol n = KnownSymbol n => SSymbol deriving instance Eq (SSymbol n) deriving instance Ord (SSymbol n) instance Show (SSymbol n) where- showsPrec d x@SSymbol = showParen (d > 10) $+ showsPrec d x@SSymbol =+ showParen (d > 10) $ showString "SSymbol @" . showsPrec 11 (fromSSymbol x) instance GShow SSymbol where- gshowsPrec = showsPrec+ gshowsPrec = showsPrec instance TestEquality SSymbol where- testEquality (SSymbol :: SSymbol n) (SSymbol :: SSymbol m) =- flip fmap (sameSymbol (Proxy :: Proxy n) (Proxy :: Proxy m)) $ \case- Refl -> Refl+ testEquality (SSymbol :: SSymbol n) (SSymbol :: SSymbol m) =+ flip fmap (sameSymbol (Proxy :: Proxy n) (Proxy :: Proxy m)) $ \case+ Refl -> Refl instance GEq SSymbol where- geq = testEquality+ geq = testEquality instance GCompare SSymbol where- gcompare x y = case compare (fromSSymbol x) (fromSSymbol y) of- LT -> GLT- EQ -> unsafeCoerce GEQ- GT -> GGT+ gcompare x y = case compare (fromSSymbol x) (fromSSymbol y) of+ LT -> GLT+ EQ -> unsafeCoerce GEQ+ GT -> GGT+#endif data SomeSymbol__ = forall n. SomeSymbol__ (SSymbol n) @@ -381,9 +415,11 @@ -- -- This stands in for the /singletons/ 'Data.Singleton.SomeSing' constructor. pattern SomeSymbol_ :: SSymbol n -> SomeSymbol-pattern SomeSymbol_ x <- ((\case SomeSymbol (Proxy :: Proxy n) -> SomeSymbol__ (SSymbol :: SSymbol n)) -> SomeSymbol__ x)+pattern SomeSymbol_ x <-+ (\case SomeSymbol (Proxy :: Proxy n) -> SomeSymbol__ (SSymbol :: SSymbol n) -> SomeSymbol__ x) where SomeSymbol_ (SSymbol :: SSymbol n) = SomeSymbol (Proxy :: Proxy n)+ {-# COMPLETE SomeSymbol_ #-} -- | A useful pattern synonym for matching on a 'String' as if it "were"@@ -400,9 +436,10 @@ -- This stands in for the /singletons/ 'Data.Singleton.FromSing' pattern synonym, except -- it matches on a 'String' instead of a 'Data.Text.Text'. pattern FromSSymbol :: SSymbol n -> String-pattern FromSSymbol x <- ((\i -> withSomeSymbol i SomeSymbol_) -> SomeSymbol_ x)+pattern FromSSymbol x <- ((`withSomeSymbol` SomeSymbol_) -> SomeSymbol_ x) where FromSSymbol = fromSSymbol+ {-# COMPLETE FromSSymbol #-} -- | Given an @'SSymbol' n@ and a value that would require a @'KnownSymbol' n@@@ -420,7 +457,7 @@ -- This stands in the /singletons/ 'Data.Singleton.withSomeSing' function, except it takes -- a 'String' instead of 'Data.Text.Text'. withSomeSymbol :: String -> (forall n. SSymbol n -> r) -> r-withSomeSymbol (someSymbolVal->SomeSymbol (Proxy :: Proxy n)) x = x (SSymbol :: SSymbol n)+withSomeSymbol (someSymbolVal -> SomeSymbol (Proxy :: Proxy n)) x = x (SSymbol :: SSymbol n) -- | Promote ("reify") a 'String' to an @'SSymbol' n@ existentially hidden -- inside a 'SomeNat'. To use it, pattern match using 'SomeSymbol_'.
typelits-witnesses.cabal view
@@ -1,52 +1,57 @@-cabal-version: 1.12+cabal-version: 1.12 -- This file has been generated from package.yaml by hpack version 0.34.5. -- -- see: https://github.com/sol/hpack -name: typelits-witnesses-version: 0.4.0.1-synopsis: Existential witnesses, singletons, and classes for operations on GHC TypeLits-description: This library contains:- .- * A small specialized subset of the *singletons* library as it pertains to- `Nat` and `Symbol`, for when you need some simple functionality without- wanting to invoke the entire *singletons* library.- * Operations for manipulating these singletons and `KnownNat` and- `KnownSymbol` instances, such as addition and multiplication of- singletons/`KnownNat` instances.- * Operations for the comparison of `Nat`s in a way that works well with- *GHC.TypeLits*'s different comparison systems. This is helpful for- bridging together libraries that use different systems; this functionality- is not yet provided by *singletons*.-category: Data-homepage: https://github.com/mstksg/typelits-witnesses-author: Justin Le-maintainer: justin@jle.im-copyright: (c) Justin Le 2018-license: MIT-license-file: LICENSE-build-type: Simple-tested-with:- GHC>=8.2+name: typelits-witnesses+version: 0.4.1.0+synopsis:+ Existential witnesses, singletons, and classes for operations on GHC TypeLits++description:+ This library contains:+ .+ * A small specialized subset of the *singletons* library as it pertains to+ `Nat` and `Symbol`, for when you need some simple functionality without+ wanting to invoke the entire *singletons* library.+ * Operations for manipulating these singletons and `KnownNat` and+ `KnownSymbol` instances, such as addition and multiplication of+ singletons/`KnownNat` instances.+ * Operations for the comparison of `Nat`s in a way that works well with+ *GHC.TypeLits*'s different comparison systems. This is helpful for+ bridging together libraries that use different systems; this functionality+ is not yet provided by *singletons*.++category: Data+homepage: https://github.com/mstksg/typelits-witnesses+author: Justin Le+maintainer: justin@jle.im+copyright: (c) Justin Le 2024+license: MIT+license-file: LICENSE+build-type: Simple+tested-with: GHC >= 8.10 extra-source-files:- README.md- CHANGELOG.md+ CHANGELOG.md+ README.md source-repository head- type: git+ type: git location: git://github.com/mstksg/typelits-witnesses.git library exposed-modules:- GHC.TypeLits.Compare- GHC.TypeLits.Witnesses- other-modules:- Paths_typelits_witnesses- hs-source-dirs:- src- ghc-options: -Wall -Wredundant-constraints -Werror=incomplete-patterns -Wcompat+ GHC.TypeLits.Compare+ GHC.TypeLits.Witnesses++ other-modules: Paths_typelits_witnesses+ hs-source-dirs: src+ ghc-options:+ -Wall -Wredundant-constraints -Werror=incomplete-patterns -Wcompat+ build-depends:- base >=4.10 && <5- , dependent-sum <0.8+ base >=4.10 && <5+ , dependent-sum+ default-language: Haskell2010