{-# 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 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 = typeRep
instance SingKind (TYPE rep) where
  type Demote (TYPE rep) = SomeTypeRepTYPE rep
  fromSing = SomeTypeRepTYPE
  toSing (SomeTypeRepTYPE tr) = SomeSing tr

instance PEq (TYPE rep) where
  type x == y = DefaultEq x y
instance SEq (TYPE rep) where
  tra %== 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
  tra %~ trb =
    case eqTypeRep tra trb of
      Just HRefl -> Proved Refl
      Nothing    -> Disproved (\Refl -> error "Type.Reflection.eqTypeRep failed")