typelits-witnesses 0.3.0.3 → 0.4.0.0

raw patch · 6 files changed

+447/−1041 lines, 6 filesdep +dependent-sumdep −constraintsdep −reflectiondep ~basePVP ok

version bump matches the API change (PVP)

Dependencies added: dependent-sum

Dependencies removed: constraints, reflection

Dependency ranges changed: base

API changes (from Hackage documentation)

Files

• CHANGELOG.md +32/−12
• README.md +11/−260
• src/GHC/TypeLits/Compare.hs +34/−6
• src/GHC/TypeLits/List.hs +0/−503
• src/GHC/TypeLits/Witnesses.hs +348/−221
• typelits-witnesses.cabal +22/−39

@@ -1,5 +1,25 @@+Changelog+=========++Version 0.4.0.0+---------------++<https://github.com/mstksg/typelits-witnesses/releases/tag/v0.4.0.0>++*June 20, 2019*++*   Complete overhaul of *GHC.TypeLits.Witnesses* to more or less match the+    interface of singletons.  This changes the role of the module to be a+    "lightweight" version of the singletons library as it pertains to `Nat` and+    `Symbol`.+*   Removal of the *GHC.TypeLits.List* module.  We could perform the same+    overhaul as *GHC.TypeLits.Witnesses*, but it is complex enough that it+    would be better to just use *singletons* instead at that point.+*   Remove all external dependencies, except for *base* and *dependent-sum*.+*   Break compatibility with GHC < 8.2+ Version 0.3.0.3-===============+---------------  <https://github.com/mstksg/typelits-witnesses/releases/tag/v0.3.0.3> @@ -9,7 +29,7 @@ *   Break compatibility with GHC < 8.0  Version 0.3.0.2-===============+---------------  <https://github.com/mstksg/typelits-witnesses/releases/tag/v0.3.0.2> @@ -19,7 +39,7 @@     take different "proxy" types (`p` and `q`).  Version 0.3.0.1-===============+---------------  <https://github.com/mstksg/typelits-witnesses/releases/tag/v0.3.0.1> @@ -27,7 +47,7 @@     haddocks for *GHC.TypeLits.List*.  Version 0.3.0.0-===============+---------------  <https://github.com/mstksg/typelits-witnesses/releases/tag/v0.3.0.0> @@ -40,7 +60,7 @@     because it's just so much more unweidly than using *singletons*.  Version 0.2.3.0-===============+---------------  <https://github.com/mstksg/typelits-witnesses/releases/tag/v0.2.3.0> @@ -48,7 +68,7 @@     inequalities on `KnownNat`s and associated utility functions.  Version 0.2.2.0-===============+---------------  <https://github.com/mstksg/typelits-witnesses/releases/tag/v0.2.2.0> @@ -56,7 +76,7 @@     and `sameSymbols`.  Version 0.2.1.0-===============+---------------  <https://github.com/mstksg/typelits-witnesses/releases/tag/v0.2.1.0> @@ -64,7 +84,7 @@     `NatList` and `SymbolList`.  Version 0.2.0.0-===============+---------------  <https://github.com/mstksg/typelits-witnesses/releases/tag/v0.2.0.0> @@ -77,7 +97,7 @@     the *reflection* package is very strong and worth preserving, I think.  Version 0.1.2.0-===============+---------------  <https://github.com/mstksg/typelits-witnesses/releases/tag/v0.1.2.0> @@ -91,7 +111,7 @@     are both the same.  Version 0.1.1.0-===============+---------------  <https://github.com/mstksg/typelits-witnesses/releases/tag/v0.1.1.0> @@ -99,7 +119,7 @@     `SomeSymbols`.  It really doesn't make any sense for them to be lazy.  Version 0.1.0.1-===============+---------------  <https://github.com/mstksg/typelits-witnesses/releases/tag/v0.1.0.1> @@ -107,7 +127,7 @@     Hackage.  Version 0.1.0.0-===============+---------------  <https://github.com/mstksg/typelits-witnesses/releases/tag/v0.1.0.0> 

