typelits-witnesses (empty) → 0.1.0.0

raw patch · 5 files changed

+607/−0 lines, 5 filesdep +basedep +constraintsdep +reflectionsetup-changed

Dependencies added: base, constraints, reflection

Files

• LICENSE +20/−0
• Setup.hs +2/−0
• src/GHC/TypeLits/List.hs +312/−0
• src/GHC/TypeLits/Witnesses.hs +227/−0
• typelits-witnesses.cabal +46/−0

@@ -0,0 +1,20 @@+Copyright (c) 2015 Justin Le++Permission is hereby granted, free of charge, to any person obtaining+a copy of this software and associated documentation files (the+"Software"), to deal in the Software without restriction, including+without limitation the rights to use, copy, modify, merge, publish,+distribute, sublicense, and/or sell copies of the Software, and to+permit persons to whom the Software is furnished to do so, subject to+the following conditions:++The above copyright notice and this permission notice shall be included+in all copies or substantial portions of the Software.++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,+EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.+IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY+CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT,+TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE+SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.

@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain

@@ -0,0 +1,312 @@+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE FlexibleContexts #-}++-- |+-- Module      : GHC.TypeLits.List+-- Description : Typeclasses, singletons, and reifiers for type-level lists+--               of 'Nat's and 'Symbol's.+-- Copyright   : (c) Justin Le 2015+-- 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 for more information.++module GHC.TypeLits.List (+  -- * @KnownNats@+    KnownNats(..)+  , SomeNats(..)+  , NatList(..)+  , someNatsVal+  , someNatsVal'+  , reifyNats+  , traverseNatList+  , traverseNatList'+  , traverseNatList_+  , mapNatList+  -- * @KnownSymbols@+  , KnownSymbols(..)+  , SomeSymbols(..)+  , SymbolList(..)+  , someSymbolsVal+  , reifySymbols+  , traverseSymbolList+  , traverseSymbolList'+  , traverseSymbolList_+  , mapSymbolList+  ) where++import Data.Proxy+import Data.Reflection+import GHC.TypeLits+import Data.Functor.Identity++-- | @'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]@.+class KnownNats (ns :: [Nat]) where+    natsVal  :: p ns -> [Integer]+    natsList :: NatList ns++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.+data SomeNats :: * where+    SomeNats :: KnownNats ns => NatList ns -> SomeNats++-- | 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'.+data NatList :: [Nat] -> * where+    ØNL   :: NatList '[]+    (:<#) :: (KnownNat n, KnownNats ns) => Proxy n -> NatList ns -> NatList (n ': ns)++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' 'SomeNat' 'SomeNats'@.+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 nl = case nl of+              ØNL       -> pure $ SomeNats ØNL+              p :<# nl' -> merge <$> f p <*> go nl'+    merge :: SomeNat -> SomeNats -> SomeNats+    merge sn sns = case sn of+                     SomeNat i ->+                       case sns of+                         SomeNats is ->+                           SomeNats (i :<# is)++-- | Like 'traverseNatList', but literally actually a+-- @Traversal' 'SomeNat' 'SomeNats'@, so is usable with lens-library+-- machinery.+traverseNatList' :: forall f. Applicative f+                 => (SomeNat -> f SomeNat)+                 -> SomeNats+                 -> f SomeNats+traverseNatList' f ns =+    case ns of+      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 nl = case nl of+              ØNL       -> pure ()+              p :<# nl' -> f p *> go nl'++-- | 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)++-- | 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.+someNatsVal :: [Integer] -> Maybe SomeNats+someNatsVal []     = Just (SomeNats ØNL)+someNatsVal (n:ns) = do+    SomeNat  m  <- someNatVal n+    SomeNats ms <- someNatsVal ns+    return $ SomeNats (m :<# ms)++-- | 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'.+--+-- For compatability with 'reifyNat', be aware that this also produces+-- @'KnownNat' n@s where @n@ is negative, without complaining.+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)++-- | 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.+someNatsVal' :: [Integer] -> SomeNats+someNatsVal' ns = reifyNats ns SomeNats++-- | @'KnownSymbols' ns@ is intended to represent that every 'Symbol' in the+-- type-level list 'ns' 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' ns@.+--+-- For reasons discussed further in the documentation for 'KnownNats', this+-- also lets you generate a @'SymbolList' ns@, in order to iterate over the+-- type-level list of 'Symbol's and take advantage of their 'KnownSymbol'+-- instances.+class KnownSymbols (ns :: [Symbol]) where+    symbolsVal  :: p ns -> [String]+    symbolsList :: SymbolList ns++instance KnownSymbols '[] where+    symbolsVal  _ = []+    symbolsList    = ØSL++instance (KnownSymbol n, KnownSymbols ns) => KnownSymbols (n ': ns) where+    symbolsVal  _ = symbolVal (Proxy :: Proxy n) : symbolsVal (Proxy :: Proxy ns)+    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.+data SomeSymbols :: * where+    SomeSymbols :: KnownSymbols ns => SymbolList ns -> SomeSymbols++-- | 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'.+data SymbolList :: [Symbol] -> * where+    ØSL   :: SymbolList '[]+    (:<$) :: (KnownSymbol n, KnownSymbols ns) => Proxy n -> SymbolList ns -> SymbolList (n ': ns)++infixr 5 :<$+deriving instance Show (SymbolList ns)++-- | Utility function for traversing over all of the @'Proxy' n@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' 'SomeSymbol' 'SomeSymbols'@.+traverseSymbolList :: forall f ns. Applicative f+                   => (forall n. KnownSymbol n => Proxy n -> f SomeSymbol)+                   -> SymbolList ns+                   -> f SomeSymbols+traverseSymbolList f = go+  where+    go :: forall ms. SymbolList ms -> f SomeSymbols+    go nl = case nl of+              ØSL       -> pure $ SomeSymbols ØSL+              p :<$ nl' -> merge <$> f p <*> go nl'+    merge :: SomeSymbol -> SomeSymbols -> SomeSymbols+    merge s sl = case s of+                   SomeSymbol ps ->+                     case sl of+                       SomeSymbols sl' ->+                         SomeSymbols (ps :<$ sl')++-- | Like 'traverseSymbolList', but literally actually a+-- @Traversal' 'SomeSymbol' 'SomeSymbols'@, so is usable with lens-library+-- machinery.+traverseSymbolList' :: forall f. Applicative f+                 => (SomeSymbol -> f SomeSymbol)+                 -> SomeSymbols+                 -> f SomeSymbols+traverseSymbolList' f ns =+    case ns of+      SomeSymbols ns' -> traverseSymbolList (f . SomeSymbol) ns'++-- | Utility function for traversing over all of the @'Proxy' n@s in+-- a 'SymbolList', each with the corresponding 'KnownSymbol' instance+-- available. Results are ignored.+traverseSymbolList_ :: forall f ns. Applicative f+                    => (forall n a. KnownSymbol n => Proxy n -> f a)+                    -> SymbolList ns+                    -> f ()+traverseSymbolList_ f = go+  where+    go :: forall ms. SymbolList ms -> f ()+    go nl = case nl of+              ØSL       -> pure ()+              p :<$ nl' -> f p *> go nl'++-- | Utility function for \"mapping\" over each of the 'Symbol's in the+-- 'SymbolList'.+mapSymbolList :: (forall n. KnownSymbol n => Proxy n -> SomeSymbol)+              -> SymbolList ns+              -> SomeSymbols+mapSymbolList f = runIdentity . traverseSymbolList (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.+someSymbolsVal :: [String] -> SomeSymbols+someSymbolsVal []     = SomeSymbols ØSL+someSymbolsVal (n:ns) =+    case someSymbolVal n of+      SomeSymbol m ->+        case someSymbolsVal ns of+          SomeSymbols ms ->+            SomeSymbols (m :<$ ms)++-- | 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 'SomeSymbols'.+reifySymbols :: [String]+             -> (forall ns. KnownSymbols ns => SymbolList ns -> r)+             -> r+reifySymbols []     f = f ØSL+reifySymbols (n:ns) f = reifySymbol n $ \m ->+                          reifySymbols ns $ \ms ->+                            f (m :<$ ms)

