{-# 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")