@@ -6,266 +6,17 @@ [![typelits-witnesses on Stackage Nightly](http://stackage.org/package/typelits-witnesses/badge/nightly)](http://stackage.org/nightly/package/typelits-witnesses) [![Build Status](https://travis-ci.org/mstksg/typelits-witnesses.svg?branch=master)](https://travis-ci.org/mstksg/typelits-witnesses) --Provides witnesses for `KnownNat` and `KnownSymbol` instances for various-operations on GHC TypeLits --- in particular, the arithmetic operations-defined in `GHC.TypeLits`, and also for type-level lists of `KnownNat` and-`KnownSymbol` instances.--This is useful for situations where you have `KnownNat n`, and you want to-prove to GHC `KnownNat (n + 3)`, or `KnownNat (2*n + 4)`.--It's also useful for when you want to work with type level lists of-`KnownNat`/`KnownSymbol` instances and singletons for traversing them, and be-able to apply analogies of `natVal`/`symbolVal` to lists with analogies for-`SomeNat` and `SomeSymbol`.+This library contains: -Note that most of the functionality in this library can be reproduced in a more-generic way using the great [singletons][] library.  The versions here are-provided as a "plumbing included" alternative that makes some commonly found-design patterns involving GHC's TypeLits functionality a little smoother,-especially when working with external libraries or GHC TypeLit's `Nat`-comparison API.+*   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*.  [singletons]: https://hackage.haskell.org/package/singletons--GHC.TypeLits.Compare-----------------------Provides tools for refining upper and lower bounds on `KnownNat`s and proving-inequalities involving *GHC.TypeLits*'s comparison API. (Both with `<=?` and-`CmpNat`).--If a library function requires `1 <= n` constraint, but only `KnownNat n` is-available:--~~~haskell-foo :: (KnownNat n, 1 <= n) => Proxy n -> Int--bar :: KnownNat n => Proxy n -> Int-bar n = case Proxy @1 %<=? n of-          LE  Refl -> foo n-          NLE _    -> 0-~~~--`foo` requires that `1 <= n`, but `bar` has to handle all cases of `n`.  `%<=?`-lets you compare the `KnownNat`s in two `Proxy`s and returns a `:<=?`, which-has two constructors, `LE` and `NLE`.--If you pattern match on the result, in the `LE` branch, the constraint-`1 <= n` will be satisfied according to GHC, so `bar` can safely call-`foo`, and GHC will recognize that `1 <= n`.--In the `NLE` branch, the constraint that `1 > n` is satisfied, so any-functions that require that constraint would be callable.--For convenience, `isLE` and `isNLE` are also offered:--~~~haskell-bar :: KnownNat n => Proxy n -> Int-bar n = case Proxy @1 `isLE` n of-          Just Refl -> foo n-          Nothing   -> 0-~~~--Similarly, if a library function requires something involving `CmpNat`,-you can use `cmpNat` and the `SCmpNat` type:--~~~haskell-foo1 :: (KnownNat n, CmpNat 5 n ~ LT) => Proxy n -> Int-foo2 :: (KnownNat n, CmpNat 5 n ~ GT) => Proxy n -> Int--bar :: KnownNat n => Proxy n -> Int-bar n = case Proxy @5 `cmpNat` n of-          CLT Refl -> foo1 n-          CEQ _    -> 0-          CGT Refl -> foo2 n-~~~--You can use the `Refl` that `cmpNat` gives you with `flipCmpNat` and-`cmpNatLE` to "flip" the inequality or turn it into something compatible-with `<=?` (useful for when you have to work with libraries that mix the-two methods) or `cmpNatEq` and `eqCmpNat` to get to/from witnesses for-equality of the two `Nat`s.---GHC.TypeLits.Witnesses-------------------------**SOFT DEPRECATED**: Use *[singletons][]* library instead!  However, this-module is still here in case people want the functionality of *singletons*-without requiring the entire library.--Provides witnesses for instances arising from the arithmetic operations-defined in `GHC.TypeLits`.--In general, if you have `KnownNat n`, GHC can't infer `KnownNat (n + 1)`;-and if you have `KnownNat m`, as well, GHC can't infer `KnownNat (n + m)`.--This can be extremely annoying when dealing with libraries and applications-where one regularly adds and subtracts type-level nats and expects `KnownNat`-instances to follow.  For example, vector concatenation of length-encoded-vector types can be:--~~~haskell-concat :: (KnownNat n, KnownNat m)-       => Vector n       a-       -> Vector m       a-       -> Vector (n + m) a-~~~--But, `n + m` now does not have a `KnownNat` instance, which severely hinders-what you can do with this!--Consider this concrete (but silly) example:--~~~haskell-getDoubled :: KnownNat n => Proxy n -> Integer-getDoubled p = natVal (Proxy @(n * 2))-~~~--Which is supposed to call `natVal` with `n * 2`.  However, this fails, because-while `n` is a `KnownNat`, `n * 2` is not necessarily so.  This module lets-you re-assure GHC that this is okay.--The most straightforward/high-level usage is with `withNatOp`:--~~~haskell-getDoubled :: forall n. KnownNat n => Proxy n -> Integer-getDoubled p = withNatOp (%*) p (Proxy @2) $-    natVal (Proxy @(n * 2))-~~~--Within the scope of the argument of-`withNatOp (%*) (Proxy @n) (Proxy @m)`, `n * m` is an instance-of `KnownNat`, so you can use `natVal` on it, and get the expected result:--~~~haskell-> getDoubled (Proxy @12)-24-~~~--There are four "nat operations" defined here, corresponding to the four-type-level operations on `Nat` provided in `GHC.TypeLits`: `(%+)`, `(%-)`,-`(%*)`, and `(%^)`, corresponding to addition, subtraction, multiplication, and-exponentiation, respectively.--Note that `(%-)` is implemented in a way that allows for the result to be a-*negative* `Nat`.--There are more advanced operations dealing with low-level machinery, as well,-in the module.  See module documentation for more detail.--### Singletons replacement--This module is deprecated, and it is recommended you use the functionality from-the *[singletons][]* package instead.  A direct translation using `Proxy` would-be:--~~~haskell-getDoubled :: forall n. KnownNat n => Proxy n -> Integer-getDoubled p = withKnownNat (SNat @n %:* SNat @2) $-    natVal (Proxy @(n * 2))-~~~--But one using singletons throughout the whole process would be:--~~~haskell-getDoubled :: forall n. KnownNat n => Sing n -> Integer-getDoubled s = withKnownNat (s %:* SNat @2) $-    natVal (Proxy @(n * 2))-~~~---GHC.TypeLits.List----------------------**HARD DEPRECATED: Use *[singletons][]* library instead!  This module is-extremely unweildy, and using *singletons* is much, much smoother on many-levels, and integrates everything together in a nice way.  This module will-likely be removed in a future version.--Provides analogies of `KnownNat`, `SomeNat`, `natVal`, etc., to type-level-lists of `KnownNat` instances, and also singletons for iterating over-type-level lists of `Nat`s and `Symbol`s.--If you had `KnownNats ns`, then you have two things you can do with it; first,-`natsVal`, which is like `natVal` but for type-level lists of `KnownNats`:--~~~haskell-> natsVal (Proxy @[1,2,3])-[1,2,3]-~~~--And more importantly, `natsList`, which provides singletons that you can-pattern match on to "reify" the structure of the list, getting a `Proxy n` for-every item in the list with a `KnownNat`/`KnownSymbol` instance in scope for-you to use:--~~~haskell-printNats :: NatList ns -> IO ()-printNats nl = case nl of-                 ØNL       ->-                   return ()-                 p :># nl' -> do-                   print $ natVal p-                   printNats nl'-~~~--~~~haskell-> printNats (natsList :: @[1,2,3])-1-2-3-~~~--Without this, there is no way to "iterate over" and "access" every `Nat` in a-list of `KnownNat`s.  You can't "iterate" over `[1,2,3]` in `Proxy [1,2,3]`,-but you can iterate over them in `NatList [1,2,3]`.--This module also lets you "reify" lists of `Integer`s or `String`s into-`NatList`s and `SymbolList`s, so you can access them at the type level for-some dependent types fun.--~~~haskell-> reifyNats [1,2,3] $ \nl -> do-    print nl-    printNats nl-Proxy :<# Proxy :<# Proxy :<# ØNL-1-2-3-~~~--Another thing you can do is provide witneses that two `[Nat]`s or `[Symbol]`s-are the same/were instantiated with the same numbers/symbols.--~~~haskell-> reifyNats [1,2,3] $ \ns -> do-  reifyNats [1,2,3] $ \ms -> do-    case sameNats ns ms of-      Just Refl -> -- in this branch, ns and ms are the same.-      Nothing   -> -- in this branch, they aren't-~~~--The above would match on the `Just Refl` branch.--See module documentation for more details and variations.--### Singletons replacement--This module is deprecated, and it is recommended you use the functionality from-the *[singletons][]* package instead.  `natsVal` is `fromSing`, `reifyNats` is-`toSing`/`withSomeSing`, `sameNats` is simply `%~`, and you can traverse/reify-singletons of lists too:--~~~haskell-printNats :: forall (ns :: [Nat]). Sing ns -> IO ()-printNats ss = case ss of-                 SNil             ->-                   return ()-                 s `SCons` ss' -> do-                   print $ fromSing s-                   printNats ss'-~~~-

@@ -9,8 +9,6 @@  -- | -- Module      : GHC.TypeLits.Compare--- Description : Tools and singletons for proving and refining inequalities---               and bounds on GHC TypeLits types using '<=' and '<=?' -- Copyright   : (c) Justin Le 2016 -- License     : MIT -- Maintainer  : justin@jle.im@@ -26,7 +24,7 @@ -- @'KnownNat' n@ is available: -- -- @--- foo :: (KnownNat n, 1 '<=' n) => 'Proxy' n -> Int+-- foo :: (KnownNat n, 1 '<=' n) => 'Data.Proxy.Proxy' n -> Int -- -- bar :: KnownNat n => Proxy n -> Int -- bar n = case (Proxy :: Proxy 1) '%<=?' n of@@ -35,7 +33,7 @@ -- @ -- -- @foo@ requires that @1 <= n@, but @bar@ has to handle all cases of @n@.--- @%<=?@ lets you compare the 'KnownNat's in two 'Proxy's and returns+-- @%<=?@ lets you compare the 'KnownNat's in two 'Data.Proxy.Proxy's and returns -- a @:<=?@, which has two constructors, 'LE' and 'NLE'. -- -- If you pattern match on the result, in the 'LE' branch, the constraint@@ -73,7 +71,9 @@ -- with '<=?' (useful for when you have to work with libraries that mix the -- two methods) or 'cmpNatEq' and 'eqCmpNat' to get to/from witnesses for -- equality of the two 'Nat's.-+--+-- 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 '<=?'     (:<=?)(..)@@ -89,8 +89,8 @@   , cmpNatEq   , eqCmpNat   , reflCmpNat-    -- ** Interfacing with '<=?'   , cmpNatLE+  , cmpNatGOrdering   )   where @@ -98,7 +98,11 @@ import           Data.Type.Equality import           GHC.TypeLits import           Unsafe.Coerce+import           Data.GADT.Compare +-- | 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@@ -108,6 +112,9 @@              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@@ -117,10 +124,13 @@     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) +-- | Compare @m@ and @n@, classifying their relationship into some+-- constructor of ':<=?'. (%<=?)      :: (KnownNat m, KnownNat n)      => p m@@ -129,11 +139,14 @@ 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 +-- | Compare @m@ and @n@, classifying their relationship into some+-- constructor of 'SCmpNat'. cmpNat     :: (KnownNat m, KnownNat n)     => p m@@ -144,21 +157,36 @@                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) +-- | @'CmpNat' m n@ being 'EQ' implies that @m@ is equal to @n@. cmpNatEq :: (CmpNat m n :~: 'EQ) -> (m :~: n) cmpNatEq = \case Refl -> unsafeCoerce Refl +-- | A witness of equality implies that @'CmpNat' m n@ is 'Eq'. eqCmpNat :: (m :~: n) -> (CmpNat m n :~: 'EQ) eqCmpNat = \case Refl -> unsafeCoerce Refl +-- | Inject a witness of equality into an 'SCmpNat' at 'CEQ'. reflCmpNat :: (m :~: n) -> SCmpNat m n reflCmpNat r = CEQ (eqCmpNat r) r +-- | 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)++-- | 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+

