[commit: base] master: Redo and cleanup the change replacing `unsafe*` with `toSing` (14bd3c1)

[Iavor Diatchki]

Repository : ssh://darcs.haskell.org//srv/darcs/packages/base

On branch  : master

https://github.com/ghc/packages-base/commit/14bd3c1a38be411f1711fc80dafa28b7a6f14dda

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

commit 14bd3c1a38be411f1711fc80dafa28b7a6f14dda
Author: Iavor S. Diatchki <diatchki at galois.com>
Date:   Thu May 30 19:58:21 2013 -0700

    Redo and cleanup the change replacing `unsafe*` with `toSing`

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

 GHC/TypeLits.hs |  118 +++++++++++++++++++++++++++++++++++++++++++------------
 1 files changed, 92 insertions(+), 26 deletions(-)

diff --git a/GHC/TypeLits.hs b/GHC/TypeLits.hs
index f8b759e..86c8958 100644
--- a/GHC/TypeLits.hs
+++ b/GHC/TypeLits.hs
@@ -9,6 +9,8 @@
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE MultiParamTypeClasses #-}  -- for <=
+{-# LANGUAGE RankNTypes #-}             -- for SingI magic
+{-# LANGUAGE ScopedTypeVariables #-}    -- for SingI magic
 {-# 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
@@ -19,8 +21,8 @@ module GHC.TypeLits
     Nat, Symbol
 
     -- * Linking type and value level
-  , Sing, SingI, SingE, SingRep, sing, fromSing
-  , unsafeSingNat, unsafeSingSymbol
+  , Sing, SingI, SingE, SingRep, sing, singByProxy, fromSing
+  , SomeSing(..), ToSing(..), SomeNat, SomeSymbol
 
     -- * Working with singletons
   , withSing, singThat
@@ -43,27 +45,28 @@ module GHC.TypeLits
   , Nat1(..), FromNat1
 
     -- * Kind parameters
-  , OfKind(..), Demote, DemoteRep
+  , KindIs(..), Demote, DemoteRep
   , KindOf
   ) where
 
-import GHC.Base(Eq((==)), Bool(..), ($), otherwise, (.))
+import GHC.Base(Eq((==)), Ord((>=)), Bool(..), ($), otherwise, (.){-, seq)-})
 import GHC.Num(Integer, (-))
 import GHC.Base(String)
 import GHC.Read(Read(..))
 import GHC.Show(Show(..))
+import GHC.Prim(magicSingI)
 import Unsafe.Coerce(unsafeCoerce)
 -- import Data.Bits(testBit,shiftR)
 import Data.Maybe(Maybe(..))
 import Data.List((++))
 
 -- | (Kind) A kind useful for passing kinds as parameters.
-data OfKind (a :: *) = KindParam
+data KindIs (a :: *) = KindParam
 
 {- | A shortcut for naming the kind parameter corresponding to the
-kind of a some type.  For example, @KindOf Int ~ (KindParam :: OfKind *)@,
-but @KindOf 2 ~ (KindParam :: OfKind Nat)@. -}
-type KindOf (a :: k) = (KindParam :: OfKind k)
+kind of a some type.  For example, @KindOf Int ~ (KindParam :: KindIs *)@,
+but @KindOf 2 ~ (KindParam :: KindIs Nat)@. -}
+type KindOf (a :: k) = (KindParam :: KindIs k)
 
 
 -- | (Kind) This is the kind of type-level natural numbers.
@@ -80,12 +83,6 @@ newtype instance Sing (n :: Nat)    = SNat Integer
 
 newtype instance Sing (n :: Symbol) = SSym String
 
-unsafeSingNat :: Integer -> Sing (n :: Nat)
-unsafeSingNat = SNat
-
-unsafeSingSymbol :: String -> Sing (n :: Symbol)
-unsafeSingSymbol = SSym
-
 --------------------------------------------------------------------------------
 
 -- | The class 'SingI' provides a \"smart\" constructor for singleton types.
@@ -97,6 +94,12 @@ class SingI a where
   -- | The only value of type @Sing a@
   sing :: Sing a
 
+-- | A convenience function to create a singleton value, when
+-- we have a proxy argument in scope.
+singByProxy :: SingI n => proxy n -> Sing n
+singByProxy _ = sing
+
+
 --------------------------------------------------------------------------------
 -- | Comparison of type-level naturals.
 class (m <=? n) ~ True => (m :: Nat) <= (n :: Nat)
@@ -129,16 +132,16 @@ and not their type---all types of a given kind are processed by the
 same instances.
 -}
 
-class (kparam ~ KindParam) => SingE (kparam :: OfKind k) where
+class (kparam ~ KindParam) => SingE (kparam :: KindIs k) where
   type DemoteRep kparam :: *
   fromSing :: Sing (a :: k) -> DemoteRep kparam
 
