typelits-witnesses 0.2.3.0 → 0.3.0.0

raw patch · 6 files changed

+267/−99 lines, 6 filesdep ~basedep ~constraintsPVP ok

version bump matches the API change (PVP)

Dependency ranges changed: base, constraints

API changes (from Hackage documentation)

Files

• CHANGELOG.md +13/−0
• README.md +110/−64
• src/GHC/TypeLits/Compare.hs +25/−22
• src/GHC/TypeLits/List.hs +21/−3
• src/GHC/TypeLits/Witnesses.hs +80/−3
• typelits-witnesses.cabal +18/−7

@@ -1,3 +1,16 @@+Version 0.3.0.0+===============++<https://github.com/mstksg/typelits-witnesses/releases/tag/v0.3.0.0>++*   Added extra witnesses inside the constructors of `(:<=?)`.+*   Allowed functions to polymorphically expect `p n` instead of `Proxy n`+    whenever possible.+*   Soft deprecation of *GHC.TypeLits.Witnesses*, in case people want to use+    the functionality of *singletons* without the full library.+*   Formal deprecation of *GHC.TypeLits.List*, with migration information,+    because it's just so much more unweidly than using *singletons*.+ Version 0.2.3.0 =============== 

@@ -1,11 +1,10 @@ typelits-witnesses ================== -[![typelits-witnesses on Hackage](https://img.shields.io/hackage/v/lens.svg?maxAge=2592000)](https://hackage.haskell.org/package/typelits-witnesses)+[![typelits-witnesses on Hackage](https://img.shields.io/hackage/v/typelits-witnesses.svg?maxAge=2592000)](https://hackage.haskell.org/package/typelits-witnesses) [![typelits-witnesses on Stackage LTS](http://stackage.org/package/typelits-witnesses/badge/lts)](http://stackage.org/lts/package/typelits-witnesses) [![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)+[![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@@ -30,10 +29,73 @@  [singletons]: https://hackage.haskell.org/package/singletons +GHC.TypeLits.Compare+-------------------- -`GHC.TypeLits.Witnesses`-------------------------+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`. @@ -59,7 +121,7 @@  ~~~haskell getDoubled :: KnownNat n => Proxy n -> Integer-getDoubled p = natVal (Proxy :: Proxy (n * 2))+getDoubled p = natVal (Proxy @(n * 2)) ~~~  Which is supposed to call `natVal` with `n * 2`.  However, this fails, because@@ -70,23 +132,23 @@  ~~~haskell getDoubled :: forall n. KnownNat n => Proxy n -> Integer-getDoubled p = withNatOp (%*) p (Proxy :: Proxy 2) $-    natVal (Proxy :: Proxy (n * 2))+getDoubled p = withNatOp (%*) p (Proxy @2) $+    natVal (Proxy @(n * 2)) ~~~  Within the scope of the argument of-`withNatOp (%*) (Proxy :: Proxy n) (Proxy :: Proxy m)`, `n * m` is an instance+`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 :: Proxy 12)+> 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.+`(%*)`, 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`.@@ -94,68 +156,35 @@ There are more advanced operations dealing with low-level machinery, as well, in the module.  See module documentation for more detail. -`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`).+### Singletons replacement -If a library function requires `1 <= n` constraint, but only `KnownNat n` is-available:+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-foo :: (KnownNat n, 1 <= n) => Proxy n -> Int--bar :: KnownNat n => Proxy n -> Int-bar n = case (Proxy :: Proxy 1) %<=? n of-          LE  Refl -> foo n-          NLE _    -> 0+getDoubled :: forall n. KnownNat n => Proxy n -> Integer+getDoubled p = withKnownNat (SNat @n %:* SNat @2) $+    natVal (Proxy @(n * 2)) ~~~ -`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:+But one using singletons throughout the whole process would be:  ~~~haskell-bar :: KnownNat n => Proxy n -> Int-bar n = case isLE (Proxy :: Proxy 1) n of-          Just Refl -> foo n-          Nothing   -> 0+getDoubled :: forall n. KnownNat n => Sing n -> Integer+getDoubled s = withKnownNat (s %:* SNat @2) $+    natVal (Proxy @(n * 2)) ~~~ -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 cmpNat (Proxy :: Proxy 5) n of-          CLT Refl -> foo1 n-          CEQ Refl -> 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.List`+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.@@ -164,7 +193,7 @@ `natsVal`, which is like `natVal` but for type-level lists of `KnownNats`:  ~~~haskell-> natsVal (Proxy :: Proxy [1,2,3])+> natsVal (Proxy @[1,2,3]) [1,2,3] ~~~ @@ -184,7 +213,7 @@ ~~~  ~~~haskell-> printNats (natsList :: NatList [1,2,3])+> printNats (natsList :: @[1,2,3]) 1 2 3@@ -222,4 +251,21 @@ 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'+~~~ 

@@ -87,65 +87,65 @@   , flipCmpNat   , cmpNatEq   , eqCmpNat+  , reflCmpNat     -- ** Interfacing with '<=?'   , cmpNatLE   )   where  import Data.Type.Equality-import Data.Proxy import GHC.TypeLits import Unsafe.Coerce  isLE     :: (KnownNat m, KnownNat n)-    => Proxy m-    -> Proxy n+    => p m+    -> p n     -> Maybe ((m <=? n) :~: 'True) isLE m n = case m %<=? n of              LE  Refl -> Just Refl-             NLE _    -> Nothing+             NLE _ _  -> Nothing  isNLE     :: (KnownNat m, KnownNat n)-    => Proxy m-    -> Proxy n+    => p m+    -> p n     -> Maybe ((m <=? n) :~: 'False) isNLE m n = case m %<=? n of-              NLE Refl -> Just Refl-              LE  _    -> Nothing+              NLE Refl Refl -> Just Refl+              LE  _         -> Nothing  data (:<=?) :: Nat -> Nat -> * where     LE  :: ((m <=? n) :~: 'True)  -> (m :<=? n)-    NLE :: ((m <=? n) :~: 'False) -> (m :<=? n)+    NLE :: ((m <=? n) :~: 'False) -> ((n <=? m) :~: 'True) -> (m :<=? n)  (%<=?)      :: (KnownNat m, KnownNat n)-     => Proxy m-     -> Proxy n+     => p m+     -> p n      -> (m :<=? n) m %<=? n | natVal m <= natVal n = LE  (unsafeCoerce Refl)-         | otherwise            = NLE (unsafeCoerce Refl)+         | otherwise            = NLE (unsafeCoerce Refl) (unsafeCoerce Refl)  data SCmpNat :: Nat -> Nat -> * where     CLT :: (CmpNat m n :~: 'LT) -> SCmpNat m n-    CEQ :: (CmpNat m n :~: 'EQ) -> SCmpNat m n+    CEQ :: (CmpNat m n :~: 'EQ) -> (m :~: n) -> SCmpNat m n     CGT :: (CmpNat m n :~: 'GT) -> SCmpNat m n  cmpNat     :: (KnownNat m, KnownNat n)-    => Proxy m-    -> Proxy n+    => p m+    -> p n     -> SCmpNat m n cmpNat m n = case compare (natVal m) (natVal n) of                LT -> CLT (unsafeCoerce Refl)-               EQ -> CEQ (unsafeCoerce Refl)+               EQ -> CEQ (unsafeCoerce Refl) (unsafeCoerce Refl)                GT -> CGT (unsafeCoerce Refl)  flipCmpNat :: SCmpNat m n -> SCmpNat n m-flipCmpNat = \case CLT Refl -> CGT (unsafeCoerce Refl)-                   CEQ Refl -> CEQ (unsafeCoerce 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)  cmpNatEq :: (CmpNat m n :~: 'EQ) -> (m :~: n) cmpNatEq = \case Refl -> unsafeCoerce Refl@@ -153,7 +153,10 @@ eqCmpNat :: (m :~: n) -> (CmpNat m n :~: 'EQ) eqCmpNat = \case Refl -> unsafeCoerce Refl +reflCmpNat :: (m :~: n) -> SCmpNat m n+reflCmpNat r = CEQ (eqCmpNat r) r+ cmpNatLE :: SCmpNat m n -> (m :<=? n)-cmpNatLE = \case CLT Refl -> LE  (unsafeCoerce Refl)-                 CEQ Refl -> LE  (unsafeCoerce Refl)-                 CGT Refl -> NLE (unsafeCoerce Refl)+cmpNatLE = \case CLT Refl      -> LE  (unsafeCoerce Refl)+                 CEQ Refl Refl -> LE  (unsafeCoerce Refl)+                 CGT Refl      -> NLE (unsafeCoerce Refl) (unsafeCoerce Refl)

@@ -33,7 +33,8 @@ -- -- See typeclass documentations and README for more information. -module GHC.TypeLits.List (+module GHC.TypeLits.List+  {-# DEPRECATED "Use singletons package instead" #-} (   -- * 'KnownNats'     KnownNats(..)   , SomeNats(..)@@ -75,6 +76,7 @@ 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').@@ -92,6 +94,9 @@ class KnownNats (ns :: [Nat]) where     natsVal  :: p ns -> [Integer]     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  _ = []@@ -106,6 +111,7 @@ -- compile-time. data SomeNats :: * 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'@@ -117,6 +123,7 @@     Ø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)@@ -211,6 +218,7 @@     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@@ -228,6 +236,7 @@ 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@@ -241,13 +250,14 @@     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. 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).@@ -274,7 +284,7 @@         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@@ -291,6 +301,9 @@ class KnownSymbols (ss :: [Symbol]) where     symbolsVal  :: p ss -> [String]     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  _ = []@@ -304,6 +317,7 @@ -- but you don't know what the list contains at compile-time. data SomeSymbols :: * 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,@@ -315,6 +329,7 @@     Ø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)@@ -411,6 +426,7 @@         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@@ -424,6 +440,7 @@ 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"@@ -451,4 +468,5 @@         Refl <- sameSymbol s t         Refl <- sameSymbols ss ts         return Refl+{-# DEPRECATED sameSymbols "Use (%~) from the singletons package instead" #-} 

@@ -15,6 +15,7 @@ -- Stability   : unstable -- Portability : non-portable --+-- __Deprecated: Use the /singletons/ package instead__ -- -- This module provides witnesses for instances that result from the -- various arithmetic operations on GHC TypeLits 'Nat' types.  In general,@@ -67,9 +68,13 @@ -- 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.+--+--   module GHC.TypeLits.Witnesses (+  -- * Singletons+  -- $singletons   -- * High level wrapper     withNatOp   -- * Direct witnesses@@ -93,12 +98,61 @@ import Data.Reflection import Unsafe.Coerce +-- $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 '%^'.+--+--   * 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'.+--+--   * 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.+--+ -- | Create a 'Dict' witness for @'KnownNat' n@.-natDict :: KnownNat n => Proxy n -> Dict (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  -- | 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) @@ -112,6 +166,8 @@ -- -- Follows proper association and fixity for usage with other similar -- operators.+--+-- 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)) @@ -123,6 +179,8 @@ -- -- Follows proper association and fixity for usage with other similar -- operators.+--+-- 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)) @@ -131,6 +189,8 @@ -- -- Follows proper association and fixity for usage with other similar -- operators.+--+-- 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)) @@ -188,12 +248,29 @@ -- (Note that associativity and fixity for the witness-generating operators -- are set to match that of normal addition and multiplication, etc.) --+-- With /singletons/, @'withNatOp' f x y@ is @'withKnownNat' (f x y)@. --+-- So, instead of+--+-- @+-- 'withNatOp' ('%+') ('Proxy' :: 'Proxy' n) ('Proxy' :: 'Proxy' 1) $+--     'natVal' ('Proxy' :: 'Proxy' (n + 1))+-- @+--+-- You can just use+--+-- @+-- 'withKnownNat' ('SNat' @n) ('SNat @1) $+--     'natVal' ('Proxy' :: 'Proxy' (n + 1))+-- @+--+-- 'natVal' can of course be replaced with 'fromSing'.+-- withNatOp     :: (KnownNat n, KnownNat m)     => (Dict (KnownNat n) -> Dict (KnownNat m) -> Dict (KnownNat q))-    -> Proxy n-    -> Proxy m+    -> p n+    -> p m     -> (KnownNat q => r)     -> r withNatOp op x y r = case natDict x `op` natDict y of

@@ -1,5 +1,5 @@ name:                typelits-witnesses-version:             0.2.3.0+version:             0.3.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@@ -34,12 +34,16 @@ license-file:        LICENSE author:              Justin Le maintainer:          justin@jle.im-copyright:           (c) Justin Le 2016+copyright:           (c) Justin Le 2018 category:            Data build-type:          Simple extra-source-files:  README.md                    , CHANGELOG.md cabal-version:       >=1.10+tested-with:         GHC == 7.8.4+                   , GHC == 7.10.3+                   , GHC == 8.0.2+                   , GHC == 8.2.1  source-repository head   type:              git@@ -51,11 +55,18 @@                        GHC.TypeLits.Compare   -- other-modules:          -- other-extensions:    -  build-depends:       base >=4.7 && <5-                     , base-compat-                     , constraints-                     , reflection >= 2-                     , transformers+  if impl(ghc >= 8.0)+    build-depends:       base >=4.7 && <5+                       , base-compat+                       , constraints+                       , reflection >= 2+                       , transformers+  else+    build-depends:       base >=4.7 && <5+                       , base-compat+                       , constraints < 0.9.1+                       , reflection >= 2+                       , transformers   hs-source-dirs:      src   ghc-options:         -Wall   default-language:    Haskell2010