[commit: packages/base] master: Redo <= with a type synonym instead of a class, add instance for boolean singletons, remove (-) (3323f41)

[git at git.haskell.org]

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

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

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

commit 3323f41778c5b5209cfd905aec4b7558df7755ee
Author: Iavor S. Diatchki <iavor.diatchki at gmail.com>
Date:   Sun Sep 8 14:38:47 2013 -0700

    Redo <= with a type synonym instead of a class, add instance for boolean singletons, remove (-)


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

3323f41778c5b5209cfd905aec4b7558df7755ee
 GHC/TypeLits.hs |   35 +++++++++++++++++++++++++++--------
 1 file changed, 27 insertions(+), 8 deletions(-)

diff --git a/GHC/TypeLits.hs b/GHC/TypeLits.hs
index c2e4906..f71f654 100644
--- a/GHC/TypeLits.hs
+++ b/GHC/TypeLits.hs
@@ -8,9 +8,9 @@
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE UndecidableInstances #-}
-{-# LANGUAGE MultiParamTypeClasses #-}  -- for <=
 {-# LANGUAGE RankNTypes #-}             -- for SingI magic
 {-# LANGUAGE ScopedTypeVariables #-}    -- for SingI magic
+{-# LANGUAGE ConstraintKinds #-}        -- for <=
 {-# OPTIONS_GHC -XNoImplicitPrelude #-}
 {-| This module is an internal GHC module.  It declares the constants used
 in the implementation of type-level natural numbers.  The programmer interface
@@ -29,10 +29,9 @@ module GHC.TypeLits
 
     -- * Functions on type nats
   , type (<=), type (<=?), type (+), type (*), type (^)
-  , type (-)
 
     -- * Comparing for equality
-  , type (:~:) (..), eqSingNat, eqSingSym
+  , type (:~:) (..), eqSingNat, eqSingSym, eqSingBool
 
     -- * Destructing type-nat singletons.
   , isZero, IsZero(..)
@@ -83,6 +82,10 @@ newtype instance Sing (n :: Nat)    = SNat Integer
 
 newtype instance Sing (n :: Symbol) = SSym String
 
+data instance Sing (n :: Bool) where
+  SFalse :: Sing False
+  STrue  :: Sing True
+
 --------------------------------------------------------------------------------
 
 -- | The class 'SingI' provides a \"smart\" constructor for singleton types.
@@ -99,11 +102,13 @@ class SingI a where
 singByProxy :: SingI n => proxy n -> Sing n
 singByProxy _ = sing
 
+instance SingI False where sing = SFalse
+instance SingI True  where sing = STrue
+
 
 --------------------------------------------------------------------------------
 -- | Comparison of type-level naturals.
-class (m <=? n) ~ True => (m :: Nat) <= (n :: Nat)
-instance ((m <=? n) ~ True) => m <= n
+type x <= y = (x <=? y) ~ True
 
 type family (m :: Nat) <=? (n :: Nat) :: Bool
 
@@ -116,9 +121,7 @@ type family (m :: Nat) * (n :: Nat) :: Nat
 -- | Exponentiation of type-level naturals.
 type family (m :: Nat) ^ (n :: Nat) :: Nat
 
--- | Subtraction of type-level naturals.
--- Note that this operation is unspecified for some inputs.
-type family (m :: Nat) - (n :: Nat) :: Nat
+
 
 
 --------------------------------------------------------------------------------
@@ -144,6 +147,13 @@ instance SingE (KindParam :: KindIs Symbol) where
   type DemoteRep (KindParam :: KindIs Symbol) = String
   fromSing (SSym s) = s
 
+
+instance SingE (KindParam :: KindIs Bool) where
+  type DemoteRep (KindParam :: KindIs Bool) = Bool
+  fromSing SFalse = False
+  fromSing STrue  = True
+
+
 {- | A convenient name for the type used to representing the values
 for a particular singleton family.  For example, @Demote 2 ~ Integer@,
 and also @Demote 3 ~ Integer@, but @Demote "Hello" ~ String at . -}
@@ -185,6 +195,9 @@ instance ToSing (KindParam :: KindIs Nat) where
 instance ToSing (KindParam :: KindIs Symbol) where
   toSing n          = Just (incoherentForgetSing (SSym n))
 
+instance ToSing (KindParam :: KindIs Bool) where
+  toSing False      = Just (SomeSing SFalse)
+  toSing True       = Just (SomeSing STrue)
 
 
 {- PRIVATE:
@@ -329,4 +342,10 @@ eqSingSym x y
   | otherwise                 = Nothing
 
 
+eqSingBool :: Sing (m :: Bool) -> Sing (n :: Bool) -> Maybe (m :~: n)
+eqSingBool STrue STrue    = Just Refl
+eqSingBool SFalse SFalse  = Just Refl
+eqSingBool _ _            = Nothing
+
+