kind-integer (empty) → 0.1

raw patch · 6 files changed

+858/−0 lines, 6 filesdep +basedep +ghc-primdep +kind-integer

Dependencies added: base, ghc-prim, kind-integer

Files

CHANGELOG.md +3/−0
LICENSE +27/−0
README.md +4/−0
kind-integer.cabal +46/−0
lib/KindInteger.hs +404/−0
test/Main.hs +374/−0

+ CHANGELOG.md view

@@ -0,0 +1,3 @@+# Version 0.1++* Initial version.

+ LICENSE view

@@ -0,0 +1,27 @@+Copyright (c) 2023, Renzo Carbonara.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are+met:++1. Redistributions of source code must retain the above copyright+notice, this list of conditions and the following disclaimer.++2. Redistributions in binary form must reproduce the above copyright+notice, this list of conditions and the following disclaimer in the+documentation and/or other materials provided with the distribution.++3. Neither the name of the copyright holder nor the names of its+contributors may be used to endorse or promote products derived from+this software without specific prior written permission.  THIS SOFTWARE+IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY+EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE+IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR+PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR+CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,+EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,+PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR+PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF+LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING+NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS+SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

+ README.md view

@@ -0,0 +1,4 @@+# kind-integer++Haskell type-level `Integer`s. Like `KnownNat`, but for `Integer`s.+

+ kind-integer.cabal view

@@ -0,0 +1,46 @@+cabal-version: 2.4+name: kind-integer+version: 0.1+license: BSD-3-Clause+license-file: LICENSE+extra-source-files: README.md CHANGELOG.md+author: Renzo Carbonara+maintainer: renλren.zone+copyright: Copyright (c) Renzo Carbonara 2023+category: Types+build-type: Simple+synopsis: Type-level integers. Like KnownNat, but for integers.+description: Type-level integers. Like KnownNat, but for integers.+homepage: https://github.com/k0001/hs-kind+bug-reports: https://github.com/k0001/hs-kind/issues+tested-with: GHC ==9.2.5, GHC ==9.4.3++source-repository head+  type: git+  location: https://github.com/k0001/hs-kind+  subdir: kind-integer++common basic+  default-language: GHC2021+  ghc-options: -O2 -Wall -Werror=incomplete-patterns+  build-depends: base ==4.*+  default-extensions:+    DataKinds+    NoStarIsType+    PatternSynonyms+    TypeFamilies+    TypeOperators+    ViewPatterns++library+  import: basic+  hs-source-dirs: lib+  build-depends: ghc-prim+  exposed-modules: KindInteger++test-suite test+  import: basic+  type: exitcode-stdio-1.0+  hs-source-dirs: test+  main-is: Main.hs+  build-depends: kind-integer

+ lib/KindInteger.hs view

