[commit: packages/base] master: Clean-up implementation of GHC.TypeLits. (fdd40f2)

[git at git.haskell.org]

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

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

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

commit fdd40f22817b6beb9cc26ec0e605ea73fac2dcdb
Author: Iavor S. Diatchki <diatchki at galois.com>
Date:   Wed Oct 9 19:25:37 2013 -0700

    Clean-up implementation of GHC.TypeLits.
    
    For a more detailed explanation please see the following commint in GHC:
    8af2dbea315f5d0c9f6b1db39d78cee7b6cc43f1


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

fdd40f22817b6beb9cc26ec0e605ea73fac2dcdb
 GHC/TypeLits.hs |   84 ++++++++++++++++++++++---------------------------------
 1 file changed, 34 insertions(+), 50 deletions(-)

diff --git a/GHC/TypeLits.hs b/GHC/TypeLits.hs
index 8609e01..ec48bf1 100644
--- a/GHC/TypeLits.hs
+++ b/GHC/TypeLits.hs
@@ -2,9 +2,8 @@
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
-{-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE ExistentialQuantification #-}
@@ -22,7 +21,8 @@ module GHC.TypeLits
     Nat, Symbol
 
     -- * Linking type and value level
-  , KnownNat(..), KnownSymbol(..)
+  , KnownNat, natVal
+  , KnownSymbol, symbolVal
   , SomeNat(..), SomeSymbol(..)
   , someNatVal, someSymbolVal
 
@@ -36,7 +36,7 @@ import GHC.Num(Integer)
 import GHC.Base(String)
 import GHC.Show(Show(..))
 import GHC.Read(Read(..))
-import GHC.Prim(magicSingI)
+import GHC.Prim(magicDict)
 import Data.Maybe(Maybe(..))
 import Data.Proxy(Proxy(..))
 
@@ -52,12 +52,22 @@ data Symbol
 -- | This class gives the integer associated with a type-level natural.
 -- There are instances of the class for every concrete literal: 0, 1, 2, etc.
 class KnownNat (n :: Nat) where
-  natVal :: proxy n -> Integer
+  natSing :: SNat n
 
 -- | This class gives the integer associated with a type-level symbol.
 -- There are instances of the class for every concrete literal: "hello", etc.
 class KnownSymbol (n :: Symbol) where
-  symbolVal :: proxy n -> String
+  symbolSing :: SSymbol n
+
+natVal :: forall n proxy. KnownNat n => proxy n -> Integer
+natVal _ = case natSing :: SNat n of
+             SNat x -> x
+
+symbolVal :: forall n proxy. KnownSymbol n => proxy n -> String
+symbolVal _ = case symbolSing :: SSymbol n of
+                SSymbol x -> x
+
+
 
 -- | This type represents unknown type-level natural numbers.
 data SomeNat    = forall n. KnownNat n    => SomeNat    (Proxy n)
@@ -65,23 +75,19 @@ data SomeNat    = forall n. KnownNat n    => SomeNat    (Proxy n)
 -- | This type represents unknown type-level symbols.
 data SomeSymbol = forall n. KnownSymbol n => SomeSymbol (Proxy n)
 
-instance SingI n => KnownNat n where
-  natVal _ = case sing :: Sing n of
-               SNat x -> x
-
-instance SingI n => KnownSymbol n where
-  symbolVal _ = case sing :: Sing n of
-                  SSym x -> x
-
 -- | Convert an integer into an unknown type-level natural.
+{-# NOINLINE someNatVal #-}
 someNatVal :: Integer -> Maybe SomeNat
 someNatVal n
-  | n >= 0        = Just (forgetSingNat (SNat n))
+  | n >= 0        = Just (withSNat SomeNat (SNat n) Proxy)
   | otherwise     = Nothing
 
 -- | Convert a string into an unknown type-level symbol.
+{-# NOINLINE someSymbolVal #-}
 someSymbolVal :: String -> SomeSymbol
-someSymbolVal n   = forgetSingSymbol (SSym n)
+someSymbolVal n   = withSSymbol SomeSymbol (SSymbol n) Proxy
+
+
 
 instance Eq SomeNat where
   SomeNat x == SomeNat y = natVal x == natVal y
@@ -144,41 +150,19 @@ type family (m :: Nat) - (n :: Nat) :: Nat
 --------------------------------------------------------------------------------
 -- PRIVATE:
 
--- | This is an internal GHC class.  It has built-in instances in the compiler.
-class SingI a where
-  sing :: Sing a
-
--- | This is used only in the type of the internal `SingI` class.
-data family      Sing (n :: k)
-newtype instance Sing (n :: Nat)    = SNat Integer
-newtype instance Sing (n :: Symbol) = SSym String
-
-
-{- PRIVATE:
-The functions below convert a value of type `Sing n` into a dictionary
-for `SingI` for `Nat` and `Symbol`.
-
-NOTE: The implementation is a bit of a hack at present,
-hence all the very special annotations.  See Note [magicSingIId magic]
-for more details.
--}
-forgetSingNat :: forall n. Sing (n :: Nat) -> SomeNat
-forgetSingNat x = withSingI x it Proxy
-  where
-  it :: SingI n => Proxy n -> SomeNat
-  it = SomeNat
-
-forgetSingSymbol :: forall n. Sing (n :: Symbol) -> SomeSymbol
-forgetSingSymbol x = withSingI x it Proxy
-  where
-  it :: SingI n => Proxy n -> SomeSymbol
-  it = SomeSymbol
+newtype SNat    (n :: Nat)    = SNat    Integer
+newtype SSymbol (s :: Symbol) = SSymbol String
 
--- | THIS IS NOT SUPPOSED TO MAKE SENSE.
--- See Note [magicSingIId magic]
-{-# NOINLINE withSingI #-}
-withSingI :: Sing n -> (SingI n => a) -> a
-withSingI x = magicSingI x ((\f -> f) :: () -> ())
+data WrapN a b = WrapN (KnownNat    a => Proxy a -> b)
+data WrapS a b = WrapS (KnownSymbol a => Proxy a -> b)
 
+-- See Note [magicDictId magic] in "basicType/MkId.hs"
+withSNat :: (KnownNat a => Proxy a -> b)
+         -> SNat a      -> Proxy a -> b
+withSNat f x y = magicDict (WrapN f) x y
 
+-- See Note [magicDictId magic] in "basicType/MkId.hs"
+withSSymbol :: (KnownSymbol a => Proxy a -> b)
+            -> SSymbol a      -> Proxy a -> b
+withSSymbol f x y = magicDict (WrapS f) x y