From 018ebecade82009a3410f19982dd435b6e0715d8 Mon Sep 17 00:00:00 2001
From: Tom Smeding <tom@tomsmeding.com>
Date: Sun, 14 Apr 2024 10:31:46 +0200
Subject: Rename inductive naturals to INat

---
 src/Data/Array/Mixed.hs           | 62 ++++++++++++-------------
 src/Data/Array/Nested.hs          |  6 +--
 src/Data/Array/Nested/Internal.hs | 72 ++++++++++++++---------------
 src/Data/INat.hs                  | 95 +++++++++++++++++++++++++++++++++++++++
 src/Data/Nat.hs                   | 87 -----------------------------------
 5 files changed, 166 insertions(+), 156 deletions(-)
 create mode 100644 src/Data/INat.hs
 delete mode 100644 src/Data/Nat.hs

(limited to 'src')

diff --git a/src/Data/Array/Mixed.hs b/src/Data/Array/Mixed.hs
index 2bbf81d..049a0c4 100644
--- a/src/Data/Array/Mixed.hs
+++ b/src/Data/Array/Mixed.hs
@@ -17,16 +17,16 @@ import Data.Kind
 import Data.Proxy
 import Data.Type.Equality
 import qualified Data.Vector.Storable as VS
-import qualified GHC.TypeLits as GHC
+import GHC.TypeLits
 import Unsafe.Coerce (unsafeCoerce)
 
-import Data.Nat
+import Data.INat
 
 
--- | The 'GHC.SNat' pattern synonym is complete, but it doesn't have a
+-- | The 'SNat' pattern synonym is complete, but it doesn't have a
 -- @COMPLETE@ pragma. This copy of it does.