@@ -0,0 +1,404 @@+{-# LANGUAGE MagicHash #-}+{-# LANGUAGE UndecidableInstances #-}++-- | This module provides a type-level representation for term-level+-- 'P.Integer's. This type-level representation is also named 'P.Integer',+-- So import this module qualified to avoid name conflicts.+--+-- @+-- import "KindInteger" qualified as K+-- @+--+-- The implementation details are the same as the ones for type-level 'Natural's+-- in "GHC.TypeNats" as of @base-4.18@, and it will continue to evolve together+-- with @base@, trying to follow its API as much as possible until the day+-- @base@ provides its own type-level integer, making this module redundant.+module KindInteger+  ( -- * Integer Kind+    Integer+  , type P+  , type N+  , Normalize++    -- * Linking type and value level+  , KnownInteger(integerSing), integerVal, integerVal'+  , SomeInteger(..)+  , someIntegerVal+  , sameInteger++    -- ** Singleton values+  , SInteger+  , pattern SInteger+  , fromSInteger+  , withSomeSInteger+  , withKnownInteger++    -- * Arithmethic+  , type (+), type (*), type (^), type (-)+  , Negate, Div, Mod, Quot, Rem, Log2++    -- * Comparisons+  , CmpInteger+  , cmpInteger+  , type (==?), type (==), type (/=?), type (/=)+  ) where++import GHC.Base (WithDict(..))+import GHC.Types (TYPE, Constraint)+import GHC.Show (appPrec, appPrec1)+import GHC.Prim (Proxy#)+import GHC.TypeLits qualified as L+import Data.Proxy+import Data.Type.Coercion+import Data.Type.Equality (TestEquality(..), (:~:)(..))+import Data.Type.Bool (If)+import Data.Type.Ord+import Numeric.Natural (Natural)+import Prelude hiding (Integer, (==), (/=))+import Prelude qualified as P+import Unsafe.Coerce(unsafeCoerce)++--------------------------------------------------------------------------------++-- | Type-level version of 'P.Integer', only ever used as a /kind/+-- for 'P' and 'N'+--+-- * A positive number /+x/ is represented as @'P' x@.+--+-- * A negative number /-x/ is represented as @'N' x@.+--+-- * /Zero/ can be represented as @'P' 0@ or @'N' 0@. For consistency, all+-- /zero/ outputs from type families in this "KindInteger" module use the+-- @'P' 0@, but don't assume that this will be the case elsewhere. So, if you+-- need to treat /zero/ specially in some situation, be sure to handle both the+-- @'P' 0@ and @'N' 0@ cases.+data Integer+  = Positive Natural+  | Negative Natural++-- | * A positive number /+x/ is represented as @'P' x@.+--+-- * /Zero/ can be represented as @'P' 0@ (see notes at 'Integer').+type P (x :: Natural) = 'Positive x :: Integer++-- | * A negative number /-x/ is represented as @'N' x@.+--+-- * /Zero/ can be represented as @'N' 0@ (but often isn't, see notes at 'Integer').+type N (x :: Natural) = 'Negative x :: Integer++-- Not used:+--+-- typeIntegerToTermInteger :: Integer -> P.Integer+-- typeIntegerToTermInteger (P n) = toInteger n+-- typeIntegerToTermInteger (N n) = negate (toInteger n)++termIntegerToTypeInteger :: P.Integer -> Integer+termIntegerToTypeInteger i = let n = fromInteger i+                             in  if i >= 0 then Positive n else Negative n++-- | We are not interested in giving any instance to type-level 'Integer's,+-- so we implement 'showsPrec' here.+showsPrecInteger :: Int -> Integer -> ShowS+showsPrecInteger p i = showParen (p > appPrec) $ case i of+  Positive x -> showString "P " . shows x+  Negative x -> showString "N " . shows x++--------------------------------------------------------------------------------++-- | This class gives the integer associated with a type-level integer.+-- There are instances of the class for every integer.+class KnownInteger (i :: Integer) where+  integerSing :: SInteger i++-- | Positive numbers and zero.+instance L.KnownNat x => KnownInteger (P x) where+  integerSing = UnsafeSInteger (L.natVal (Proxy @x))++-- | Negative numbers and zero.+instance L.KnownNat x => KnownInteger (N x) where+  integerSing = UnsafeSInteger (negate (L.natVal (Proxy @x)))++-- | Term-level 'P.Integer' representation of the type-level 'Integer' @i@.+integerVal :: forall i proxy. KnownInteger i => proxy i -> P.Integer+integerVal _ = case integerSing :: SInteger i of UnsafeSInteger x -> x++-- | Term-level 'P.Integer' representation of the type-level 'Integer' @i@.+integerVal' :: forall i. KnownInteger i => Proxy# i -> P.Integer+integerVal' _ = case integerSing :: SInteger i of UnsafeSInteger x -> x++-- | This type represents unknown type-level 'Integer'.+data SomeInteger = forall n. KnownInteger n => SomeInteger (Proxy n)++-- | Convert a term-level 'P.Integer' into an unknown type-level 'Integer'.+someIntegerVal :: P.Integer -> SomeInteger+someIntegerVal i = withSomeSInteger i (\(si :: SInteger i) ->+                   withKnownInteger si (SomeInteger @i Proxy))++instance Eq SomeInteger where+  SomeInteger x == SomeInteger y = integerVal x P.== integerVal y++instance Ord SomeInteger where+  compare (SomeInteger x) (SomeInteger y) =+    compare (integerVal x) (integerVal y)++instance Show SomeInteger where+  showsPrec p (SomeInteger x) = showsPrec p (integerVal x)++instance Read SomeInteger where+  readsPrec p xs = do (a, ys) <- readsPrec p xs+                      [(someIntegerVal a, ys)]++--------------------------------------------------------------------------------+-- Within this module, we use these “normalization” tools to make sure that+-- /zero/ is always represented as @'P' 0@. We don't export any of these+-- normalization tools to end-users because it seems like we can't make them+-- reliable enough so as to offer a decent user experience. So, we just tell+-- users to deal with the fact that both @'P' 0@ and @'N' 0@ mean /zero/.++-- | Make sure /zero/ is represented as @'P' 0@, not as @'N' 0@+--+-- Notice that all the tools in the "KindInteger" can readily handle+-- non-'Normalize'd inputs. This 'Normalize' type-family is offered offered+-- only as a convenience in case you want to simplify /your/ dealing with+-- /zeros/.+type family Normalize (i :: Integer) :: Integer where+  Normalize (N 0) = P 0+  Normalize i     = i++-- | Construct a 'Normalize'd 'N'egative type-level 'Integer'.+--+-- To be used for producing all negative outputs in this module.+type NN (a :: Natural) = Normalize (N a) :: Integer++--------------------------------------------------------------------------------++infixl 6 +, -+infixl 7 *, `Div`, `Mod`, `Quot`, `Rem`+infixr 8 ^++-- | Negation of type-level 'Integer's.+type family Negate (x :: Integer) :: Integer where+  Negate (P 0) = P 0+  Negate (P x) = N x+  Negate (N x) = P x++-- | Addition of type-level 'Integer's.+type (a :: Integer) + (b :: Integer) = Add_ (Normalize a) (Normalize b) :: Integer+type family Add_ (a :: Integer) (b :: Integer) :: Integer where+  Add_ (P a) (P b) = P (a L.+ b)+  Add_ (N a) (N b) = NN (a L.+ b)+  Add_ (P a) (N b) = If (b <=? a) (P (a L.- b)) (NN (b L.- a))+  Add_ (N a) (P b) = Add_ (P b) (N a)++-- | Multiplication of type-level 'Integer's.+type (a :: Integer) * (b :: Integer) = Mul_ (Normalize a) (Normalize b) :: Integer+type family Mul_ (a :: Integer) (b :: Integer) :: Integer where+  Mul_ (P a) (P b) = P (a L.* b)+  Mul_ (N a) (N b) = Mul_ (P a) (P b)+  Mul_ (P a) (N b) = NN (a L.* b)+  Mul_ (N a) (P b) = Mul_ (P a) (N b)++-- | Exponentiation of type-level 'Integer's.+--+-- * Exponentiation by negative 'Integer' doesn't type-check.+type (a :: Integer) ^ (b :: Integer) = Pow_ (Normalize a) (Normalize b) :: Integer+type family Pow_ (a :: Integer) (b :: Integer) :: Integer where+  Pow_ (P a) (P b) = P (a L.^ b)+  Pow_ (N a) (P b) = NN (a L.^ b)+  Pow_ _     (N _) = L.TypeError ('L.Text "KindInteger.(^): Negative exponent")++-- | Subtraction of type-level 'Integer's.+type (a :: Integer) - (b :: Integer) = a + Negate b :: Integer++-- | Division ('floor'ed) of type-level 'Integer's.+--+-- @+-- forall (a :: 'Integer') (b :: 'Integer').+--   /such that/ (b '/=' 0).+--     a  '=='  'Div' a b '*' 'Negate' b '+' 'Mod' a b+-- @+--+-- * Division by /zero/ doesn't type-check.+type Div (a :: Integer) (b :: Integer) = Div_ (Normalize a) (Normalize b) :: Integer+type family Div_ (a :: Integer) (b :: Integer) :: Integer where+  Div_ _ (P 0) = L.TypeError ('L.Text "KindInteger.Div: Division by zero")+  Div_ (P a) (P b) = P (L.Div a b)+  Div_ (N a) (N b) = Div_ (P a) (P b)+  Div_ (P a) (N b) = NN (If (b L.* (L.Div a b) ==? a) (L.Div a b) (L.Div a b L.+ 1))+  Div_ (N a) (P b) = Div_ (P a) (N b)++-- | Modulus ('floor'ed division) of type-level 'Integer's.+--+-- @+-- forall (a :: 'Integer') (b :: 'Integer').+--   /such that/ (b '/=' 0).+--     a  '=='  'Div' a b '*' 'Negate' b '+' 'Mod' a b+-- @+--+-- * Modulus by /zero/ doesn't type-check.+type Mod (a :: Integer) (b :: Integer) = Div a b * Negate b + a :: Integer++-- | Division ('truncate'd) of type-level 'Integer's.+--+-- @+-- forall (a :: 'Integer') (b :: 'Integer').+--   /such that/ (b '/=' 0).+--     a  '=='  'Quot' a b '*' 'Negate' b '+' 'Rem' a b+-- @+--+-- * Division by /zero/ doesn't type-check.+type Quot (a :: Integer) (b :: Integer) = Quot_ (Normalize a) (Normalize b) :: Integer+type family Quot_ (a :: Integer) (b :: Integer) :: Integer where+  Quot_ _ (P 0) = L.TypeError ('L.Text "KindInteger.Quot: Division by zero")+  Quot_ (P a) (P b) = P (L.Div a b)+  Quot_ (N a) (N b) = Quot_ (P a) (P b)+  Quot_ (P a) (N b) = Negate (Quot_ (P a) (P b))+  Quot_ (N a) (P b) = Quot_ (P a) (N b)++-- | Remulus ('truncate'd division) of type-level 'Integer's.+--+-- @+-- forall (a :: 'Integer') (b :: 'Integer').+--   /such that/ (b '/=' 0).+--     a  '=='  'Quot' a b '*' 'Negate' b '+' 'Rem' a b+-- @+--+-- * Remulus by /zero/ doesn't type-check.+type Rem (a :: Integer) (b :: Integer) = Quot a b * Negate b + a :: Integer++-- | Log base 2 ('floor'ed) of integer numbers.+--+-- * Logarithm of /zero/ doesn't type-check.+--+-- * Logarithm of negative number doesn't type-check.+type Log2 (a :: Integer) = Log2_ (Normalize a) :: Integer+type family Log2_ (a :: Integer) :: Integer where+  Log2_ (P 0) = L.TypeError ('L.Text "KindInteger.Log2: Logarithm of zero")+  Log2_ (P a) = P (L.Log2 a)+  Log2_ (N a) = L.TypeError ('L.Text "KindInteger.Log2: Logarithm of negative number")++-- | Comparison of type-level integers, as a function.+type CmpInteger (a :: Integer) (b :: Integer) = CmpInteger_ (Normalize a) (Normalize b) :: Ordering+type family CmpInteger_ (a :: Integer) (b :: Integer) :: Ordering where+  CmpInteger_ a a = 'EQ+  CmpInteger_ (P a) (P b) = Compare a b+  CmpInteger_ (N a) (N b) = Compare b a+  CmpInteger_ (N _) (P _) = 'LT+  CmpInteger_ (P _) (N _) = 'GT++-- | "Data.Type.Ord" support for type-level 'Integer's.+type instance Compare (a :: Integer) (b :: Integer) = CmpInteger a b :: Ordering++--------------------------------------------------------------------------------++-- | We either get evidence that this function was instantiated with the+-- same type-level 'Integer's, or 'Nothing'.+sameInteger+  :: forall a b proxy1 proxy2+  .  (KnownInteger a, KnownInteger b)+  => proxy1 a+  -> proxy2 b+  -> Maybe (a :~: b)+sameInteger _ _ = testEquality (integerSing @a) (integerSing @b)++-- | Like 'sameInteger', but if the type-level 'Integer's aren't equal, this+-- additionally provides proof of 'LT' or 'GT'.+cmpInteger+  :: forall a b proxy1 proxy2+  .  (KnownInteger a, KnownInteger b)+  => proxy1 a+  -> proxy2 b+  -> OrderingI a b+cmpInteger x y = case compare (integerVal x) (integerVal y) of+  EQ -> case unsafeCoerce (Refl, Refl) :: (CmpInteger a b :~: 'EQ, a :~: b) of+    (Refl, Refl) -> EQI+  LT -> case unsafeCoerce Refl :: (CmpInteger a b :~: 'LT) of+    Refl -> LTI+  GT -> case unsafeCoerce Refl :: (CmpInteger a b :~: 'GT) of+    Refl -> GTI++--------------------------------------------------------------------------------++-- | Singleton type for a type-level 'Integer' @i@.+newtype SInteger (i :: Integer) = UnsafeSInteger P.Integer++-- | A explicitly bidirectional pattern synonym relating an 'SInteger' to a+-- 'KnownInteger' constraint.+--+-- As an __expression__: Constructs an explicit @'SInteger' i@ value from an+-- implicit @'KnownInteger' i@ constraint:+--+-- @+-- 'SInteger' @i :: 'KnownInteger' i => 'SInteger' i+-- @+--+-- As a __pattern__: Matches on an explicit @'SInteger' i@ value bringing+-- an implicit @'KnownInteger' i@ constraint into scope:+--+-- @+-- f :: 'SInteger' i -> ..+-- f SInteger = {- SInteger i in scope -}+-- @+pattern SInteger :: forall i. () => KnownInteger i => SInteger i+pattern SInteger <- (knownIntegerInstance -> KnownIntegeregerInstance)+  where SInteger = integerSing++-- | An internal data type that is only used for defining the 'SInteger' pattern+-- synonym.+data KnownIntegeregerInstance (i :: Integer) where+  KnownIntegeregerInstance :: KnownInteger i => KnownIntegeregerInstance i++-- | An internal function that is only used for defining the 'SInteger' pattern+-- synonym.+knownIntegerInstance :: SInteger i -> KnownIntegeregerInstance i+knownIntegerInstance si = withKnownInteger si KnownIntegeregerInstance++instance Show (SInteger i) where+  showsPrec p (UnsafeSInteger i) = showParen (p > appPrec) $+    showString "SInteger @" .+    showsPrecInteger appPrec1 (termIntegerToTypeInteger i)++instance TestEquality SInteger where+  testEquality (UnsafeSInteger x) (UnsafeSInteger y)+    | x P.== y  = Just (unsafeCoerce Refl)+    | otherwise = Nothing++instance TestCoercion SInteger where+  testCoercion x y = fmap (\Refl -> Coercion) (testEquality x y)++-- | Return the type-level 'P.Integer' number corresponding to @i@ in+-- a @'SInteger' i@ value.+fromSInteger :: SInteger i -> P.Integer+fromSInteger (UnsafeSInteger i) = i++-- | Convert an explicit @'SInteger' i@ value into an implicit+-- @'KnownInteger' i@ constraint.+withKnownInteger+  :: forall i rep (r :: TYPE rep). SInteger i -> (KnownInteger i => r) -> r+withKnownInteger = withDict @(KnownInteger i)++-- | Convert a 'P.Integer' number into an @'SInteger' n@ value, where @n@ is a+-- fresh type-level 'Integer'.+withSomeSInteger+  :: forall rep (r :: TYPE rep). P.Integer -> (forall n. SInteger n -> r) -> r+withSomeSInteger n k = k (UnsafeSInteger n)+-- It's very important to keep this NOINLINE! See the docs at "GHC.TypeNats"+{-# NOINLINE withSomeSInteger #-}++--------------------------------------------------------------------------------+-- Extras++infixr 4 /=, /=?, ==, ==?++-- | This should be exported by 'Data.Type.Ord'.+type (a :: k) ==? (b :: k) = OrdCond (Compare a b) 'False 'True 'False :: Bool++-- | This should be exported by 'Data.Type.Ord'.+type (a :: k) == (b :: k) = (a ==? b) ~ 'True :: Constraint++-- | This should be exported by 'Data.Type.Ord'.+type (a :: k) /=? (b :: k) = OrdCond (Compare a b) 'True 'False 'True :: Bool++-- | This should be exported by 'Data.Type.Ord'.+type (a :: k) /= (b :: k) = (a /=? b) ~ 'True :: Constraint+

+ test/Main.hs view

@@ -0,0 +1,374 @@+{-# LANGUAGE MagicHash #-}+module Main (main) where++import Control.Applicative+import Data.Maybe+import Data.Proxy+import Data.Type.Ord (type (<=))+import GHC.Exts (Constraint, proxy#)+import System.Exit+import Text.Read++import KindInteger (P, N)+import KindInteger qualified as K++--------------------------------------------------------------------------------++data Dict (c :: Constraint) where+  Dict :: c => Dict c++--------------------------------------------------------------------------------++_testEq =  Dict+_testEq :: Dict+  ( P 0 K.== P 0,   'True ~ (P 0 K.==? P 0)+  , N 0 K.== N 0,   'True ~ (N 0 K.==? N 0)+  , P 0 K.== N 0,   'True ~ (P 0 K.==? N 0)+  , N 0 K.== P 0,   'True ~ (N 0 K.==? P 0)++  , P 0 K./= P 1,   'True ~ (P 0 K./=? P 1)+  , P 0 K./= N 1,   'True ~ (P 0 K./=? N 1)++  , N 0 K./= N 1,   'True ~ (N 0 K./=? N 1)+  , N 0 K./= N 1,   'True ~ (N 0 K./=? N 1)++  , P 1 K./= P 0,   'True ~ (P 1 K./=? P 0)+  , P 1 K./= N 0,   'True ~ (P 1 K./=? N 0)++  , N 1 K./= N 0,   'True ~ (N 1 K./=? N 0)+  , N 1 K./= N 0,   'True ~ (N 1 K./=? N 0)+  )++_testCmp =  Dict+_testCmp :: Dict+  ( P 0 <= P 0+  , P 0 <= N 0+  , N 0 <= P 0+  , N 0 <= N 0++  , N 2 <= N 1+  , N 1 <= N 0+  , N 0 <= P 1++  , P 0 <= P 1+  , P 1 <= P 2+  )++_testAdd  = Dict+_testAdd :: Dict+  ( P 0 ~ P 0 K.+ P 0+  , P 0 ~ N 0 K.+ N 0+  , P 0 ~ P 0 K.+ N 0+  , P 0 ~ N 0 K.+ P 0++  , P 1 ~ P 1 K.+ P 0+  , N 1 ~ N 1 K.+ N 0+  , P 1 ~ P 1 K.+ N 0+  , N 1 ~ N 1 K.+ P 0++  , P 1 ~ P 0 K.+ P 1+  , N 1 ~ N 0 K.+ N 1+  , N 1 ~ P 0 K.+ N 1+  , P 1 ~ N 0 K.+ P 1++  , P 2 ~ P 1 K.+ P 1+  , N 2 ~ N 1 K.+ N 1+  , P 0 ~ P 1 K.+ N 1+  , P 0 ~ N 1 K.+ P 1+  )++_testMul  = Dict+_testMul :: Dict+  ( P 0 ~ P 0 K.* P 0+  , P 0 ~ N 0 K.* N 0+  , P 0 ~ P 0 K.* N 0+  , P 0 ~ N 0 K.* P 0++  , P 0 ~ P 1 K.* P 0+  , P 0 ~ N 1 K.* N 0+  , P 0 ~ P 1 K.* N 0+  , P 0 ~ N 1 K.* P 0++  , P 0 ~ P 0 K.* P 1+  , P 0 ~ N 0 K.* N 1+  , P 0 ~ P 0 K.* N 1+  , P 0 ~ N 0 K.* P 1++  , P 1 ~ P 1 K.* P 1+  , P 1 ~ N 1 K.* N 1+  , N 1 ~ P 1 K.* N 1+  , N 1 ~ N 1 K.* P 1++  , P 2 ~ P 2 K.* P 1+  , P 2 ~ N 2 K.* N 1+  , N 2 ~ P 2 K.* N 1+  , N 2 ~ N 2 K.* P 1++  , P 6 ~ P 2 K.* P 3+  , P 6 ~ N 2 K.* N 3+  , N 6 ~ P 2 K.* N 3+  , N 6 ~ N 2 K.* P 3+  )++_testDiv  = Dict+_testDiv :: Dict+  ( P 0 ~ P 0 `K.Div` P 1+  , P 0 ~ N 0 `K.Div` N 1+  , P 0 ~ P 0 `K.Div` N 1+  , P 0 ~ N 0 `K.Div` P 1++  , P 1 ~ P 1 `K.Div` P 1+  , P 1 ~ N 1 `K.Div` N 1+  , N 1 ~ P 1 `K.Div` N 1+  , N 1 ~ N 1 `K.Div` P 1++  , P 2 ~ P 2 `K.Div` P 1+  , P 2 ~ N 2 `K.Div` N 1+  , N 2 ~ P 2 `K.Div` N 1+  , N 2 ~ N 2 `K.Div` P 1++  , P 1 ~ P 2 `K.Div` P 2+  , P 1 ~ N 2 `K.Div` N 2+  , N 1 ~ P 2 `K.Div` N 2+  , N 1 ~ N 2 `K.Div` P 2++  , P 1 ~ P 3 `K.Div` P 2+  , P 1 ~ N 3 `K.Div` N 2+  , N 2 ~ P 3 `K.Div` N 2+  , N 2 ~ N 3 `K.Div` P 2++  , P 0 ~ P 0 `K.Div` P 1+  , P 0 ~ N 0 `K.Div` N 1+  , P 0 ~ P 0 `K.Div` N 1+  , P 0 ~ N 0 `K.Div` P 1++  , P 0 ~ P 1 `K.Div` P 2+  , P 0 ~ N 1 `K.Div` N 2+  , N 1 ~ P 1 `K.Div` N 2+  , N 1 ~ N 1 `K.Div` P 2+  )++_testMod  = Dict+_testMod :: Dict+  ( P 0 ~ P 0 `K.Mod` P 1+  , P 0 ~ N 0 `K.Mod` N 1+  , P 0 ~ P 0 `K.Mod` N 1+  , P 0 ~ N 0 `K.Mod` P 1++  , P 0 ~ P 1 `K.Mod` P 1+  , P 0 ~ N 1 `K.Mod` N 1+  , P 0 ~ P 1 `K.Mod` N 1+  , P 0 ~ N 1 `K.Mod` P 1++  , P 0 ~ P 2 `K.Mod` P 1+  , P 0 ~ N 2 `K.Mod` N 1+  , P 0 ~ P 2 `K.Mod` N 1+  , P 0 ~ N 2 `K.Mod` P 1++  , P 0 ~ P 2 `K.Mod` P 2+  , P 0 ~ N 2 `K.Mod` N 2+  , P 0 ~ P 2 `K.Mod` N 2+  , P 0 ~ N 2 `K.Mod` P 2++  , P 1 ~ P 3 `K.Mod` P 2+  , N 1 ~ N 3 `K.Mod` N 2+  , N 1 ~ P 3 `K.Mod` N 2+  , P 1 ~ N 3 `K.Mod` P 2++  , P 0 ~ P 0 `K.Mod` P 1+  , P 0 ~ N 0 `K.Mod` N 1+  , P 0 ~ P 0 `K.Mod` N 1+  , P 0 ~ N 0 `K.Mod` P 1++  , P 1 ~ P 1 `K.Mod` P 2+  , N 1 ~ N 1 `K.Mod` N 2+  , N 1 ~ P 1 `K.Mod` N 2+  , P 1 ~ N 1 `K.Mod` P 2+  )++_testQuot  = Dict+_testQuot :: Dict+  ( P 0 ~ P 0 `K.Quot` P 1+  , P 0 ~ N 0 `K.Quot` N 1+  , P 0 ~ P 0 `K.Quot` N 1+  , P 0 ~ N 0 `K.Quot` P 1++  , P 1 ~ P 1 `K.Quot` P 1+  , P 1 ~ N 1 `K.Quot` N 1+  , N 1 ~ P 1 `K.Quot` N 1+  , N 1 ~ N 1 `K.Quot` P 1++  , P 2 ~ P 2 `K.Quot` P 1+  , P 2 ~ N 2 `K.Quot` N 1+  , N 2 ~ P 2 `K.Quot` N 1+  , N 2 ~ N 2 `K.Quot` P 1++  , P 1 ~ P 2 `K.Quot` P 2+  , P 1 ~ N 2 `K.Quot` N 2+  , N 1 ~ P 2 `K.Quot` N 2+  , N 1 ~ N 2 `K.Quot` P 2++  , P 1 ~ P 3 `K.Quot` P 2+  , P 1 ~ N 3 `K.Quot` N 2+  , N 1 ~ P 3 `K.Quot` N 2+  , N 1 ~ N 3 `K.Quot` P 2++  , P 0 ~ P 0 `K.Quot` P 1+  , P 0 ~ N 0 `K.Quot` N 1+  , P 0 ~ P 0 `K.Quot` N 1+  , P 0 ~ N 0 `K.Quot` P 1++  , P 0 ~ P 1 `K.Quot` P 2+  , P 0 ~ N 1 `K.Quot` N 2+  , P 0 ~ P 1 `K.Quot` N 2+  , P 0 ~ N 1 `K.Quot` P 2+  )++_testRem  = Dict+_testRem :: Dict+  ( P 0 ~ P 0 `K.Rem` P 1+  , P 0 ~ N 0 `K.Rem` N 1+  , P 0 ~ P 0 `K.Rem` N 1+  , P 0 ~ N 0 `K.Rem` P 1++  , P 0 ~ P 1 `K.Rem` P 1+  , P 0 ~ N 1 `K.Rem` N 1+  , P 0 ~ P 1 `K.Rem` N 1+  , P 0 ~ N 1 `K.Rem` P 1++  , P 0 ~ P 2 `K.Rem` P 1+  , P 0 ~ N 2 `K.Rem` N 1+  , P 0 ~ P 2 `K.Rem` N 1+  , P 0 ~ N 2 `K.Rem` P 1++  , P 0 ~ P 2 `K.Rem` P 2+  , P 0 ~ N 2 `K.Rem` N 2+  , P 0 ~ P 2 `K.Rem` N 2+  , P 0 ~ N 2 `K.Rem` P 2++  , P 1 ~ P 3 `K.Rem` P 2+  , N 1 ~ N 3 `K.Rem` N 2+  , P 1 ~ P 3 `K.Rem` N 2+  , N 1 ~ N 3 `K.Rem` P 2++  , P 0 ~ P 0 `K.Rem` P 1+  , P 0 ~ N 0 `K.Rem` N 1+  , P 0 ~ P 0 `K.Rem` N 1+  , P 0 ~ N 0 `K.Rem` P 1++  , P 1 ~ P 1 `K.Rem` P 2+  , N 1 ~ N 1 `K.Rem` N 2+  , P 1 ~ P 1 `K.Rem` N 2+  , N 1 ~ N 1 `K.Rem` P 2+  )++_testLog2 =  Dict+_testLog2 :: Dict+  ( P 0 ~ K.Log2 (P 1)+  , P 1 ~ K.Log2 (P 2)+  , P 1 ~ K.Log2 (P 3)+  , P 2 ~ K.Log2 (P 4)+  , P 2 ~ K.Log2 (P 5)+  , P 2 ~ K.Log2 (P 6)+  , P 2 ~ K.Log2 (P 7)+  , P 3 ~ K.Log2 (P 8)+  , P 3 ~ K.Log2 (P 9)+  , P 3 ~ K.Log2 (P 10)+  , P 3 ~ K.Log2 (P 11)+  , P 3 ~ K.Log2 (P 12)+  , P 3 ~ K.Log2 (P 13)+  , P 3 ~ K.Log2 (P 14)+  , P 3 ~ K.Log2 (P 15)+  , P 4 ~ K.Log2 (P 16)+  , P 4 ~ K.Log2 (P 17)+  , P 4 ~ K.Log2 (P 18)+  , P 4 ~ K.Log2 (P 19)+  , P 4 ~ K.Log2 (P 20)+  , P 4 ~ K.Log2 (P 21)+  , P 4 ~ K.Log2 (P 22)+  , P 4 ~ K.Log2 (P 23)+  , P 4 ~ K.Log2 (P 24)+  , P 4 ~ K.Log2 (P 25)+  , P 4 ~ K.Log2 (P 26)+  , P 4 ~ K.Log2 (P 27)+  , P 4 ~ K.Log2 (P 28)+  , P 4 ~ K.Log2 (P 29)+  , P 4 ~ K.Log2 (P 30)+  , P 4 ~ K.Log2 (P 31)+  , P 5 ~ K.Log2 (P 32)+  )++--------------------------------------------------------------------------------++assert+  :: String  -- ^ Test name+  -> Bool    -- ^ Successful is true+  -> IO Bool -- ^ Return the same 'Bool' given as input.+assert n x = do+  putStrLn ((if x then "[OK] " else "[FAIL] ") <> n)+  pure x++testsMain :: [IO Bool] -> IO a+testsMain xs = do+  oks <- sequence xs+  if and oks+     then do putStrLn "All tests passed successfully."+             exitSuccess+     else do putStrLn "Some tests failed."+             exitFailure++main :: IO ()+main = testsMain+  [ assert "integerVal . someIntegerVal == id" $+    flip all [-5 .. 5] $ \a ->+      case K.someIntegerVal a of+        K.SomeInteger pa ->+          a == K.integerVal pa++  , assert "integerVal' . someIntegerVal == id" $+    flip all [-5 .. 5] $ \a ->+      case K.someIntegerVal a of+        K.SomeInteger (_ :: Proxy a) ->+          a == K.integerVal' (proxy# @a)++  , assert "sameIntegerVal a a" $+    flip all [-5 .. 5] $ \a ->+      case K.someIntegerVal a of+        K.SomeInteger pa ->+          isJust (K.sameInteger pa pa)++  , assert "sameIntegerVal a a'" $+    flip all [-5 .. 5] $ \a ->+      case (K.someIntegerVal a, K.someIntegerVal a) of+        (K.SomeInteger pa1, K.SomeInteger pa2) ->+          isJust (K.sameInteger pa1 pa2)++  , assert "sameIntegerVal a b" $+    flip all (liftA2 (,) [-5 .. 5] [-5 .. 5])$ \(a, b) ->+      case (K.someIntegerVal a, K.someIntegerVal b) of+        (K.SomeInteger pa, K.SomeInteger pb)+          | a == b    -> isJust    (K.sameInteger pa pb)+          | otherwise -> isNothing (K.sameInteger pa pb)++  , assert "Eq SomeInteger" $+    flip all (liftA2 (,) [-5 .. 5] [-5 .. 5])$ \(a, b) ->+      (a == b) == (K.someIntegerVal a == K.someIntegerVal b)++  , assert "Ord SomeInteger" $+    flip all (liftA2 (,) [-5 .. 5] [-5 .. 5])$ \(a, b) ->+      (a `compare` b) == (K.someIntegerVal a `compare` K.someIntegerVal b)++  , assert "Show SomeInteger" $+    flip all [-5 .. 5] $ \i ->+      show i == show (K.someIntegerVal i)++  , assert "Read SomeInteger" $+    flip all [-5 .. 5] $ \i ->+      let str = show (i :: Integer)+      in readMaybe @Integer str+            == fmap (\(K.SomeInteger p) -> K.integerVal p)+                    (readMaybe @K.SomeInteger str)++  ]++