@@ -1,503 +0,0 @@-{-# LANGUAGE ConstraintKinds      #-}-{-# LANGUAGE FlexibleContexts     #-}-{-# LANGUAGE GADTs                #-}-{-# LANGUAGE KindSignatures       #-}-{-# LANGUAGE LambdaCase           #-}-{-# LANGUAGE PolyKinds            #-}-{-# LANGUAGE RankNTypes           #-}-{-# LANGUAGE ScopedTypeVariables  #-}-{-# LANGUAGE StandaloneDeriving   #-}-{-# LANGUAGE TypeFamilies         #-}-{-# LANGUAGE TypeInType           #-}-{-# LANGUAGE TypeOperators        #-}-{-# LANGUAGE UndecidableInstances #-}---- |--- Module      : GHC.TypeLits.List--- Description : Typeclasses, singletons, and reifiers for type-level lists---               of 'Nat's and 'Symbol's.--- Copyright   : (c) Justin Le 2016--- License     : MIT--- Maintainer  : justin@jle.im--- Stability   : unstable--- Portability : non-portable--------- Provides the 'KnownNats' and 'KnownSymbols' typeclasses in analogy to--- 'KnownNat' and 'KnownSymbol' from "GHC.TypeLits".  Also provides--- singleton-esque structures for traversing over type-level lists of--- 'Nat's and 'Symbol's.  Comes with continuation-style reifiers and--- existential types for dependent typing usage, and as an analogy with--- 'SomeNat' and 'SomeSymbol'.------ See typeclass documentations and README for more information.--module GHC.TypeLits.List-  {-# DEPRECATED "Use singletons package instead" #-} (-  -- * 'KnownNats'-    KnownNats(..)-  , SomeNats(..)-  , NatList(..)-  , someNatsVal-  , someNatsValPos-  , reifyNats-  , reifyNats'-  , sameNats-  , elimNatList-  -- ** Traversals-  , traverseNatList-  , traverseNatList'-  , traverseNatList_-  -- *** Maps-  , mapNatList-  , mapNatList'-  -- * 'KnownSymbols'-  , KnownSymbols(..)-  , SomeSymbols(..)-  , SymbolList(..)-  , someSymbolsVal-  , reifySymbols-  , sameSymbols-  , elimSymbolList-  -- ** Traversals-  , traverseSymbolList-  , traverseSymbolList'-  , traverseSymbolList_-  -- *** Maps-  , mapSymbolList-  , mapSymbolList'-  ) where--import           Data.Functor.Identity-import           Data.Kind-import           Data.Proxy-import           Data.Reflection-import           Data.Type.Equality-import           GHC.TypeLits----- | @'KnownNats' ns@ is intended to represent that every 'Nat' in the--- type-level list 'ns' is itself a 'KnownNat' (meaning, you can use--- 'natVal' to get its corresponding 'Integer').------ In practice, just knowing that every item has a 'KnownNat' instance is--- not enough; it's nice, but unless you're able to "iterate" over every--- 'Nat' in the list, it's of limited use.  That's why this class also--- provides a constructor for @'NatList' ns@, so that you can produce--- a 'NatList' for every @'KnownNat' ns@, which you can iterate over to get--- @'Proxy' n@s for every 'n' in 'ns' along with the @'KnownNat' n@--- instances.------ It also has an analogy to 'natVal', 'natsVal', which lets you get a list--- of the represented 'Integer's for, say, @'Proxy' [1,2,3]@.------ __Deprecated:__ Use 'SingI' from /singletons/ instead.-class KnownNats (ns :: [Nat]) where-    -- | __Deprecated:__ Use 'fromSing' from /singletons/ instead.-    natsVal  :: p ns -> [Integer]-    -- | __Deprecated:__ Use 'sing' from /singletons/ instead.-    natsList :: NatList ns-{-# DEPRECATED KnownNats "Use SingI from the singletons package instead" #-}-{-# DEPRECATED natsVal "Use fromSing from the singletons package instead" #-}-{-# DEPRECATED natsList "Use sing from the singletons package instead" #-}--instance KnownNats '[] where-    natsVal  _ = []-    natsList   = ØNL--instance (KnownNat n, KnownNats ns) => KnownNats (n ': ns) where-    natsVal  _ = natVal (Proxy :: Proxy n) : natsVal (Proxy :: Proxy ns)-    natsList   = Proxy :<# natsList---- | Represents unknown type-level lists of type-level natural numbers.--- It's a 'NatList', but you don't know what the list contains at--- compile-time.------ __Deprecated:__ Use 'SomeSing' from /singletons/ instead.-data SomeNats :: Type where-    SomeNats :: KnownNats ns => !(NatList ns) -> SomeNats-{-# DEPRECATED SomeNats "Use SomeSing from the singletons package instead" #-}---- | Singleton-esque type for "traversing" over type-level lists of 'Nat's.--- Essentially contains a (value-level) list of @'Proxy' n@s, but each 'n'--- has a 'KnownNat' instance for you to use.  At runtime (after type--- erasure), is more or less equivalent to a @['Integer']@.------ Typically generated using 'natsList'.------ __Deprecated:__ Use 'Sing' from /singletons/ instead.-data NatList :: [Nat] -> Type where-    ØNL   :: NatList '[]-    (:<#) :: (KnownNat n, KnownNats ns)-          => !(Proxy n) -> !(NatList ns) -> NatList (n ': ns)-{-# DEPRECATED NatList "Use Sing from the singletons package instead" #-}--infixr 5 :<#-deriving instance Show (NatList ns)---- | Utility function for traversing over all of the @'Proxy' n@s in--- a 'NatList', each with the corresponding 'KnownNat' instance available.--- Gives the the ability to "change" the represented natural number to--- a new one, in a 'SomeNat'.------ Can be considered a form of a @Traversal' 'SomeNats' 'SomeNat'@.-traverseNatList-    :: forall f ns. Applicative f-    => (forall n. KnownNat n => Proxy n -> f SomeNat)-    -> NatList ns-    -> f SomeNats-traverseNatList f = go-  where-    go :: forall ms. NatList ms -> f SomeNats-    go = \case-      ØNL      -> pure $ SomeNats ØNL-      n :<# ns -> merge <$> f n <*> go ns-    merge :: SomeNat -> SomeNats -> SomeNats-    merge = \case-      SomeNat n -> \case-        SomeNats ns ->-          SomeNats (n :<# ns)---- | Like 'traverseNatList', but literally actually a @Traversal'--- 'SomeNats' 'SomeNat'@, avoiding the Rank-2 types, so is usable with--- lens-library machinery.-traverseNatList'-    :: forall f. Applicative f-    => (SomeNat -> f SomeNat)-    -> SomeNats-    -> f SomeNats-traverseNatList' f = \case-    SomeNats ns -> traverseNatList (f . SomeNat) ns---- | Utility function for traversing over all of the @'Proxy' n@s in--- a 'NatList', each with the corresponding 'KnownNat' instance available.--- Results are ignored.-traverseNatList_-    :: forall f a ns. Applicative f-    => (forall n. KnownNat n => Proxy n -> f a)-    -> NatList ns-    -> f ()-traverseNatList_ f = go-  where-    go :: forall ms. NatList ms -> f ()-    go = \case-      ØNL       -> pure ()-      n :<# ns -> f n *> go ns---- | The "eliminator" for 'NatList'.  You can think of this as--- a dependently typed analogy for a fold.------ /Since 0.2.1.0/-elimNatList-    :: forall p ns. ()-    => p '[]-    -> (forall m ms. (KnownNat m, KnownNats ms) => Proxy m -> p ms -> p (m ': ms))-    -> NatList ns-    -> p ns-elimNatList z s = \case-    ØNL      -> z-    n :<# ns -> s n (elimNatList z s ns)----- | Utility function for \"mapping\" over each of the 'Nat's in the--- 'NatList'.-mapNatList-    :: (forall n. KnownNat n => Proxy n -> SomeNat)-    -> NatList ns-    -> SomeNats-mapNatList f = runIdentity . traverseNatList (Identity . f)---- | Like 'mapNatList', but avoids the Rank-2 types, so can be used with--- '.' (function composition) and in other situations where 'mapNatList'--- would cause problems.-mapNatList'-    :: (SomeNat -> SomeNat)-    -> SomeNats-    -> SomeNats-mapNatList' f = runIdentity . traverseNatList' (Identity . f)---- | List equivalent of 'someNatVal'.  Convert a list of integers into an--- unknown type-level list of naturals.  Will return 'Nothing' if any of--- the given 'Integer's is negative.------ __Deprecated:__ Use 'toSing' from /singletons/ instead.-someNatsVal :: [Integer] -> Maybe SomeNats-someNatsVal []     = Just (SomeNats ØNL)-someNatsVal (n:ns) = do-    SomeNat  m  <- someNatVal n-    SomeNats ms <- someNatsVal ns-    return $ SomeNats (m :<# ms)-{-# DEPRECATED someNatsVal "Use toSing from the singletons package instead" #-}---- | List equivalent of 'reifyNat'.  Given a list of integers, takes--- a function in an "environment" with a @'NatList' ns@ corresponding to--- the given list, where every @n@ in @ns@ has a 'KnownNat' instance.------ Essentially a continuation-style version of 'SomeNats'.------ Be aware that this also produces @'KnownNat' n@s where @n@ is negative,--- without complaining.  To be consistent, within the library, this--- /should/ be called @reifyNatsPos@; however, the naming choice is for--- consistency with 'reifyNat' from the /reflections/ package.  Use--- 'reifyNats'' for a "safe" version.------ __Deprecated:__ Use 'withSomeSing' from /singletons/ instead.-reifyNats :: [Integer] -> (forall ns. KnownNats ns => NatList ns -> r) -> r-reifyNats []     f = f ØNL-reifyNats (n:ns) f = reifyNat n $ \m ->-                       reifyNats ns $ \ms ->-                         f (m :<# ms)-{-# DEPRECATED reifyNats "Use withSomeSing from the singletons package instead" #-}---- | "Safe" version of 'reifyNats', which will only run the continuation if--- every 'Integer' in the list is non-negative.  If not, then returns--- the given "default" value instead.------ __Deprecated:__ Use 'withSomeSing' from /singletons/ instead.-reifyNats'-    :: [Integer]-    -> r-    -> (forall ns. KnownNats ns => NatList ns -> r)-    -> r-reifyNats' ns d f =-    case someNatsVal ns of-      Just (SomeNats ms) -> f ms-      Nothing            -> d-{-# DEPRECATED reifyNats' "Use withSomeSing from the singletons package instead" #-}---- | Like 'someNatsVal', but will also go ahead and produce 'KnownNat's--- whose integer values are negative.  It won't ever error on producing--- them, but extra care must be taken when using the produced 'SomeNat's.------ __Deprecated:__ Use 'toSing' from /singletons/ instead.-someNatsValPos :: [Integer] -> SomeNats-someNatsValPos ns = reifyNats ns SomeNats-{-# DEPRECATED someNatsValPos "Use toSing from the singletons package instead" #-}---- | Get evidence that the two 'KnownNats' lists are actually the "same"--- list of 'Nat's (that they were instantiated with the same numbers).------ Essentialy runs 'sameNat' over the lists:------ @--- case 'sameNats' ns ms of---   Just 'Refl' -> -- in this branch, GHC recognizes that the two ['Nat']s---                  -- are the same.---   Nothing   -> -- in this branch, they aren't--- @------ __Deprecated:__ Use '%~' from /singletons/ instead.-sameNats-    :: NatList ns-    -> NatList ms-    -> Maybe (ns :~: ms)-sameNats = \case-    ØNL      -> \case-      ØNL      -> Just Refl-      _ :<# _  -> Nothing-    n :<# ns -> \case-      ØNL      -> Nothing-      m :<# ms -> do-        Refl <- sameNat n m-        Refl <- sameNats ns ms-        return Refl-{-# DEPRECATED sameNats "Use (%~) from the singletons package instead" #-}----- | @'KnownSymbols' ss@ is intended to represent that every 'Symbol' in the--- type-level list 'ss' is itself a 'KnownSymbol' (meaning, you can use--- 'symbolVal' to get its corresponding 'String').------ You can use 'symbolsVal' to get the corresponding @['String']@ from--- @'KnownSymbols' ss@.------ For reasons discussed further in the documentation for 'KnownNats', this--- also lets you generate a @'SymbolList' ss@, in order to iterate over the--- type-level list of 'Symbol's and take advantage of their 'KnownSymbol'--- instances.------ __Deprecated:__ Use 'SingI from /singletons/ instead.-class KnownSymbols (ss :: [Symbol]) where-    -- | __Deprecated:__ Use 'fromSing' from /singletons/ instead.-    symbolsVal  :: p ss -> [String]-    -- | __Deprecated:__ Use 'sing from /singletons/ instead.-    symbolsList :: SymbolList ss-{-# DEPRECATED KnownSymbols "Use SingI from the singletons package instead" #-}-{-# DEPRECATED symbolsVal "Use fromSing from the singletons package instead" #-}-{-# DEPRECATED symbolsList "Use sing from the singletons package instead" #-}--instance KnownSymbols '[] where-    symbolsVal  _ = []-    symbolsList    = ØSL--instance (KnownSymbol s, KnownSymbols ss) => KnownSymbols (s ': ss) where-    symbolsVal  _ = symbolVal (Proxy :: Proxy s) : symbolsVal (Proxy :: Proxy ss)-    symbolsList   = Proxy :<$ symbolsList---- | Represents unknown type-level lists of 'Symbol's. It's a 'SymbolList',--- but you don't know what the list contains at compile-time.------ __Deprecated:__ Use 'SomeSing' from /singletons/ instead.-data SomeSymbols :: Type where-    SomeSymbols :: KnownSymbols ss => !(SymbolList ss) -> SomeSymbols-{-# DEPRECATED SomeSymbols "Use SomeSing from the singletons package instead" #-}---- | Singleton-esque type for "traversing" over type-level lists of--- 'Symbol's. Essentially contains a (value-level) list of @'Proxy' n@s,--- but each 'n' has a 'KnownSymbol' instance for you to use.  At runtime--- (after type erasure), is more or less equivalent to a @['String']@.------ Typically generated using 'symbolsList'.------ __Deprecated:__ Use 'Sing' from /singletons/ instead.-data SymbolList :: [Symbol] -> Type where-    ØSL   :: SymbolList '[]-    (:<$) :: (KnownSymbol s, KnownSymbols ss)-          => !(Proxy s) -> !(SymbolList ss) -> SymbolList (s ': ss)-{-# DEPRECATED SymbolList "Use Sing from the singletons package instead" #-}--infixr 5 :<$-deriving instance Show (SymbolList ns)---- | Utility function for traversing over all of the @'Proxy' s@s in--- a 'SymbolList', each with the corresponding 'KnownSymbol' instance--- available.  Gives the the ability to "change" the represented natural--- number to a new one, in a 'SomeSymbol'.------ Can be considered a form of a @Traversal' 'SomeSymbols' 'SomeSymbol'@.-traverseSymbolList-    :: forall f ss. Applicative f-    => (forall s. KnownSymbol s => Proxy s -> f SomeSymbol)-    -> SymbolList ss-    -> f SomeSymbols-traverseSymbolList f = go-  where-    go :: forall ms. SymbolList ms -> f SomeSymbols-    go = \case-      ØSL      -> pure $ SomeSymbols ØSL-      s :<$ ss -> merge <$> f s <*> go ss-    merge :: SomeSymbol -> SomeSymbols -> SomeSymbols-    merge = \case-      SomeSymbol s -> \case-        SomeSymbols ss ->-          SomeSymbols (s :<$ ss)---- | Like 'traverseSymbolList', but literally actually a--- @Traversal' 'SomeSymbols' 'SomeSymbol'@, avoiding the Rank-2 types, so--- is usable with lens-library machinery.-traverseSymbolList'-    :: forall f. Applicative f-    => (SomeSymbol -> f SomeSymbol)-    -> SomeSymbols-    -> f SomeSymbols-traverseSymbolList' f = \case-    SomeSymbols ns' -> traverseSymbolList (f . SomeSymbol) ns'---- | Utility function for traversing over all of the @'Proxy' s@s in--- a 'SymbolList', each with the corresponding 'KnownSymbol' instance--- available. Results are ignored.-traverseSymbolList_-    :: forall f ss. Applicative f-    => (forall s a. KnownSymbol s => Proxy s -> f a)-    -> SymbolList ss-    -> f ()-traverseSymbolList_ f = go-  where-    go :: forall ts. SymbolList ts -> f ()-    go = \case-      ØSL      -> pure ()-      s :<$ ss -> f s *> go ss---- | Utility function for \"mapping\" over each of the 'Symbol's in the--- 'SymbolList'.-mapSymbolList-    :: (forall s. KnownSymbol s => Proxy s -> SomeSymbol)-    -> SymbolList ss-    -> SomeSymbols-mapSymbolList f = runIdentity . traverseSymbolList (Identity . f)---- | Like 'mapSymbolList', but avoids the Rank-2 types, so can be used with--- '.' (function composition) and in other situations where 'mapSymbolList'--- would cause problems.-mapSymbolList'-    :: (SomeSymbol -> SomeSymbol)-    -> SomeSymbols-    -> SomeSymbols-mapSymbolList' f = runIdentity . traverseSymbolList' (Identity . f)---- | The "eliminator" for 'SymbolList'.  You can think of this as--- a dependently typed analogy for a fold.------ /Since 0.2.1.0/-elimSymbolList-    :: forall p ss. ()-    => p '[]-    -> (forall t ts. (KnownSymbol t, KnownSymbols ts) => Proxy t -> p ts -> p (t ': ts))-    -> SymbolList ss-    -> p ss-elimSymbolList z s = \case-    ØSL      -> z-    n :<$ ns -> s n (elimSymbolList z s ns)----- | List equivalent of 'someNatVal'.  Convert a list of integers into an--- unknown type-level list of naturals.  Will return 'Nothing' if any of--- the given 'Integer's is negative.------ __Deprecated:__ Use 'toSing' from /singletons/ instead.-someSymbolsVal :: [String] -> SomeSymbols-someSymbolsVal []     = SomeSymbols ØSL-someSymbolsVal (s:ss) =-    case someSymbolVal s of-      SomeSymbol t ->-        case someSymbolsVal ss of-          SomeSymbols ts ->-            SomeSymbols (t :<$ ts)-{-# DEPRECATED someSymbolsVal "Use toSing from the singletons package instead" #-}---- | List equivalent of 'reifyNat'.  Given a list of integers, takes--- a function in an "environment" with a @'SymbolList' ss@ corresponding to--- the given list, where every @s@ in @ss@ has a 'KnownSymbol' instance.------ Essentially a continuation-style version of 'SomeSymbols'.------ __Deprecated:__ Use 'withSomeSing' from /singletons/ instead.-reifySymbols :: [String]-             -> (forall ss. KnownSymbols ss => SymbolList ss -> r)-             -> r-reifySymbols []     f = f ØSL-reifySymbols (s:ss) f = reifySymbol s $ \t ->-                          reifySymbols ss $ \ts ->-                            f (t :<$ ts)-{-# DEPRECATED reifySymbols "Use withSomeSing from the singletons package instead" #-}----- | Get evidence that the two 'KnownSymbols' lists are actually the "same"--- list of 'Symboles's (that they were instantiated with the same strings).------ Essentialy runs 'sameSymbol' over the lists:------ @--- case 'sameSymbols' ns ms of---   Just 'Refl' -> -- in this branch, GHC recognizes that the---                  -- two ['Symbol']s are the same---   Nothing   -> -- in this branch, they aren't--- @------ __Deprecated:__ Use '%~' from /singletons/ instead.-sameSymbols-    :: SymbolList ns-    -> SymbolList ms-    -> Maybe (ns :~: ms)-sameSymbols = \case-    ØSL      -> \case-      ØSL      -> Just Refl-      _ :<$ _  -> Nothing-    s :<$ ss -> \case-      ØSL      -> Nothing-      t :<$ ts -> do-        Refl <- sameSymbol s t-        Refl <- sameSymbols ss ts-        return Refl-{-# DEPRECATED sameSymbols "Use (%~) from the singletons package instead" #-}-

@@ -1,307 +1,434 @@-{-# LANGUAGE CPP                 #-}-{-# LANGUAGE ConstraintKinds     #-}-{-# LANGUAGE FlexibleContexts    #-}-{-# LANGUAGE PolyKinds           #-}-{-# LANGUAGE RankNTypes          #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TypeOperators       #-}-#if __GLASGOW_HASKELL__ >= 806-{-# LANGUAGE NoStarIsType #-}-#endif+{-# LANGUAGE ConstraintKinds           #-}+{-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE FlexibleContexts          #-}+{-# LANGUAGE GADTs                     #-}+{-# LANGUAGE LambdaCase                #-}+{-# LANGUAGE PatternSynonyms           #-}+{-# LANGUAGE RankNTypes                #-}+{-# LANGUAGE ScopedTypeVariables       #-}+{-# LANGUAGE StandaloneDeriving        #-}+{-# LANGUAGE TypeInType                #-}+{-# LANGUAGE TypeOperators             #-}+{-# LANGUAGE ViewPatterns              #-}  -- | -- Module      : GHC.TypeLits.Witnesses--- Description : Instance witnesses for various arithmetic operations on---               GHC TypeLits. -- Copyright   : (c) Justin Le 2016 -- License     : MIT -- Maintainer  : justin@jle.im -- Stability   : unstable -- Portability : non-portable ----- This module provides witnesses for instances that result from the--- various arithmetic operations on GHC TypeLits 'Nat' types.  In general,--- if you have @'KnownNat' n@, GHC can't infer @'KnownNat' (n + 1)@; and if--- you have @'KnownNat' m@, as well, GHC can't infer @'KnownNat' (n + m)@.+-- This module essentially provides a lightweight subset of the+-- /singletons/ library specifically for 'Nat' and 'Symbol', from+-- "GHC.TypeLits". ----- This can be extremely annoying when dealing with libraries and--- applications where one regularly adds and subtracts type-level nats and--- expects 'KnownNat' instances to follow.  For example, vector--- concatenation of length-encoded vector types can be:+-- Its main functionality is for first-class manipulation of 'KnownNat' and+-- 'KnownSymbol' constraints.  For example, in general, if you have+-- @'KnownNat' n@, GHC can't infer @'KnownNat' (n + 1)@.  And, if you have+-- both @'KnownNat' n@ and @'KnownNat' m@, GHC can't infer @'KnownNat (n+-- + m)@. --+-- This can be annoying when dealing with libraries and applications where+-- one regularly adds and subtracts type-level nats and expects 'KnownNat'+-- instances to follow.  For example, vector concatenation of+-- length-encoded vector types can be:+-- -- @ -- concat :: ('KnownNat' n, 'KnownNat' m) => Vector n a -> Vector m a -> Vector (n + m) a -- @ -- -- But, now @n + m@ does not have a 'KnownNat' instance...which makes--- operations like this extremely less useful!+-- operations like this much less useful. ----- At the highest level, this module can be used with 'withNatOp':+-- Usually, the easiest way to get around this is to use a typechecker+-- plugin, like+-- <https://hackage.haskell.org/package/ghc-typelits-knownnat>.  However,+-- we can do this without the help of a typechecker plugin using+-- first-class values, at the cost of some increased verbosity. --+-- We introduce @'SNat' n@, which is a term-level witness of knownnat-ness+-- that can be manipulated as a first-class value.+--+-- If we have @'KnownNat' n@, we can construct an @'SNat' n@:+-- -- @--- getDoubled :: forall n. 'KnownNat' n => 'Proxy' n -> 'Integer'--- getDoubled p = 'withNatOp' ('%*') p ('Proxy' :: 'Proxy' 2) $---     natVal ('Proxy' :: 'Proxy' (n * 2))+-- 'SNat' :: KnownNat n -> SNat n -- @ ----- With the final argument of 'withNatOp', you can provide a result--- computed in an environment where @n * 2@ is indeed an instance of--- 'KnownNat'.------ For more complex usage, you can directly manipulate witnesses and then--- use them via pattern matching:+-- Furthermore, if we have an @'SNat' n@, we can /pattern match/ on the+-- 'SNat' constructor to get a @'KnownNat' n@ constraint: -- -- @--- let pn = 'natDict' ('Proxy' :: 'Proxy' n)---     p1 = 'natDict' ('Proxy' :: 'Proxy' 1)---     p2 = 'natDict' ('Proxy' :: 'Proxy' 2)--- in  case pn '%*' p2 '%+' p1 of---       'Dict' -> 'natVal' ('Proxy' :: 'Proxy' (n * 2 + 1))+-- myFunc :: SNat n -> Bool+-- myFunc SNat = ...  -- in this body, we have `KnownNat n` -- @ ----- In the branch of the case statement, @n * 2 + 1@ indeed has a 'KnownNat'--- instance.+-- So if we have @'KnownNat' n@ and @'KnownNat' m@, we can get @'KnownNat'+-- (n + m)@ by using '%+', which adds together 'SNat's: ----- Note that the operators have appropriate fixities to mimic value-level--- arithmetic operations.+-- @+-- case (SNat :: SNat n) %+ (SNat :: SNat m) of+--   SNat -> -- in this branch, we have `KnownNat (n + m)`+-- @ ----- __WARNING__: '%-' and 'entailSub' are is implemented in a way such--- that /negative/ 'KnownNat's are produced without any errors.  The--- production of witnesses and entailments will hold, but be aware that any--- functions that rely on 'KnownNat' instances to be non-negative can--- potentially break.+-- Note that this module converts between 'SNat' and 'Natural', and not+-- 'SNat' and 'Integer', in "GHC.TypeNats"-style. -----module GHC.TypeLits.Witnesses-  {-# DEPRECATED "Use singletons package instead" #-} (-  -- * Singletons-  -- $singletons-  -- * High level wrapper-    withNatOp-  -- * Direct witnesses-  , natDict-  , dictNatVal-  -- * Witness generators+-- Of course, all of this functionality is provided by the /singletons/+-- library, in "Data.Singletons.TypeLits".  This module can be useful if+-- you want a lightweight alternative without the full might of+-- /singletons/.  The main benefit of the /singletons/ library is providing+-- a unified interface for singletons of /all/ different kinds/types, and+-- not just 'Natural' and 'String'.+module GHC.TypeLits.Witnesses (+  -- * Nats+    SNat(..)+  , SomeNat(SomeNat_)+  , Natural(FromSNat)+  , fromSNat+  , withKnownNat+  , withSomeNat+  , toSomeNat+  -- ** Operations   , (%+)   , (%-)+  , minusSNat+  , minusSNat_   , (%*)   , (%^)-  -- * Entailments-  , entailAdd-  , entailSub-  , entailMul-  , entailExp+  -- ** Compare+  , (%<=?)+  , sCmpNat+  -- ** Unsafe+  , unsafeLiftNatOp1+  , unsafeLiftNatOp2+  -- * Symbols+  , SSymbol(..)+  , SomeSymbol(SomeSymbol_)+  , pattern FromSSymbol+  , fromSSymbol+  , withKnownSymbol+  , withSomeSymbol+  , toSomeSymbol   ) where -import           Data.Constraint+import           Data.GADT.Compare+import           Data.GADT.Show import           Data.Proxy-import           Data.Reflection-import           GHC.TypeLits+import           Data.Type.Equality+import           GHC.Natural+import           GHC.TypeLits hiding         (natVal, someNatVal)+import           GHC.TypeLits.Compare hiding ((%<=?))+import           GHC.TypeNats import           Unsafe.Coerce+import qualified GHC.TypeLits.Compare        as Comp --- $singletons------ All of the functionality in this module can be subsumed by the--- /singletons/ package, by utilizing:------   * "Data.Singletons"---   * "Data.Singletons.TypeLits"---   * "Data.Singletons.Prelude.Num"------ This module is left in this package as an alternative for those who--- might, for some reason, not want to add a /singletons/ dependency to--- their project.  However, if you do much at the type level, using the--- /singletons/ library is much preferred, as it provides a unifed--- interface for all of the functionality here, generalized to other kinds--- besides 'Nat'.------ For all functions in this module, a /singletons/ equivalent is included--- for help migrating.------ In general:---------   * The /singletons/ type @'Sing' n@ (or its equivalent, @'SNat' n@)---     subsumes both @'Proxy' n@ and @'Dict' ('KnownNat' n)@.  You can---     replace both @'Proxy' n@ and @'Dict' ('KnownNat' n)@ with @'SNat' n@---     to move to singletons style.------   * 'dictNatVal' and 'natVal' are both just 'fromSing'.------   * Replace '%+', '%-', and '%*' with their /singletons/---     equivalents, '%:+', '%:-', and '%:*' from---     "Data.Singletons.Prelude.Num".  Note that the current version of---     /singletons/ does not have an equivalent for '%^'.+-- | An @'SNat' n@ is a witness for @'KnownNat' n@. -----   * Use 'withKnownNat' from /singletons/ (or just pattern match on---     'SNat') to get a 'KnownNat' instance from a @'SNat' n@, the same way---     you'd get one from a 'Dict'.+-- This means that if you pattern match on the 'SNat' constructor, in that+-- branch you will have a @'KnownNat' n@ constraint. -----   * The high-level combinator 'withNatOp' can simply be replaced with---     applying your singleton functions ('%+' etc.) to 'SNat' values, and---     pattern matching on the result, or using 'withKnownNat' on the result.+-- @+-- myFunc :: SNat n -> Bool+-- myFunc SNat = ...  -- in this body, we have `KnownNat n`+-- @ --+-- This is essentially a singleton for 'Nat', and stands in for the+-- /singletons/ 'SNat' and 'Data.Singleton.Sing' types.+data SNat n = KnownNat n => SNat --- | Create a 'Dict' witness for @'KnownNat' n@.------ Not necessary with /singletons/, as @'SNat' n@ stands in for both--- @'Proxy' n@ and @'Dict' ('KnownNat' n)@.-natDict :: KnownNat n => p n -> Dict (KnownNat n)-natDict _ = Dict+deriving instance Eq (SNat n)+deriving instance Ord (SNat n) --- | Get the 'Integer' from the 'KnownNat' instance witnessed by the--- 'Dict'.------ With /singletons/, this is 'fromSing', which takes an @'SNat' n@ and--- returns an 'Integer'.-dictNatVal :: forall n. Dict (KnownNat n) -> Integer-dictNatVal Dict = natVal (Proxy :: Proxy n)+instance Show (SNat n) where+    showsPrec d x@SNat = showParen (d > 10) $+      showString "SNat @" . showsPrec 11 (fromSNat x) -infixl 6 %+-infixl 6 %--infixl 7 %*-infixr 8 %^+instance GShow SNat where+    gshowsPrec = showsPrec --- | Given witnesses for @'KnownNat' n@ and @'KnownNat' m@, generates--- a witness for @'KnownNat' (n + m)@.+instance TestEquality SNat where+    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++instance GCompare SNat where+    gcompare x = cmpNatGOrdering . sCmpNat x++data SomeNat__ = forall n. SomeNat__ (SNat n)++-- | A useful pattern synonym for matching on a 'SomeNat' as if it+-- contained an @'SNat' n@, and not a @'Proxy' n@ as it exists in+-- "GHC.TypeLits". ----- Follows proper association and fixity for usage with other similar--- operators.+-- A layer of compatibility letting us use the original 'SomeNat' type in+-- a way that works well with 'SNat'. ----- With /singletons/, this is '%:+' from "Data.Singletons.Prelude.Num".-(%+) :: forall n m. Dict (KnownNat n) -> Dict (KnownNat m) -> Dict (KnownNat (n + m))-Dict %+ Dict = mapDict entailAdd (Dict :: Dict (KnownNat n, KnownNat m))+-- 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)+  where+    SomeNat_ (SNat :: SNat n) = SomeNat (Proxy :: Proxy n)+{-# COMPLETE SomeNat_ #-} --- | Given witnesses for @'KnownNat' n@ and @'KnownNat' m@, generates--- a witness for @'KnownNat' (n - m)@.+-- | A useful pattern synonym for matching on a 'Natural' as if it "were"+-- a 'SNat': ----- Note that this is implemented in a way such that /negative/ 'KnownNat's--- are produced without any errors.+-- @+-- myFunc :: Natural -> Bool+-- myFunc (FromSNat x) = ...  -- x is `SNat n`, with `n` coming from the input+-- @ ----- Follows proper association and fixity for usage with other similar--- operators.+-- It can be used as a function, as well, to convert an @'SNat' n@ back+-- into the 'Natural' that it represents. ----- With /singletons/, this is '%:-' from "Data.Singletons.Prelude.Num".-(%-) :: forall n m. Dict (KnownNat n) -> Dict (KnownNat m) -> Dict (KnownNat (n - m))-Dict %- Dict = mapDict entailSub (Dict :: Dict (KnownNat n, KnownNat m))+-- 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)+  where+    FromSNat = fromSNat+{-# COMPLETE FromSNat #-} --- | Given witnesses for @'KnownNat' n@ and @'KnownNat' m@, generates--- a witness for @'KnownNat' (n * m)@.+-- | Given an @'SNat' n@ and a value that would require a @'KnownNat' n@+-- instance, create that value. ----- Follows proper association and fixity for usage with other similar--- operators.+-- This stands in for the function of the same name from+-- "Data.Singletons.TypeLits".+withKnownNat :: SNat n -> (KnownNat n => r) -> r+withKnownNat SNat x = x++-- | Promote ("reify") a 'Natural' to an @'SNat' n@, by providing+-- a continuation that would handle it in a way that is polymorphic over+-- all possible @n@. ----- With /singletons/, this is '%:*' from "Data.Singletons.Prelude.Num".-(%*) :: forall n m. Dict (KnownNat n) -> Dict (KnownNat m) -> Dict (KnownNat (n * m))-Dict %* Dict = mapDict entailMul (Dict :: Dict (KnownNat n, KnownNat m))+-- 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) --- | Given witnesses for @'KnownNat' n@ and @'KnownNat' m@, generates--- a witness for @'KnownNat' (n ^ m)@.+-- | Promote ("reify") a 'Natural' to an @'SNat' n@ existentially hidden+-- inside a 'SomeNat'.  To use it, pattern match using 'SomeNat_'. ----- Follows proper association and fixity for usage with other similar--- operators.-(%^) :: forall n m. Dict (KnownNat n) -> Dict (KnownNat m) -> Dict (KnownNat (n ^ m))-Dict %^ Dict = mapDict entailExp (Dict :: Dict (KnownNat n, KnownNat m))+-- This stands in the /singletons/ 'Data.Singleton.toSomeSing' function.+toSomeNat :: Natural -> SomeNat+toSomeNat = someNatVal --- | A high-level the interface of this module.  Give it one of--- the witness-generating operators on 'KnownNat's in this module ('%+',--- '%-', '%*', or '%^'), two 'Proxy's containing the 'KnownNat's to--- be modified, and receive an environment where the result of the--- operation (applied to the 'KnownNat's) has a 'KnownNat' instance.+-- | Convert ("reflect") an 'SNat' back into the 'Natural' it represents. ----- For example, with+-- This stands in the /singletons/ 'Data.Singleton.fromSing' function.+fromSNat :: SNat n -> Natural+fromSNat x@SNat = natVal x++-- | Lift a unary operation to act on an @'SNat' n@ that returns an @'SNat'+-- m@.  The function given must properly describe the relationship between+-- @n@ and @m@. --+-- For example:+-- -- @--- 'withNatOp' ('%+') ('Proxy' :: 'Proxy' n) ('Proxy' :: 'Proxy' 1) r+-- double :: SNat n -> SNat (n * 2)+-- double = unsafeLiftNatOp1 (*2) -- @ ----- in @r@, @n + 1@ has a 'KnownNat' instance:+-- 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 f x = withSomeNat (f (fromSNat x)) unsafeCoerce++-- | Lift a binary operation to act on an @'SNat' n@ and @'SNat' m@ that+-- returns an @'SNat' o@.  The function given must properly describe the+-- relationship between @n@, @m@, and @o@. --+-- For example:+-- -- @--- 'withNatOp' ('%+') ('Proxy' :: 'Proxy' n) ('Proxy' :: 'Proxy' 1) $---     'natVal' ('Proxy' :: 'Proxy' (n + 1))--- -- => will return the 'Integer' correpsonding to n + 1+-- multiply :: SNat n -> SNat m -> SNat (n * m)+-- multiply = unsafeLiftNatOp2 (*) -- @ ----- Normally, if @n@ is a 'KnownNat' instance, it is not in general--- inferrable that @n + 1@ also has a 'KnownNat' instance.  This combinator--- makes it so.+-- 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 f x y = withSomeNat (f (fromSNat x) (fromSNat y)) unsafeCoerce++-- | Addition of 'SNat's. ----- For multiple operations on values, this can be chained:+-- This also will provide the correct 'KnownNat' instance for @'SNat' (n+-- + m)@, so can be used as a way to "add" 'KnownNat' instances. ----- @--- 'withNatOp' ('%*') ('Proxy' :: 'Proxy' n) ('Proxy' :: 'Proxy' 2) $---   'withNatOp' ('%+') ('Proxy' :: 'Proxy' (n*2)) ('Proxy' :: 'Proxy' 1) $---     'natVal' ('Proxy' :: 'Proxy' (n * 2 + 1))--- @+-- This stands in for the function with the same name from+-- "Data.Singletons.Prelude.Num".+(%+) :: SNat n -> SNat m -> SNat (n + m)+(%+) = unsafeLiftNatOp2 (+)++-- | Subtraction of 'SNat's.  Note that this is unsafe, as will trigger+-- a run-time underflow if @m@ is bigger than @n@ even though it will always+-- succeed at compiletime. ----- But, at this point, it's easier and simpler to just directly use the--- operators and pattern match:+-- This also will provide the correct 'KnownNat' instance for @'SNat' (n+-- - m)@, so can be used as a way to "subtract" 'KnownNat' instances. ----- @--- let pn = 'natDict' ('Proxy' :: 'Proxy' n)---     p1 = 'natDict' ('Proxy' :: 'Proxy' 1)---     p2 = 'natDict' ('Proxy' :: 'Proxy' 2)--- in  case pn '%*' p2 '%+' p1 of---       'Dict' -> 'natVal' ('Proxy' :: 'Proxy' (n * 2 + 1))--- @+-- This stands in for the function with the same name from+-- "Data.Singletons.Prelude.Num".+(%-) :: SNat n -> SNat m -> SNat (n - m)+(%-) = unsafeLiftNatOp2 (-)++-- | 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 unsafeCoerce++-- | A version of 'minusSNat' that just returns a 'Maybe'.+minusSNat_ :: SNat n -> SNat m -> Maybe (SNat (n - m))+minusSNat_ x = either (const Nothing) Just . minusSNat x++-- | Addition of 'SNat's. ----- (Note that associativity and fixity for the witness-generating operators--- are set to match that of normal addition and multiplication, etc.)+-- This also will provide the correct 'KnownNat' instance for @'SNat' (n+-- * m)@, so can be used as a way to "multiply" 'KnownNat' instances. ----- With /singletons/, @'withNatOp' f x y@ is @'withKnownNat' (f x y)@.+-- This stands in for the function with the same name from+-- "Data.Singletons.Prelude.Num".+(%*) :: SNat n -> SNat m -> SNat (n - m)+(%*) = unsafeLiftNatOp2 (*)++-- | Exponentiation of 'SNat's. ----- So, instead of+-- This also will provide the correct 'KnownNat' instance for @'SNat' (n+-- ^ m)@, so can be used as a way to "exponentiate" 'KnownNat' instances. --+-- This stands in for the function with the same name from+-- "Data.Singletons.TypeLits".+(%^) :: SNat n -> SNat m -> SNat (n ^ m)+(%^) = unsafeLiftNatOp2 (^)++-- | Compare @n@ and @m@, categorizing them into one of the constructors of+-- ':<=?'.+(%<=?) :: SNat n -> SNat m -> n :<=? m+x@SNat %<=? y@SNat = x Comp.%<=? y++-- | Compare @n@ and @m@, categorizing them into one of the constructors of+-- 'SCmpNat'.+sCmpNat :: SNat n -> SNat m -> SCmpNat n m+sCmpNat x@SNat y@SNat = cmpNat x y++-- | An @'SSymbol' n@ is a witness for @'KnownSymbol' n@.+--+-- This means that if you pattern match on the 'SSymbol' constructor, in that+-- branch you will have a @'KnownSymbol' n@ constraint.+-- -- @--- 'withNatOp' ('%+') ('Proxy' :: 'Proxy' n) ('Proxy' :: 'Proxy' 1) $---     'natVal' ('Proxy' :: 'Proxy' (n + 1))+-- myFunc :: SSymbol n -> Bool+-- myFunc SSymbol = ...  -- in this body, we have `KnownSymbol n` -- @ ----- You can just use+-- This is essentially a singleton for 'Symbol', and stands in for the+-- /singletons/ 'SSymbol' and 'Data.Singleton.Sing' types.+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) $+      showString "SSymbol @" . showsPrec 11 (fromSSymbol x)++instance GShow SSymbol where+    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++instance GEq SSymbol where+    geq = testEquality++instance GCompare SSymbol where+    gcompare x y = case compare (fromSSymbol x) (fromSSymbol y) of+      LT -> GLT+      EQ -> unsafeCoerce GEQ+      GT -> GGT++data SomeSymbol__ = forall n. SomeSymbol__ (SSymbol n)++-- | A useful pattern synonym for matching on a 'SomeSymbol' as if it+-- contained an @'SSymbol' n@, and not a @'Proxy' n@ as it exists in+-- "GHC.TypeLits". --+-- A layer of compatibility letting us use the original 'SomeSymbol' type in+-- a way that works well with 'SSymbol'.+--+-- 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)+  where+    SomeSymbol_ (SSymbol :: SSymbol n) = SomeSymbol (Proxy :: Proxy n)+{-# COMPLETE SomeSymbol_ #-}++-- | A useful pattern synonym for matching on a 'String' as if it "were"+-- a 'SSymbol':+-- -- @--- 'withKnownNat' ('SNat' @n) ('SNat @1) $---     'natVal' ('Proxy' :: 'Proxy' (n + 1))+-- myFunc :: String -> Bool+-- myFunc (FromSSymbol x) = ...  -- x is `SSymbol n`, with `n` coming from the input -- @ ----- 'natVal' can of course be replaced with 'fromSing'.+-- It can be used as a function, as well, to convert an @'SSymbol' n@ back+-- into the 'String' that it represents. ---withNatOp-    :: (KnownNat n, KnownNat m)-    => (Dict (KnownNat n) -> Dict (KnownNat m) -> Dict (KnownNat q))-    -> p n-    -> p m-    -> (KnownNat q => r)-    -> r-withNatOp op x y r = case natDict x `op` natDict y of-                       Dict -> r---- | An entailment for addition of 'KnownNat' instances.-entailAdd :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (n + m)-entailAdd = Sub $-  reifyNat (natVal (Proxy :: Proxy n) + natVal (Proxy :: Proxy m)) $ \p ->-    unsafeCoerce (natDict p)+-- 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)+  where+    FromSSymbol = fromSSymbol+{-# COMPLETE FromSSymbol #-} --- | An entailment for subtraction of 'KnownNat' instances.+-- | Given an @'SSymbol' n@ and a value that would require a @'KnownSymbol' n@+-- instance, create that value. ----- Note that this is implemented in a way such that /negative/ 'KnownNat's--- are produced without any errors.-entailSub :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (n - m)-entailSub = Sub $-  reifyNat (natVal (Proxy :: Proxy n) - natVal (Proxy :: Proxy m)) $ \p ->-    unsafeCoerce (natDict p)+-- This stands in for the function of the same name from+-- "Data.Singletons.TypeLits".+withKnownSymbol :: SSymbol n -> (KnownSymbol n => r) -> r+withKnownSymbol SSymbol x = x --- | An entailment for multiplication of 'KnownNat' instances.-entailMul :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (n * m)-entailMul = Sub $-  reifyNat (natVal (Proxy :: Proxy n) * natVal (Proxy :: Proxy m)) $ \p ->-    unsafeCoerce (natDict p)+-- | Promote ("reify") a 'String' to an @'SSymbol' n@, by providing+-- a continuation that would handle it in a way that is polymorphic over+-- all possible @n@.+--+-- 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) --- | An entailment for exponentiation of 'KnownNat' instances.-entailExp :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (n ^ m)-entailExp = Sub $-  reifyNat (natVal (Proxy :: Proxy n) ^ natVal (Proxy :: Proxy m)) $ \p ->-    unsafeCoerce (natDict p)+-- | Promote ("reify") a 'String' to an @'SSymbol' n@ existentially hidden+-- inside a 'SomeNat'.  To use it, pattern match using 'SomeSymbol_'.+--+-- This stands in the /singletons/ 'Data.Singleton.toSomeSing' function, except it takes+-- a 'String' instead of 'Data.Text.Text'.+toSomeSymbol :: String -> SomeSymbol+toSomeSymbol = someSymbolVal +-- | Convert ("reflect") an 'SSymbol' back into the 'String' it represents.+--+-- This stands in the /singletons/ 'Data.Singleton.fromSing' function, except it returns+-- a 'String' instead of 'Data.Text.Text'.+fromSSymbol :: SSymbol n -> String+fromSSymbol x@SSymbol = symbolVal x

@@ -1,40 +1,26 @@--- This file has been generated from package.yaml by hpack version 0.28.2.+cabal-version: 1.12++-- This file has been generated from package.yaml by hpack version 0.31.1. -- -- see: https://github.com/sol/hpack ----- hash: 49b45270e83bf287fa91eedadcbf979e2b8e5438d6ec9adaa6e6fea22183f1a0+-- hash: 8a6351c34d982cd0199ea26cf5f6378e136998abb7019115d627268f8977bdda  name:           typelits-witnesses-version:        0.3.0.3+version:        0.4.0.0 synopsis:       Existential witnesses, singletons, and classes for operations on GHC TypeLits-description:    Provides witnesses for 'KnownNat' and 'KnownSymbol'-                instances for various operations on GHC TypeLits - in-                particular, the arithmetic operations defined in-                "GHC.TypeLits", and also for type-level lists of-                'KnownNat' and 'KnownSymbol' instances.-                .-                This is useful for situations where you have-                @'KnownNat' n@, and you want to prove to GHC-                @'KnownNat' (n + 3)@, or @'KnownNat' (2*n + 4)@, or when-                constraints on the lower or upper limits of @n@ are-                needed.-                .-                It's also useful for when you want to work with type-                level lists of 'KnownNat' or 'KnownSymbol' instances and-                singletons for traversing them, and be able to apply-                analogies of 'natVal' and 'symbolVal' to lists with-                analogies for 'SomeNat' and 'SomeSymbol'.-                .-                Note that most of the functionality in this library can-                be reproduced in a more generic way using the great-                <https://hackage.haskell.org/package/singletons singletons>-                library.  The versions here are provided as a "plumbing-                included" alternative that makes some commonly found-                design patterns involving GHC's TypeLits functionality a-                little smoother, especially when working with external-                libraries or GHC TypeLit's Nat comparison API.+description:    This library contains:                 .-                See README for more information.+                *   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@@ -42,12 +28,11 @@ copyright:      (c) Justin Le 2018 license:        MIT license-file:   LICENSE-tested-with:    GHC>=8.0 && <8.8+tested-with:    GHC>=8.2 && <8.8 build-type:     Simple-cabal-version:  >= 1.10 extra-source-files:-    CHANGELOG.md     README.md+    CHANGELOG.md  source-repository head   type: git@@ -55,16 +40,14 @@  library   exposed-modules:-      GHC.TypeLits.Witnesses-      GHC.TypeLits.List       GHC.TypeLits.Compare+      GHC.TypeLits.Witnesses   other-modules:       Paths_typelits_witnesses   hs-source-dirs:       src-  ghc-options: -Wall+  ghc-options: -Wall -Wredundant-constraints -Werror=incomplete-patterns -Wcompat   build-depends:-      base >=4.7 && <5-    , constraints-    , reflection >=2+      base >=4.10 && <5+    , dependent-sum   default-language: Haskell2010