Commit 5d608279 authored by Simon Peyton Jones's avatar Simon Peyton Jones

Merge branch 'master' of http://darcs.haskell.org/packages/base

parents e1779a71 875beafa
......@@ -29,10 +29,14 @@ module GHC.TypeLits
, type (<=), type (<=?), type (+), type (*), type (^)
, type (-)
-- * Comparing for equality
, type (:~:) (..), eqSingNat, eqSingSym
-- * Destructing type-nat singletons.
, isZero, IsZero(..)
, isEven, IsEven(..)
-- * Matching on type-nats
, Nat1(..), FromNat1
......@@ -215,4 +219,40 @@ type family FromNat1 (n :: Nat1) :: Nat
type instance FromNat1 Zero = 0
type instance FromNat1 (Succ n) = 1 + FromNat1 n
--------------------------------------------------------------------------------
-- | A type that provides evidence for equality between two types.
data (:~:) :: k -> k -> * where
Refl :: a :~: a
instance Show (a :~: b) where
show Refl = "Refl"
{- | 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 unsoudness:
> eqSingNat (sing :: Sing 1) (unsafeSingNat 1 :: Sing 2)
> == Just (Refl :: 1 :~: 2)
-}
eqSingNat :: Sing (m :: Nat) -> Sing (n :: Nat) -> Maybe (m :~: n)
eqSingNat x y
| fromSing x == fromSing y = Just (unsafeCoerce Refl)
| otherwise = Nothing
{- | 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 unsoudness
(see `eqSingNat` for an example).
-}
eqSingSym:: Sing (m :: Symbol) -> Sing (n :: Symbol) -> Maybe (m :~: n)
eqSingSym x y
| fromSing x == fromSing y = Just (unsafeCoerce Refl)
| otherwise = Nothing
......@@ -2,7 +2,6 @@
import Control.Concurrent
import Control.Exception
import Control.Monad
import Control.Concurrent.STM
new = newQSemN
wait = waitQSemN
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment