Add ToINat

1 files changed, 6 insertions, 1 deletions

diff --git a/src/Data/INat.hs b/src/Data/INat.hs
index f7523ee..7a495ca 100644
--- a/src/Data/INat.hs
+++ b/src/Data/INat.hs
@@ -43,7 +43,7 @@ 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'.
+-- evidence of 'KnownINat' given an 'SINat'.
 snatKnown :: SINat n -> Dict KnownINat n
 snatKnown SZ = Dict
 snatKnown (SS n) | Dict <- snatKnown n = Dict
@@ -72,6 +72,11 @@ type family FromINat n where
   FromINat Z = 0
   FromINat (S n) = 1 + FromINat n
 
+-- | Convert a "GHC.TypeLits" 'G.Nat' to a 'INat'.
+type family ToINat n where
+  ToINat 0 = Z
+  ToINat n = S (ToINat (n - 1))
+
 -- | 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)