{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}

-----------------------------------------------------------------------------

-- |

-- Module      :  Data.Singletons.Base.TypeRepTYPE

-- Copyright   :  (C) 2013 Richard Eisenberg

-- License     :  BSD-style (see LICENSE)

-- Maintainer  :  Ryan Scott

-- Stability   :  experimental

-- Portability :  non-portable

--

-- This module defines singleton instances making 'TypeRep' the singleton for

-- the kind @'TYPE' rep@ (for some 'RuntimeRep' @rep@), an instantiation of

-- which is the famous kind 'Type'. The definitions don't fully line up with

-- what is expected within the singletons library, so expect unusual results!

--

----------------------------------------------------------------------------


module Data.Singletons.Base.TypeRepTYPE (
  Sing,
  -- | Here is the definition of the singleton for @'TYPE' rep@:

  --

  -- > type instance Sing \@(TYPE rep) = TypeRep

  --

  -- Instances for 'SingI', 'SingKind', 'SEq', 'SDecide', and

  -- 'TestCoercion' are also supplied.


  SomeTypeRepTYPE(..)
  ) where

import Data.Eq.Singletons
import Data.Kind (Type)
import Data.Singletons
import Data.Singletons.Base.Instances
import Data.Singletons.Decide
import GHC.Exts (RuntimeRep, TYPE)
import Type.Reflection
import Type.Reflection.Unsafe
import Unsafe.Coerce

-- | A choice of singleton for the kind @'TYPE' rep@ (for some 'RuntimeRep'

-- @rep@), an instantiation of which is the famous kind 'Type'.

--

-- Conceivably, one could generalize this instance to `Sing \@k` for

-- /any/ kind @k@, and remove all other 'Sing' instances. We don't adopt this

-- design, however, since it is far more convenient in practice to work with

-- explicit singleton values than 'TypeRep's (for instance, 'TypeRep's are

-- more difficult to pattern match on, and require extra runtime checks).

--

-- We cannot produce explicit singleton values for everything in @'TYPE' rep@,

-- however, since it is an open kind, so we reach for 'TypeRep' in this one

-- particular case.

type instance Sing @(TYPE rep) = TypeRep

-- | A variant of 'SomeTypeRep' whose underlying 'TypeRep' is restricted to

-- kind @'TYPE' rep@ (for some 'RuntimeRep' @rep@).

type SomeTypeRepTYPE :: RuntimeRep -> Type
data SomeTypeRepTYPE :: RuntimeRep -> Type where
  SomeTypeRepTYPE :: forall (rep :: RuntimeRep) (a :: TYPE rep). !(TypeRep a) -> SomeTypeRepTYPE rep

instance Eq (SomeTypeRepTYPE rep) where
  SomeTypeRepTYPE TypeRep a
a == :: SomeTypeRepTYPE rep -> SomeTypeRepTYPE rep -> Bool
== SomeTypeRepTYPE TypeRep a
b =
    case TypeRep a -> TypeRep a -> Maybe (a :~~: a)
forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
eqTypeRep TypeRep a
a TypeRep a
b of
      Just a :~~: a
HRefl -> Bool
True
      Maybe (a :~~: a)
Nothing    -> Bool
False

instance Ord (SomeTypeRepTYPE rep) where
  SomeTypeRepTYPE TypeRep a
a compare :: SomeTypeRepTYPE rep -> SomeTypeRepTYPE rep -> Ordering
`compare` SomeTypeRepTYPE TypeRep a
b =
    TypeRep a -> Fingerprint
forall {k} (a :: k). TypeRep a -> Fingerprint
typeRepFingerprint TypeRep a
a Fingerprint -> Fingerprint -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` TypeRep a -> Fingerprint
forall {k} (a :: k). TypeRep a -> Fingerprint
typeRepFingerprint TypeRep a
b

instance Show (SomeTypeRepTYPE rep) where
  showsPrec :: Int -> SomeTypeRepTYPE rep -> ShowS
showsPrec Int
p (SomeTypeRepTYPE TypeRep a
ty) = Int -> TypeRep a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
p TypeRep a
ty

instance Typeable a => SingI (a :: TYPE rep) where
  sing :: Sing a
sing = TypeRep a
Sing a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep
instance SingKind (TYPE rep) where
  type Demote (TYPE rep) = SomeTypeRepTYPE rep
  fromSing :: forall (a :: TYPE rep). Sing a -> Demote (TYPE rep)
fromSing = TypeRep a -> SomeTypeRepTYPE rep
Sing a -> Demote (TYPE rep)
forall a. TypeRep a -> SomeTypeRepTYPE LiftedRep
SomeTypeRepTYPE
  toSing :: Demote (TYPE rep) -> SomeSing (TYPE rep)
toSing (SomeTypeRepTYPE TypeRep a
tr) = Sing a -> SomeSing (TYPE rep)
forall k (a :: k). Sing a -> SomeSing k
SomeSing TypeRep a
Sing a
tr

instance PEq (TYPE rep) where
  type x == y = DefaultEq x y
instance SEq (TYPE rep) where
  Sing t1
tra %== :: forall (t1 :: TYPE rep) (t2 :: TYPE rep).
Sing t1 -> Sing t2 -> Sing (Apply (Apply (==@#@$) t1) t2)
%== Sing t2
trb =
    case TypeRep t1 -> TypeRep t2 -> Maybe (t1 :~~: t2)
forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
eqTypeRep TypeRep t1
Sing t1
tra TypeRep t2
Sing t2
trb of
      Just t1 :~~: t2
HRefl -> Sing (Apply (Apply (==@#@$) t1) t2)
SBool 'True
STrue
      Maybe (t1 :~~: t2)
Nothing    -> SBool 'False -> SBool (DefaultEq t1 t2)
forall a b. a -> b
unsafeCoerce SBool 'False
SFalse
                    -- the Data.Typeable interface isn't strong enough

                    -- to enable us to define this without unsafeCoerce


instance SDecide (TYPE rep) where
  Sing a
tra %~ :: forall (a :: TYPE rep) (b :: TYPE rep).
Sing a -> Sing b -> Decision (a :~: b)
%~ Sing b
trb =
    case TypeRep a -> TypeRep b -> Maybe (a :~~: b)
forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
eqTypeRep TypeRep a
Sing a
tra TypeRep b
Sing b
trb of
      Just a :~~: b
HRefl -> (a :~: b) -> Decision (a :~: b)
forall a. a -> Decision a
Proved a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
      Maybe (a :~~: b)
Nothing    -> Refuted (a :~: b) -> Decision (a :~: b)
forall a. Refuted a -> Decision a
Disproved (\a :~: b
Refl -> String -> Void
forall a. HasCallStack => String -> a
error String
"Type.Reflection.eqTypeRep failed")