-instance SingE (KindParam :: OfKind Nat) where
-  type DemoteRep (KindParam :: OfKind Nat) = Integer
+instance SingE (KindParam :: KindIs Nat) where
+  type DemoteRep (KindParam :: KindIs Nat) = Integer
   fromSing (SNat n) = n
 
-instance SingE (KindParam :: OfKind Symbol) where
-  type DemoteRep (KindParam :: OfKind Symbol) = String
+instance SingE (KindParam :: KindIs Symbol) where
+  type DemoteRep (KindParam :: KindIs Symbol) = String
   fromSing (SSym s) = s
 
 {- | A convenient name for the type used to representing the values
@@ -153,6 +156,75 @@ class    (SingI a, SingE (KindOf a)) => SingRep (a :: k)
 instance (SingI a, SingE (KindOf a)) => SingRep (a :: k)
 
 
+-- The type of an unknown singletons of a given kind.
+-- Note that the "type" parameter on this type is really
+-- a *kind* parameter (this is simillar to the trick used in `SingE`).
+data SomeSing :: KindIs k -> * where
+  SomeSing :: SingI (n::k) => proxy n -> SomeSing (kp :: KindIs k)
+
+-- | A definition of natural numbers in terms of singletons.
+type SomeNat    = SomeSing (KindParam :: KindIs Nat)
+
+-- | A definition of strings in tterms of singletons.
+type SomeSymbol = SomeSing (KindParam :: KindIs Symbol)
+
+-- | The class of function that can promote a representation value
+-- into a singleton.  Like `SingE`, this class overloads based
+-- on a *kind*.
+-- The method returns `Maybe` because sometimes
+-- the representation type contains more values than are supported
+-- by the singletons.
+class (kp ~ KindParam) => ToSing (kp :: KindIs k) where
+  toSing :: DemoteRep kp -> Maybe (SomeSing kp)
+
+instance ToSing (KindParam :: KindIs Nat) where
+  toSing n
+    | n >= 0        = Just (incoherentForgetSing (SNat n))
+    | otherwise     = Nothing
+
+instance ToSing (KindParam :: KindIs Symbol) where
+  toSing n          = Just (incoherentForgetSing (SSym n))
+
+
+
+{- PRIVATE:
+WARNING: This function has the scary name because,
+in general, it could lead to incoherent behavior of the `sing` method.
+
+The reason is that it converts the provided `Sing n` value,
+into the the evidence for the `SingI` class hidden in `SomeSing`.
+
+Now, for proper singleton types this should not happen,
+because if there is only one value of type `Sing n`,
+then the parameter must be the same as the value of `sing`.
+However, we have no guarantees about the definition of `Sing a`,
+or, indeed, the instance of `Sing`.
+
+We use the function in the instances for `ToSing` for
+kind `Nat` and `Symbol`, where the use is guarantted to be safe.
+
+NOTE: The implementation is a bit of a hack at present,
+hence all the very special annotation.
+-}
+incoherentForgetSing :: forall (n :: k) (kp :: KindIs k). Sing n -> SomeSing kp
+incoherentForgetSing x = withSingI x it LocalProxy
+  where
+  it :: SingI n => LocalProxy n -> SomeSing kp
+  it = SomeSing
+
+{-# LANGUAGE NOINLINE withSingI #-}
+withSingI :: Sing n -> (SingI n => a) -> a
+withSingI x = magicSingI x ((\f -> f) :: () -> ())
+
+
+
+-- PRIVATE
+data LocalProxy n = LocalProxy
+
+
+
+
+
 {- | A convenience function useful when we need to name a singleton value
 multiple times.  Without this function, each use of 'sing' could potentially
 refer to a different singleton, and one has to use type signatures to
@@ -162,6 +234,7 @@ withSing :: SingI a => (Sing a -> b) -> b
 withSing f = f sing
 
 
+
 {- | A convenience function that names a singleton satisfying a certain
 property.  If the singleton does not satisfy the property, then the function
 returns 'Nothing'. The property is expressed in terms of the underlying
@@ -238,11 +311,6 @@ instance Show (a :~: b) where
 
 {- | Check if two type-natural singletons of potentially different types
 are indeed the same, by comparing their runtime representations.
-
-WARNING: in combination with `unsafeSingNat` this may lead to unsoundness:
-
-> eqSingNat (sing :: Sing 1) (unsafeSingNat 1 :: Sing 2)
-> == Just (Refl :: 1 :~: 2)
 -}
 
 eqSingNat :: Sing (m :: Nat) -> Sing (n :: Nat) -> Maybe (m :~: n)
@@ -253,8 +321,6 @@ eqSingNat x y
 
 {- | Check if two symbol singletons of potentially different types
 are indeed the same, by comparing their runtime representations.
-WARNING: in combination with `unsafeSingSymbol` this may lead to unsoundness
-(see `eqSingNat` for an example).
 -}
 
 eqSingSym:: Sing (m :: Symbol) -> Sing (n :: Symbol) -> Maybe (m :~: n)