Add code to convert from representation types, to existentially quantified singletons.

The basic idea is like this:

data SomeSing where SomeSing :: SingI n => Proxy n -> SomeSing

toSing :: Integer -> Maybe SomeSing  -- Maybe, so that we rejetc -ve numbers

The actual implementation is a bit more complicated because `SomeSing`
is actually parameterized by a kind, so we really have something akin
`SomeSing k`.  Also, `toSing` is a bit more general because, depending
on the kind, the representation is different.  For example, we also
support:

toSing :: String -> Maybe (SomeSing (KindParam :: KindIs Symbol))


This change relies on the primitive added to the compiler, which
converts `Sing` values into `SingI` dictionaries.

A nice benefit of this change is that, as far as I can see,
we don't need  `unsafeSinNat` and friends, so I removed them.

1 files changed, 94 insertions, 26 deletions

diff --git a/libraries/base/GHC/TypeLits.hs b/libraries/base/GHC/TypeLits.hs
index f8b759efd4..56b0481e91 100644
--- a/libraries/base/GHC/TypeLits.hs
+++ b/libraries/base/GHC/TypeLits.hs
@@ -9,6 +9,7 @@
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE MultiParamTypeClasses #-}  -- for <=
+{-# LANGUAGE RankNTypes #-}             -- 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 +20,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 +44,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, asTypeOf)
 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 +82,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 +93,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 +131,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 +155,78 @@ 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 = seq x (magic1 SomeSing (LocalProxy :: LocalProxy n))
+  where
+  -- The signature ensures that we instantiate things in the right order
+  magic1 :: (SingI n => LocalProxy n -> SomeSing kp) -> LocalProxy n -> SomeSing kp
+  magic1 = magic
+
+  -- For a description of the `magicSingI` stuff in this
+  -- take a look at Note [magicSingI magic] in MkId in GHC's source.
+  -- The NOINLINE and the type signature ensure that the
+  -- definitional rule fires.
+  {-# NOINLINE magic #-}
+  magic :: (SingI n => b) -> b
+  magic = magicSingI x (\f -> f `asTypeOf` ())
+
+-- 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 +236,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 +313,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 +323,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)