-pattern GHC_SNat :: () => GHC.KnownNat n => GHC.SNat n
-pattern GHC_SNat = GHC.SNat
+pattern GHC_SNat :: () => KnownNat n => SNat n
+pattern GHC_SNat = SNat
 {-# COMPLETE GHC_SNat #-}
 
 
@@ -42,7 +42,7 @@ lemAppAssoc :: Proxy a -> Proxy b -> Proxy c -> (a ++ b) ++ c :~: a ++ (b ++ c)
 lemAppAssoc _ _ _ = unsafeCoerce Refl
 
 
-type IxX :: [Maybe GHC.Nat] -> Type
+type IxX :: [Maybe Nat] -> Type
 data IxX sh where
   IZX :: IxX '[]
   (::@) :: Int -> IxX sh -> IxX (Just n : sh)
@@ -52,23 +52,23 @@ infixr 5 ::@
 infixr 5 ::?
 
 -- | The part of a shape that is statically known.
-type StaticShapeX :: [Maybe GHC.Nat] -> Type
+type StaticShapeX :: [Maybe Nat] -> Type
 data StaticShapeX sh where
   SZX :: StaticShapeX '[]
-  (:$@) :: GHC.SNat n -> StaticShapeX sh -> StaticShapeX (Just n : sh)
+  (:$@) :: SNat n -> StaticShapeX sh -> StaticShapeX (Just n : sh)
   (:$?) :: () -> StaticShapeX sh -> StaticShapeX (Nothing : sh)
 deriving instance Show (StaticShapeX sh)
 infixr 5 :$@
 infixr 5 :$?
 
 -- | Evidence for the static part of a shape.
-type KnownShapeX :: [Maybe GHC.Nat] -> Constraint
+type KnownShapeX :: [Maybe Nat] -> Constraint
 class KnownShapeX sh where
   knownShapeX :: StaticShapeX sh
 instance KnownShapeX '[] where
   knownShapeX = SZX
-instance (GHC.KnownNat n, KnownShapeX sh) => KnownShapeX (Just n : sh) where
-  knownShapeX = GHC.natSing :$@ knownShapeX
+instance (KnownNat n, KnownShapeX sh) => KnownShapeX (Just n : sh) where
+  knownShapeX = natSing :$@ knownShapeX
 instance KnownShapeX sh => KnownShapeX (Nothing : sh) where
   knownShapeX = () :$? knownShapeX
 
@@ -76,8 +76,8 @@ type family Rank sh where
   Rank '[] = Z
   Rank (_ : sh) = S (Rank sh)
 
-type XArray :: [Maybe GHC.Nat] -> Type -> Type
-data XArray sh a = XArray (S.Array (GNat (Rank sh)) a)
+type XArray :: [Maybe Nat] -> Type -> Type
+data XArray sh a = XArray (S.Array (FromINat (Rank sh)) a)
   deriving (Show)
 
 zeroIdx :: StaticShapeX sh -> IxX sh
@@ -165,19 +165,19 @@ ssxIotaFrom i (_ :$@ ssh) = i : ssxIotaFrom (i+1) ssh
 ssxIotaFrom i (_ :$? ssh) = i : ssxIotaFrom (i+1) ssh
 
 lemRankApp :: StaticShapeX sh1 -> StaticShapeX sh2
-           -> GNat (Rank (sh1 ++ sh2)) :~: GNat (Rank sh1) GHC.+ GNat (Rank sh2)
+           -> FromINat (Rank (sh1 ++ sh2)) :~: FromINat (Rank sh1) + FromINat (Rank sh2)
 lemRankApp _ _ = unsafeCoerce Refl  -- TODO improve this
 
 lemRankAppComm :: StaticShapeX sh1 -> StaticShapeX sh2
-               -> GNat (Rank (sh1 ++ sh2)) :~: GNat (Rank (sh2 ++ sh1))
+               -> FromINat (Rank (sh1 ++ sh2)) :~: FromINat (Rank (sh2 ++ sh1))
 lemRankAppComm _ _ = unsafeCoerce Refl  -- TODO improve this
 
-lemKnownNatRank :: IxX sh -> Dict KnownNat (Rank sh)
+lemKnownNatRank :: IxX sh -> Dict KnownINat (Rank sh)
 lemKnownNatRank IZX = Dict
 lemKnownNatRank (_ ::@ sh) | Dict <- lemKnownNatRank sh = Dict
 lemKnownNatRank (_ ::? sh) | Dict <- lemKnownNatRank sh = Dict
 
-lemKnownNatRankSSX :: StaticShapeX sh -> Dict KnownNat (Rank sh)
+lemKnownNatRankSSX :: StaticShapeX sh -> Dict KnownINat (Rank sh)
 lemKnownNatRankSSX SZX = Dict
 lemKnownNatRankSSX (_ :$@ ssh) | Dict <- lemKnownNatRankSSX ssh = Dict
 lemKnownNatRankSSX (_ :$? ssh) | Dict <- lemKnownNatRankSSX ssh = Dict
@@ -201,14 +201,14 @@ shape (XArray arr) = go (knownShapeX @sh) (S.shapeL arr)
   where
     go :: StaticShapeX sh' -> [Int] -> IxX sh'
     go SZX [] = IZX
-    go (n :$@ ssh) (_ : l) = fromIntegral (GHC.fromSNat n) ::@ go ssh l
+    go (n :$@ ssh) (_ : l) = fromIntegral (fromSNat n) ::@ go ssh l
     go (() :$? ssh) (n : l) = n ::? go ssh l
     go _ _ = error "Invalid shapeL"
 
 fromVector :: forall sh a. S.Unbox a => IxX sh -> VS.Vector a -> XArray sh a
 fromVector sh v
   | Dict <- lemKnownNatRank sh
-  , Dict <- gknownNat (Proxy @(Rank sh))
+  , Dict <- knownNatFromINat (Proxy @(Rank sh))
   = XArray (S.fromVector (shapeLshape sh) v)
 
 toVector :: S.Unbox a => XArray sh a -> VS.Vector a
@@ -242,7 +242,7 @@ index xarr i
 append :: forall sh a. (KnownShapeX sh, S.Unbox a) => XArray sh a -> XArray sh a -> XArray sh a
 append (XArray a) (XArray b)
   | Dict <- lemKnownNatRankSSX (knownShapeX @sh)
-  , Dict <- gknownNat (Proxy @(Rank sh))
+  , Dict <- knownNatFromINat (Proxy @(Rank sh))
   = XArray (S.append a b)
 
 rerank :: forall sh sh1 sh2 a b.
@@ -252,14 +252,14 @@ rerank :: forall sh sh1 sh2 a b.
        -> XArray (sh ++ sh1) a -> XArray (sh ++ sh2) b
 rerank ssh ssh1 ssh2 f (XArray arr)
   | Dict <- lemKnownNatRankSSX ssh
-  , Dict <- gknownNat (Proxy @(Rank sh))
+  , Dict <- knownNatFromINat (Proxy @(Rank sh))
   , Dict <- lemKnownNatRankSSX ssh2
-  , Dict <- gknownNat (Proxy @(Rank sh2))
+  , Dict <- knownNatFromINat (Proxy @(Rank sh2))
   , Refl <- lemRankApp ssh ssh1
   , Refl <- lemRankApp ssh ssh2
   , Dict <- lemKnownNatRankSSX (ssxAppend ssh ssh2)  -- these two should be redundant but the
-  , Dict <- gknownNat (Proxy @(Rank (sh ++ sh2)))    -- solver is not clever enough
-  = XArray (S.rerank @(GNat (Rank sh)) @(GNat (Rank sh1)) @(GNat (Rank sh2))
+  , Dict <- knownNatFromINat (Proxy @(Rank (sh ++ sh2)))    -- solver is not clever enough
+  = XArray (S.rerank @(FromINat (Rank sh)) @(FromINat (Rank sh1)) @(FromINat (Rank sh2))
                 (\a -> unXArray (f (XArray a)))
                 arr)
   where
@@ -279,14 +279,14 @@ rerank2 :: forall sh sh1 sh2 a b c.
         -> XArray (sh ++ sh1) a -> XArray (sh ++ sh1) b -> XArray (sh ++ sh2) c
 rerank2 ssh ssh1 ssh2 f (XArray arr1) (XArray arr2)
   | Dict <- lemKnownNatRankSSX ssh
-  , Dict <- gknownNat (Proxy @(Rank sh))
+  , Dict <- knownNatFromINat (Proxy @(Rank sh))
   , Dict <- lemKnownNatRankSSX ssh2
-  , Dict <- gknownNat (Proxy @(Rank sh2))
+  , Dict <- knownNatFromINat (Proxy @(Rank sh2))
   , Refl <- lemRankApp ssh ssh1
   , Refl <- lemRankApp ssh ssh2
   , Dict <- lemKnownNatRankSSX (ssxAppend ssh ssh2)  -- these two should be redundant but the
-  , Dict <- gknownNat (Proxy @(Rank (sh ++ sh2)))  -- solver is not clever enough
-  = XArray (S.rerank2 @(GNat (Rank sh)) @(GNat (Rank sh1)) @(GNat (Rank sh2))
+  , Dict <- knownNatFromINat (Proxy @(Rank (sh ++ sh2)))  -- solver is not clever enough
+  = XArray (S.rerank2 @(FromINat (Rank sh)) @(FromINat (Rank sh1)) @(FromINat (Rank sh2))
                 (\a b -> unXArray (f (XArray a) (XArray b)))
                 arr1 arr2)
   where
@@ -296,7 +296,7 @@ rerank2 ssh ssh1 ssh2 f (XArray arr1) (XArray arr2)
 transpose :: forall sh a. KnownShapeX sh => [Int] -> XArray sh a -> XArray sh a 
 transpose perm (XArray arr)
   | Dict <- lemKnownNatRankSSX (knownShapeX @sh)
-  , Dict <- gknownNat (Proxy @(Rank sh))
+  , Dict <- knownNatFromINat (Proxy @(Rank sh))
   = XArray (S.transpose perm arr)
 
 transpose2 :: forall sh1 sh2 a.
@@ -306,9 +306,9 @@ transpose2 ssh1 ssh2 (XArray arr)
   | Refl <- lemRankApp ssh1 ssh2
   , Refl <- lemRankApp ssh2 ssh1
   , Dict <- lemKnownNatRankSSX (ssxAppend ssh1 ssh2)
-  , Dict <- gknownNat (Proxy @(Rank (sh1 ++ sh2)))
+  , Dict <- knownNatFromINat (Proxy @(Rank (sh1 ++ sh2)))
   , Dict <- lemKnownNatRankSSX (ssxAppend ssh2 ssh1)
-  , Dict <- gknownNat (Proxy @(Rank (sh2 ++ sh1)))
+  , Dict <- knownNatFromINat (Proxy @(Rank (sh2 ++ sh1)))
   , Refl <- lemRankAppComm ssh1 ssh2
   , let n1 = ssxLength ssh1
   = XArray (S.transpose (ssxIotaFrom n1 ssh2 ++ ssxIotaFrom 0 ssh1) arr)
diff --git a/src/Data/Array/Nested.hs b/src/Data/Array/Nested.hs
index aa7c7f9..0de3884 100644
--- a/src/Data/Array/Nested.hs
+++ b/src/Data/Array/Nested.hs
@@ -27,8 +27,8 @@ module Data.Array.Nested (
   Elt(mshape, mindex, mindexPartial, mlift),
   Primitive(..),
 
-  -- * Natural numbers
-  module Data.Nat,
+  -- * Inductive natural numbers
+  module Data.INat,
 
   -- * Further utilities / re-exports
   type (++),
@@ -39,4 +39,4 @@ import qualified Data.Vector.Unboxed as VU
 
 import Data.Array.Mixed
 import Data.Array.Nested.Internal
-import Data.Nat
+import Data.INat
diff --git a/src/Data/Array/Nested/Internal.hs b/src/Data/Array/Nested/Internal.hs
index 41fb1fd..15d72f0 100644
--- a/src/Data/Array/Nested/Internal.hs
+++ b/src/Data/Array/Nested/Internal.hs
@@ -21,7 +21,7 @@ TODO:
 * We should be more consistent in whether functions take a 'StaticShapeX'
   argument or a 'KnownShapeX' constraint.
 
-* Document the choice of using 'Nat' for ranks and 'GHC.Nat' for shapes. Point
+* Document the choice of using 'INat' for ranks and 'Nat' for shapes. Point
   being that we need to do induction over the former, but the latter need to be
   able to get large.
 
@@ -38,11 +38,11 @@ import Data.Type.Equality
 import qualified Data.Vector.Storable as VS
 import qualified Data.Vector.Storable.Mutable as VSM
 import Foreign.Storable (Storable)
-import qualified GHC.TypeLits as GHC
+import GHC.TypeLits
 
 import Data.Array.Mixed (XArray, IxX(..), KnownShapeX(..), StaticShapeX(..), type (++), pattern GHC_SNat)
 import qualified Data.Array.Mixed as X
-import Data.Nat
+import Data.INat
 
 
 type family Replicate n a where
@@ -53,25 +53,25 @@ type family MapJust l where
   MapJust '[] = '[]
   MapJust (x : xs) = Just x : MapJust xs
 
-lemKnownReplicate :: forall n. KnownNat n => Proxy n -> Dict KnownShapeX (Replicate n Nothing)
-lemKnownReplicate _ = X.lemKnownShapeX (go (knownNat @n))
+lemKnownReplicate :: forall n. KnownINat n => Proxy n -> Dict KnownShapeX (Replicate n Nothing)
+lemKnownReplicate _ = X.lemKnownShapeX (go (inatSing @n))
   where
-    go :: SNat m -> StaticShapeX (Replicate m Nothing)
+    go :: SINat m -> StaticShapeX (Replicate m Nothing)
     go SZ = SZX
     go (SS n) = () :$? go n
 
-lemRankReplicate :: forall n. KnownNat n => Proxy n -> X.Rank (Replicate n (Nothing @GHC.Nat)) :~: n
-lemRankReplicate _ = go (knownNat @n)
+lemRankReplicate :: forall n. KnownINat n => Proxy n -> X.Rank (Replicate n (Nothing @Nat)) :~: n
+lemRankReplicate _ = go (inatSing @n)
   where
-    go :: SNat m -> X.Rank (Replicate m (Nothing @GHC.Nat)) :~: m
+    go :: SINat m -> X.Rank (Replicate m (Nothing @Nat)) :~: m
     go SZ = Refl
     go (SS n) | Refl <- go n = Refl
 
-lemReplicatePlusApp :: forall n m a. KnownNat n => Proxy n -> Proxy m -> Proxy a
-                    -> Replicate (n + m) a :~: Replicate n a ++ Replicate m a
-lemReplicatePlusApp _ _ _ = go (knownNat @n)
+lemReplicatePlusApp :: forall n m a. KnownINat n => Proxy n -> Proxy m -> Proxy a
+                    -> Replicate (n +! m) a :~: Replicate n a ++ Replicate m a
+lemReplicatePlusApp _ _ _ = go (inatSing @n)
   where
-    go :: SNat n' -> Replicate (n' + m) a :~: Replicate n' a ++ Replicate m a
+    go :: SINat n' -> Replicate (n' +! m) a :~: Replicate n' a ++ Replicate m a
     go SZ = Refl
     go (SS n) | Refl <- go n = Refl
 
@@ -93,7 +93,7 @@ newtype Primitive a = Primitive a
 --
 -- Many of the methods for working on 'Mixed' arrays come from the 'Elt' type
 -- class.
-type Mixed :: [Maybe GHC.Nat] -> Type -> Type
+type Mixed :: [Maybe Nat] -> Type -> Type
 data family Mixed sh a
 
 newtype instance Mixed sh (Primitive a) = M_Primitive (XArray sh a)
@@ -117,7 +117,7 @@ deriving instance Show (Mixed (sh1 ++ sh2) a) => Show (Mixed sh1 (Mixed sh2 a))
 
 -- | Internal helper data family mirrorring 'Mixed' that consists of mutable
 -- vectors instead of 'XArray's.
-type MixedVecs :: Type -> [Maybe GHC.Nat] -> Type -> Type
+type MixedVecs :: Type -> [Maybe Nat] -> Type -> Type
 data family MixedVecs s sh a
 
 newtype instance MixedVecs s sh (Primitive a) = MV_Primitive (VS.MVector s a)
@@ -315,7 +315,7 @@ mgenerate sh f
   where
     checkBounds :: IxX sh' -> StaticShapeX sh' -> Bool
     checkBounds IZX SZX = True
-    checkBounds (n ::@ sh') (n' :$@ ssh') = n == fromIntegral (GHC.fromSNat n') && checkBounds sh' ssh'
+    checkBounds (n ::@ sh') (n' :$@ ssh') = n == fromIntegral (fromSNat n') && checkBounds sh' ssh'
     checkBounds (_ ::? sh') (() :$? ssh') = checkBounds sh' ssh'
 
 mtranspose :: forall sh a. (KnownShapeX sh, Elt a) => [Int] -> Mixed sh a -> Mixed sh a
@@ -325,29 +325,31 @@ mtranspose perm =
 
 
 -- | A rank-typed array: the number of dimensions of the array (its /rank/) is
--- represented on the type level as a 'Nat'.
+-- represented on the type level as a 'INat'.
 --
 -- Valid elements of a ranked arrays are described by the 'Elt' type class.
 -- Because 'Ranked' itself is also an instance of 'Elt', nested arrays are
 -- supported (and are represented as a single, flattened, struct-of-arrays
 -- array internally).
 --
--- Note that this 'Nat' is not a "GHC.TypeLits" natural, because we want a
+-- Note that this 'INat' is not a "GHC.TypeLits" natural, because we want a
 -- type-level natural that supports induction.
 --
 -- 'Ranked' is a newtype around a 'Mixed' of 'Nothing's.
-type Ranked :: Nat -> Type -> Type
+type Ranked :: INat -> Type -> Type
 newtype Ranked n a = Ranked (Mixed (Replicate n Nothing) a)
 deriving instance Show (Mixed (Replicate n Nothing) a) => Show (Ranked n a)
 
 -- | A shape-typed array: the full shape of the array (the sizes of its
--- dimensions) is represented on the type level as a list of 'Nat's.
+-- dimensions) is represented on the type level as a list of 'Nat's. Note that
+-- these are "GHC.TypeLits" naturals, because we do not need induction over
+-- them and we want very large arrays to be possible.
 --
 -- Like for 'Ranked', the valid elements are described by the 'Elt' type class,
 -- and 'Shaped' itself is again an instance of 'Elt' as well.
 --
 -- 'Shaped' is a newtype around a 'Mixed' of 'Just's.
-type Shaped :: [GHC.Nat] -> Type -> Type
+type Shaped :: [Nat] -> Type -> Type
 newtype Shaped sh a = Shaped (Mixed (MapJust sh) a)
 deriving instance Show (Mixed (MapJust sh) a) => Show (Shaped sh a)
 
@@ -364,7 +366,7 @@ newtype instance MixedVecs s sh (Shaped sh' a) = MV_Shaped (MixedVecs s sh (Mixe
 -- 'Ranked' and 'Shaped' can already be used at the top level of an array nest;
 -- these instances allow them to also be used as elements of arrays, thus
 -- making them first-class in the API.
-instance (KnownNat n, Elt a) => Elt (Ranked n a) where
+instance (KnownINat n, Elt a) => Elt (Ranked n a) where
   mshape (M_Ranked arr) | Dict <- lemKnownReplicate (Proxy @n) = mshape arr
   mindex (M_Ranked arr) i | Dict <- lemKnownReplicate (Proxy @n) = Ranked (mindex arr i)
 
@@ -431,14 +433,14 @@ instance (KnownNat n, Elt a) => Elt (Ranked n a) where
 -- | The shape of a shape-typed array given as a list of 'SNat' values.
 data SShape sh where
   ShNil :: SShape '[]
-  ShCons :: GHC.SNat n -> SShape sh -> SShape (n : sh)
+  ShCons :: SNat n -> SShape sh -> SShape (n : sh)
 deriving instance Show (SShape sh)
 infixr 5 `ShCons`
 
 -- | A statically-known shape of a shape-typed array.
 class KnownShape sh where knownShape :: SShape sh
 instance KnownShape '[] where knownShape = ShNil
-instance (GHC.KnownNat n, KnownShape sh) => KnownShape (n : sh) where knownShape = ShCons GHC.natSing knownShape
+instance (KnownNat n, KnownShape sh) => KnownShape (n : sh) where knownShape = ShCons natSing knownShape
 
 sshapeKnown :: SShape sh -> Dict KnownShape sh
 sshapeKnown ShNil = Dict
@@ -531,7 +533,7 @@ rewriteMixed Refl x = x
 -- ====== API OF RANKED ARRAYS ====== --
 
 -- | An index into a rank-typed array.
-type IxR :: Nat -> Type
+type IxR :: INat -> Type
 data IxR n where
   IZR :: IxR Z
   (:::) :: Int -> IxR n -> IxR (S n)
@@ -547,7 +549,7 @@ ixCvtRX IZR = IZX
 ixCvtRX (n ::: idx) = n ::? ixCvtRX idx
 
 
-rshape :: forall n a. (KnownNat n, Elt a) => Ranked n a -> IxR n
+rshape :: forall n a. (KnownINat n, Elt a) => Ranked n a -> IxR n
 rshape (Ranked arr)
   | Dict <- lemKnownReplicate (Proxy @n)
   , Refl <- lemRankReplicate (Proxy @n)
@@ -556,19 +558,19 @@ rshape (Ranked arr)
 rindex :: Elt a => Ranked n a -> IxR n -> a
 rindex (Ranked arr) idx = mindex arr (ixCvtRX idx)
 
-rindexPartial :: forall n m a. (KnownNat n, Elt a) => Ranked (n + m) a -> IxR n -> Ranked m a
+rindexPartial :: forall n m a. (KnownINat n, Elt a) => Ranked (n +! m) a -> IxR n -> Ranked m a
 rindexPartial (Ranked arr) idx =
   Ranked (mindexPartial @a @(Replicate n Nothing) @(Replicate m Nothing)
             (rewriteMixed (lemReplicatePlusApp (Proxy @n) (Proxy @m) (Proxy @Nothing)) arr)
             (ixCvtRX idx))
 
-rgenerate :: forall n a. (KnownNat n, Elt a) => IxR n -> (IxR n -> a) -> Ranked n a
+rgenerate :: forall n a. (KnownINat n, Elt a) => IxR n -> (IxR n -> a) -> Ranked n a
 rgenerate sh f
   | Dict <- lemKnownReplicate (Proxy @n)
   , Refl <- lemRankReplicate (Proxy @n)
   = Ranked (mgenerate (ixCvtRX sh) (f . ixCvtXR))
 
-rlift :: forall n1 n2 a. (KnownNat n2, Elt a)
+rlift :: forall n1 n2 a. (KnownINat n2, Elt a)
       => (forall sh' b. KnownShapeX sh' => Proxy sh' -> XArray (Replicate n1 Nothing ++ sh') b -> XArray (Replicate n2 Nothing ++ sh') b)
       -> Ranked n1 a -> Ranked n2 a
 rlift f (Ranked arr)
@@ -576,7 +578,7 @@ rlift f (Ranked arr)
   = Ranked (mlift f arr)
 
 rsumOuter1 :: forall n a.
-              (Storable a, Num a, KnownNat n, forall sh. Coercible (Mixed sh a) (XArray sh a))
+              (Storable a, Num a, KnownINat n, forall sh. Coercible (Mixed sh a) (XArray sh a))
            => Ranked (S n) a -> Ranked n a
 rsumOuter1 (Ranked arr)
   | Dict <- lemKnownReplicate (Proxy @n)
@@ -586,7 +588,7 @@ rsumOuter1 (Ranked arr)
     . coerce @(Mixed (Replicate (S n) Nothing) a) @(XArray (Replicate (S n) Nothing) a)
     $ arr
 
-rtranspose :: forall n a. (KnownNat n, Elt a) => [Int] -> Ranked n a -> Ranked n a
+rtranspose :: forall n a. (KnownINat n, Elt a) => [Int] -> Ranked n a -> Ranked n a
 rtranspose perm (Ranked arr)
   | Dict <- lemKnownReplicate (Proxy @n)
   = Ranked (mtranspose perm arr)
@@ -600,7 +602,7 @@ rtranspose perm (Ranked arr)
 -- (traditionally called \"@Fin@\"). Note that because the shape of a
 -- shape-typed array is known statically, you can also retrieve the array shape
 -- from a 'KnownShape' dictionary.
-type IxS :: [GHC.Nat] -> Type
+type IxS :: [Nat] -> Type
 data IxS sh where
   IZS :: IxS '[]
   (::$) :: Int -> IxS sh -> IxS (n : sh)
@@ -608,7 +610,7 @@ infixr 5 ::$
 
 cvtSShapeIxS :: SShape sh -> IxS sh
 cvtSShapeIxS ShNil = IZS
-cvtSShapeIxS (ShCons n sh) = fromIntegral (GHC.fromSNat n) ::$ cvtSShapeIxS sh
+cvtSShapeIxS (ShCons n sh) = fromIntegral (fromSNat n) ::$ cvtSShapeIxS sh
 
 ixCvtXS :: SShape sh -> IxX (MapJust sh) -> IxS sh
 ixCvtXS ShNil IZX = IZS
@@ -644,13 +646,13 @@ slift f (Shaped arr)
   = Shaped (mlift f arr)
 
 ssumOuter1 :: forall sh n a.
-              (Storable a, Num a, GHC.KnownNat n, KnownShape sh, forall sh'. Coercible (Mixed sh' a) (XArray sh' a))
+              (Storable a, Num a, KnownNat n, KnownShape sh, forall sh'. Coercible (Mixed sh' a) (XArray sh' a))
            => Shaped (n : sh) a -> Shaped sh a
 ssumOuter1 (Shaped arr)
   | Dict <- lemKnownMapJust (Proxy @sh)
   = Shaped
     . coerce @(XArray (MapJust sh) a) @(Mixed (MapJust sh) a)
-    . X.sumOuter (GHC.natSing @n :$@ SZX) (knownShapeX @(MapJust sh))
+    . X.sumOuter (natSing @n :$@ SZX) (knownShapeX @(MapJust sh))
     . coerce @(Mixed (Just n : MapJust sh) a) @(XArray (Just n : MapJust sh) a)
     $ arr
 
diff --git a/src/Data/INat.hs b/src/Data/INat.hs
new file mode 100644
index 0000000..f7523ee
--- /dev/null
+++ b/src/Data/INat.hs
@@ -0,0 +1,95 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE ViewPatterns #-}
+{-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}
+module Data.INat where
+
+import Data.Proxy
+import Numeric.Natural
+import GHC.TypeLits
+
+
+-- | Evidence for the constraint @c a@.
+data Dict c a where
+  Dict :: c a => Dict c a
+
+-- | An inductive peano natural number. Intended to be used at the type level.
+data INat = Z | S INat
+  deriving (Show)
+
+-- | Singleton for a 'INat'.
+data SINat n where
+  SZ :: SINat Z
+  SS :: SINat n -> SINat (S n)
+deriving instance Show (SINat n)
+
+-- | A singleton 'SINat' corresponding to @n@.
+class KnownINat n where inatSing :: SINat n
+instance KnownINat Z where inatSing = SZ
+instance KnownINat n => KnownINat (S n) where inatSing = SS inatSing
+
+-- | Explicitly bidirectional pattern synonym that converts between a singleton
+-- 'SINat' and evidence of a 'KnownINat' constraint. Analogous to 'GHC.SNat'.
+pattern SINat' :: () => KnownINat n => SINat n
+pattern SINat' <- (snatKnown -> Dict)
+  where SINat' = inatSing
+
+-- | A 'KnownINat' dictionary is just a singleton natural, so we can create
+-- evidence of 'KnownNat' given an 'SINat'.
+snatKnown :: SINat n -> Dict KnownINat n
+snatKnown SZ = Dict
+snatKnown (SS n) | Dict <- snatKnown n = Dict
+
+-- | Convert a 'INat' to a normal number.
+fromINat :: INat -> Natural
+fromINat Z = 0
+fromINat (S n) = 1 + fromINat n
+
+-- | Convert an 'SINat' to a normal number.
+fromSINat :: SINat n -> Natural
+fromSINat SZ = 0
+fromSINat (SS n) = 1 + fromSINat n
+
+-- | The value of a known inductive natural as a value-level integer.
+inatVal :: forall n. KnownINat n => Proxy n -> Natural
+inatVal _ = fromSINat (inatSing @n)
+
+-- | Add two 'INat's
+type family n +! m where
+  Z +! m = m
+  S n +! m = S (n +! m)
+
+-- | Convert a 'INat' to a "GHC.TypeLits" 'G.Nat'.
+type family FromINat n where
+  FromINat Z = 0
+  FromINat (S n) = 1 + FromINat n
+
+-- | If an inductive 'INat' is known, then the corresponding "GHC.TypeLits"
+-- 'G.Nat' is also known.
+knownNatFromINat :: KnownINat n => Proxy n -> Dict KnownNat (FromINat n)
+knownNatFromINat (Proxy @n) = go (SINat' @n)
+  where
+    go :: SINat m -> Dict KnownNat (FromINat m)
+    go SZ = Dict
+    go (SS n) | Dict <- go n = Dict
+
+-- * Some type-level inductive naturals
+
+type I0 = Z
+type I1 = S I0
+type I2 = S I1
+type I3 = S I2
+type I4 = S I3
+type I5 = S I4
+type I6 = S I5
+type I7 = S I6
+type I8 = S I7
+type I9 = S I8
diff --git a/src/Data/Nat.hs b/src/Data/Nat.hs
deleted file mode 100644
index b154f67..0000000
--- a/src/Data/Nat.hs
+++ /dev/null
@@ -1,87 +0,0 @@
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE GADTs #-}
-{-# LANGUAGE PolyKinds #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE StandaloneDeriving #-}
-{-# LANGUAGE TypeApplications #-}
-{-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE TypeOperators #-}
-{-# LANGUAGE UndecidableInstances #-}
-{-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}
-module Data.Nat where
-
-import Data.Proxy
-import Numeric.Natural
-import qualified GHC.TypeLits as G
-
-
--- | Evidence for the constraint @c a@.
-data Dict c a where
-  Dict :: c a => Dict c a
-
--- | A peano natural number. Intended to be used at the type level.
-data Nat = Z | S Nat
-  deriving (Show)
-
--- | Singleton for a 'Nat'.
-data SNat n where
-  SZ :: SNat Z
-  SS :: SNat n -> SNat (S n)
-deriving instance Show (SNat n)
-
--- | A singleton 'SNat' corresponding to @n@.
-class KnownNat n where knownNat :: SNat n
-instance KnownNat Z where knownNat = SZ
-instance KnownNat n => KnownNat (S n) where knownNat = SS knownNat
-
--- | Convert a 'Nat' to a normal number.
-unNat :: Nat -> Natural
-unNat Z = 0
-unNat (S n) = 1 + unNat n
-
--- | Convert an 'SNat' to a normal number.
-unSNat :: SNat n -> Natural
-unSNat SZ = 0
-unSNat (SS n) = 1 + unSNat n
-
--- | Convert an 'SNat' to an integer.
-unSNat' :: SNat n -> Int
-unSNat' = fromIntegral . unSNat
-
--- | A 'KnownNat' dictionary is just a singleton natural, so we can create
--- evidence of 'KnownNat' given an 'SNat'.
-snatKnown :: SNat n -> Dict KnownNat n
-snatKnown SZ = Dict
-snatKnown (SS n) | Dict <- snatKnown n = Dict
-
--- | Add two 'Nat's
-type family n + m where
-  Z + m = m
-  S n + m = S (n + m)
-
--- | Convert a 'Nat' to a "GHC.TypeLits" 'G.Nat'.
-type family GNat n where
-  GNat Z = 0
-  GNat (S n) = 1 G.+ GNat n
-
--- | If an inductive 'Nat' is known, then the corresponding "GHC.TypeLits"
--- 'G.Nat' is also known.
-gknownNat :: KnownNat n => Proxy n -> Dict G.KnownNat (GNat n)
-gknownNat (Proxy @n) = go (knownNat @n)
-  where
-    go :: SNat m -> Dict G.KnownNat (GNat m)
-    go SZ = Dict
-    go (SS n) | Dict <- go n = Dict
-
--- * Some type-level naturals
-
-type N0 = Z
-type N1 = S N0
-type N2 = S N1
-type N3 = S N2
-type N4 = S N3
-type N5 = S N4
-type N6 = S N5
-type N7 = S N6
-type N8 = S N7
-type N9 = S N8
-- 
cgit v1.2.3-70-g09d2