    {-# LANGUAGE RankNTypes, TypeFamilies, FlexibleInstances,
                 GADTs, UndecidableInstances, ScopedTypeVariables,
                 MagicHash, TypeOperators, PolyKinds #-}
    {-# OPTIONS_GHC -Wno-orphans #-}

    -----------------------------------------------------------------------------
    -- |
    -- Module      :  Data.Singletons.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.TypeRepTYPE (
      Sing(STypeRep),
      -- | Here is the definition of the singleton for @'TYPE' rep@:
      --
      -- > newtype instance Sing :: forall (rep :: RuntimeRep). TYPE rep -> Type where
      -- >   STypeRep :: forall (rep :: RuntimeRep) (a :: TYPE rep). TypeRep a -> Sing a
      --
      -- Instances for 'SingI', 'SingKind', 'SEq', 'SDecide', and
      -- 'TestCoercion' are also supplied.

      SomeTypeRepTYPE(..)
      ) where

    import Data.Kind (Type)
    import Data.Singletons.Prelude.Instances
    import Data.Singletons.Internal
    import Data.Singletons.Prelude.Eq
    import Data.Singletons.Decide
    import Data.Type.Equality ((:~:)(..))
    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 -> Type` 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.
    newtype instance Sing :: forall (rep :: RuntimeRep). TYPE rep -> Type where
      STypeRep :: forall (rep :: RuntimeRep) (a :: TYPE rep). TypeRep a -> Sing a
        deriving (Eq, Ord, Show)

    -- | A variant of 'SomeTypeRep' whose underlying 'TypeRep' is restricted to
    -- kind @'TYPE' rep@ (for some 'RuntimeRep' @rep@).
    data SomeTypeRepTYPE :: RuntimeRep -> Type where
      SomeTypeRepTYPE :: forall (rep :: RuntimeRep) (a :: TYPE rep). !(TypeRep a) -> SomeTypeRepTYPE rep

    instance Eq (SomeTypeRepTYPE rep) where
      SomeTypeRepTYPE a == SomeTypeRepTYPE b =
        case eqTypeRep a b of
          Just HRefl -> True
          Nothing    -> False

    instance Ord (SomeTypeRepTYPE rep) where
      SomeTypeRepTYPE a `compare` SomeTypeRepTYPE b =
        typeRepFingerprint a `compare` typeRepFingerprint b

    instance Show (SomeTypeRepTYPE rep) where
      showsPrec p (SomeTypeRepTYPE ty) = showsPrec p ty

    instance Typeable a => SingI (a :: TYPE rep) where
      sing = STypeRep typeRep
    instance SingKind (TYPE rep) where
      type Demote (TYPE rep) = SomeTypeRepTYPE rep
      fromSing (STypeRep tr) = SomeTypeRepTYPE tr
      toSing (SomeTypeRepTYPE tr) = SomeSing $ STypeRep tr

    instance PEq (TYPE rep)
    instance SEq (TYPE rep) where
      STypeRep tra %== STypeRep trb =
        case eqTypeRep tra trb of
          Just HRefl -> STrue
          Nothing    -> unsafeCoerce SFalse
                        -- the Data.Typeable interface isn't strong enough
                        -- to enable us to define this without unsafeCoerce

    instance SDecide (TYPE rep) where
      STypeRep tra %~ STypeRep trb =
        case eqTypeRep tra trb of
          Just HRefl -> Proved Refl
          Nothing    -> Disproved (\Refl -> error "Type.Reflection.eqTypeRep failed")