[commit: packages/base] master: Add type functions (-) and ToNat1; Turn FromNat1 into a closed family. (fc90436)

[git at git.haskell.org]

Repository : ssh://git@git.haskell.org/base

On branch  : master
Link       : http://ghc.haskell.org/trac/ghc/changeset/fc904366944214c135f31492f96be453c9760cf8/base

>---------------------------------------------------------------

commit fc904366944214c135f31492f96be453c9760cf8
Author: Iavor S. Diatchki <iavor.diatchki at gmail.com>
Date:   Tue Sep 24 06:22:54 2013 -0700

    Add type functions (-) and ToNat1;  Turn FromNat1 into a closed family.


>---------------------------------------------------------------

fc904366944214c135f31492f96be453c9760cf8
 GHC/TypeLits.hs |   17 +++++++++++------
 1 file changed, 11 insertions(+), 6 deletions(-)

diff --git a/GHC/TypeLits.hs b/GHC/TypeLits.hs
index 3f95646..d6eba25 100644
--- a/GHC/TypeLits.hs
+++ b/GHC/TypeLits.hs
@@ -31,7 +31,7 @@ module GHC.TypeLits
   , withSing, singThat
 
     -- * Functions on type nats
-  , type (<=), type (<=?), type (+), type (*), type (^)
+  , type (<=), type (<=?), type (+), type (*), type (^), type (-)
 
     -- * Comparing for equality
   , type (:~:) (..), eqSingNat, eqSingSym, eqSingBool
@@ -44,7 +44,7 @@ module GHC.TypeLits
 
 
     -- * Matching on type-nats
-  , Nat1(..), FromNat1
+  , Nat1(..), FromNat1, ToNat1
 
     -- * Kind parameters
   , KindIs(..), Demote, DemoteRep
@@ -124,7 +124,8 @@ type family (m :: Nat) * (n :: Nat) :: Nat
 -- | Exponentiation of type-level naturals.
 type family (m :: Nat) ^ (n :: Nat) :: Nat
 
-
+-- | Subtraction of type-level naturals.
+type family (m :: Nat) - (n :: Nat) :: Nat
 
 
 --------------------------------------------------------------------------------
@@ -312,9 +313,13 @@ instance Show (IsEven n) where
 -- Used both at the type and at the value level.
 data Nat1 = Zero | Succ Nat1
 
-type family FromNat1 (n :: Nat1) :: Nat
-type instance FromNat1 Zero     = 0
-type instance FromNat1 (Succ n) = 1 + FromNat1 n
+type family ToNat1 (n :: Nat) where
+  ToNat1 0 = Zero
+  ToNat1 x = Succ (ToNat1 (x - 1))
+
+type family FromNat1 (n :: Nat1) :: Nat where
+  FromNat1 Zero     = 0
+  FromNat1 (Succ n) = 1 + FromNat1 n
 
 --------------------------------------------------------------------------------