@@ -0,0 +1,227 @@+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE PolyKinds #-}++-- |+-- Module      : GHC.TypeLits.Witnesses+-- Description : Instance witnesses for various arithmetic operations on+--               GHC TypeLits.+-- Copyright   : (c) Justin Le 2015+-- 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 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:+--+-- @+-- 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!+--+-- At the highest level, this module can be used with 'withNatOp':+--+-- @+-- getDoubled :: forall n. 'KnownNat' n => 'Proxy' n -> 'Integer'+-- getDoubled p = 'withNatOp' ('%*') p ('Proxy' :: 'Proxy' 2) $+--     natVal ('Proxy' :: 'Proxy' (n * 2))+-- @+--+-- 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:+--+-- @+-- 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))+-- @+--+-- In the branch of the case statement, @n * 2 + 1@ indeed has a 'KnownNat'+-- instance.+--+-- Note that the operators have appropriate fixities to mimic value-level+-- arithmetic operations.+--+-- __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.+++module GHC.TypeLits.Witnesses (+  -- * High level wrapper+    withNatOp+  -- * Direct witnesses+  , natDict+  , dictNatVal+  -- * Witness generators+  , (%+)+  , (%-)+  , (%*)+  , (%^)+  -- * Entailments+  , entailAdd+  , entailSub+  , entailMul+  , entailExp+  ) where++import Data.Constraint+import GHC.TypeLits+import Data.Proxy+import Data.Reflection+import Unsafe.Coerce++-- | Create a 'Dict' witness for @'KnownNat' n@.+natDict :: KnownNat n => Proxy n -> Dict (KnownNat n)+natDict _ = Dict++-- | Get the 'Integer' from the 'KnownNat' instance witnessed by the+-- 'Dict'.+dictNatVal :: forall n. Dict (KnownNat n) -> Integer+dictNatVal Dict = natVal (Proxy :: Proxy n)++infixl 6 %++infixl 6 %-+infixl 7 %*+infixr 8 %^++-- | Given witnesses for @'KnownNat' n@ and @'KnownNat' m@, generates+-- a witness for @'KnownNat' (n + m)@.+--+-- 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 entailAdd (Dict :: Dict (KnownNat n, KnownNat m))++-- | Given witnesses for @'KnownNat' n@ and @'KnownNat' m@, generates+-- a witness for @'KnownNat' (n - m)@.+--+-- Note that this is implemented in a way such that /negative/ 'KnownNat's+-- are produced without any errors.+--+-- 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 entailSub (Dict :: Dict (KnownNat n, KnownNat m))++-- | Given witnesses for @'KnownNat' n@ and @'KnownNat' m@, generates+-- a witness for @'KnownNat' (n * m)@.+--+-- 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 entailMul (Dict :: Dict (KnownNat n, KnownNat m))++-- | Given witnesses for @'KnownNat' n@ and @'KnownNat' m@, generates+-- a witness for @'KnownNat' (n ^ m)@.+--+-- 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))++-- | 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.+--+-- For example, with+--+-- @+-- 'withNatOp' ('%+') ('Proxy' :: 'Proxy' n) ('Proxy' :: 'Proxy' 1) r+-- @+--+-- in @r@, @n + 1@ has a 'KnownNat' instance:+--+-- @+-- 'withNatOp' ('%+') ('Proxy' :: 'Proxy' n) ('Proxy' :: 'Proxy' 1) $+--     'natVal' ('Proxy' :: 'Proxy' (n + 1))+-- -- => will return the 'Integer' correpsonding to n + 1+-- @+--+-- 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.+--+-- For multiple operations on values, this can be chained:+--+-- @+-- 'withNatOp' ('%*') ('Proxy' :: 'Proxy' n) ('Proxy' :: 'Proxy' 2) $+--   'withNatOp' ('%+') ('Proxy' :: 'Proxy' (n*2)) ('Proxy' :: 'Proxy' 1) $+--     'natVal' ('Proxy' :: 'Proxy' (n * 2 + 1))+-- @+--+-- But, at this point, it's easier and simpler to just directly use the+-- operators and pattern match:+--+-- @+-- 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))+-- @+--+-- (Note that associativity and fixity for the witness-generating operators+-- are set to match that of normal addition and multiplication, etc.)+--+--+withNatOp :: (KnownNat n, KnownNat m)+          => (Dict (KnownNat n) -> Dict (KnownNat m) -> Dict (KnownNat q))+          -> Proxy n+          -> Proxy 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)++-- | An entailment for subtraction of 'KnownNat' instances.+--+-- 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)++-- | 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)++-- | 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)+

@@ -0,0 +1,46 @@+name:                typelits-witnesses+version:             0.1.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)@.+                     .+                     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'.+                     .+                     See README for more information.+homepage:            https://github.com/mstksg/typelits-witnesses+license:             MIT+license-file:        LICENSE+author:              Justin Le+maintainer:          justin@jle.im+copyright:           (c) Justin Le 2015+category:            Data+build-type:          Simple+-- extra-source-files:  +cabal-version:       >=1.10++source-repository head+  type:              git+  location:          git://github.com/mstksg/typelits-witnesses.git++library+  exposed-modules:     GHC.TypeLits.Witnesses+                       GHC.TypeLits.List+  -- other-modules:       +  -- other-extensions:    +  build-depends:       base >=4.8 && <4.9+                     , reflection+                     , constraints+  hs-source-dirs:      src+  ghc-options:         -Wall+  default-language:    Haskell2010