    {-# LANGUAGE RankNTypes, TypeFamilies, FlexibleInstances,
                 GADTs, UndecidableInstances, ScopedTypeVariables,
                 MagicHash, TypeOperators, PolyKinds, TypeApplications #-}
    {-# 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,
      -- | 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.Kind (Type)
    import Data.Singletons.Prelude.Instances
    import Data.Singletons.Internal
    import Data.Singletons.Prelude.Eq
    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@).
    data SomeTypeRepTYPE :: RuntimeRep -> Type where
      SomeTypeRepTYPE :: forall (rep :: RuntimeRep) (a :: TYPE rep). !(TypeRep a) -> SomeTypeRepTYPE rep

    instance Eq (SomeTypeRepTYPE rep) where
      SomeTypeRepTYPE a :: TypeRep a
    a == :: SomeTypeRepTYPE rep -> SomeTypeRepTYPE rep -> Bool
    == SomeTypeRepTYPE b :: 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 HRefl -> Bool
    True
          Nothing    -> Bool
    False

    instance Ord (SomeTypeRepTYPE rep) where
      SomeTypeRepTYPE a :: TypeRep a
    a compare :: SomeTypeRepTYPE rep -> SomeTypeRepTYPE rep -> Ordering
    `compare` SomeTypeRepTYPE b :: 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 p :: Int
    p (SomeTypeRepTYPE ty :: 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 :: 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 tr) = Sing a -> SomeSing (TYPE rep)
    forall k (a :: k). Sing a -> SomeSing k
    SomeSing TypeRep a
    Sing a
    tr

    instance PEq (TYPE rep)
    instance SEq (TYPE rep) where
      tra :: Sing a
    tra %== :: Sing a -> Sing b -> Sing (a == b)
    %== trb :: 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 HRefl -> Sing (a == b)
    SBool 'True
    STrue
          Nothing    -> SBool 'False -> SBool (DefaultEq a b)
    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
      tra :: Sing a
    tra %~ :: Sing a -> Sing b -> Decision (a :~: b)
    %~ trb :: 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 HRefl -> (a :~: a) -> Decision (a :~: a)
    forall a. a -> Decision a
    Proved a :~: a
    forall k (a :: k). a :~: a
    Refl
          Nothing    -> Refuted (a :~: b) -> Decision (a :~: b)
    forall a. Refuted a -> Decision a
    Disproved (\Refl -> String -> Void
    forall a. HasCallStack => String -> a
    error "Type.Reflection.eqTypeRep failed")