{-# LANGUAGE RankNTypes, TypeFamilies, FlexibleInstances,
             GADTs, UndecidableInstances, ScopedTypeVariables,
             MagicHash, TypeOperators, PolyKinds, TypeApplications,
             StandaloneKindSignatures #-}
{-# 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 = 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 = 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 t
tra %== :: forall (t :: TYPE rep) (t :: TYPE rep).
Sing t -> Sing t -> Sing (Apply (Apply (==@#@$) t) t)
%== Sing t
trb =
    case TypeRep t -> TypeRep t -> Maybe (t :~~: t)
forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
eqTypeRep TypeRep t
Sing t
tra TypeRep t
Sing t
trb of
      Just t :~~: t
HRefl -> Sing (Apply (Apply (==@#@$) t) t)
SBool 'True
STrue
      Maybe (t :~~: t)
Nothing    -> SBool 'False -> SBool (DefaultEq t t)
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 :~: 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")