recover-rtti-0.1.0.0: Recover run-time type information from the GHC heap
Safe HaskellSafe-Inferred
LanguageHaskell2010

Debug.RecoverRTTI.Util.TypeLevel

Synopsis

Singletons

data family Sing :: k -> Type Source #

Instances

Instances details
Show (Sing c) Source # 
Instance details

Defined in Debug.RecoverRTTI.Constr

Methods

showsPrec :: Int -> Sing c -> ShowS #

show :: Sing c -> String #

showList :: [Sing c] -> ShowS #

data Sing (a :: Type) Source # 
Instance details

Defined in Debug.RecoverRTTI.Util.TypeLevel

data Sing (a :: Type) where
data Sing (n :: Symbol) Source # 
Instance details

Defined in Debug.RecoverRTTI.Util.TypeLevel

data Sing (n :: Symbol) where
data Sing (n :: Nat) Source # 
Instance details

Defined in Debug.RecoverRTTI.Util.TypeLevel

data Sing (n :: Nat) where
data Sing (xs :: [k]) Source # 
Instance details

Defined in Debug.RecoverRTTI.Util.TypeLevel

data Sing (xs :: [k]) where
  • SN :: forall k. Sing ('[] :: [k])
  • SC :: forall a (x :: a) (xs :: [a]). Sing x -> Sing xs -> Sing (x ': xs)
data Sing (c :: Constr Symbol) Source # 
Instance details

Defined in Debug.RecoverRTTI.Constr

data Sing (c :: Constr Symbol) where

class SingI (a :: k) where Source #

Methods

sing :: Sing a Source #

Instances

Instances details
SingI (a :: Type) Source # 
Instance details

Defined in Debug.RecoverRTTI.Util.TypeLevel

Methods

sing :: Sing a Source #

KnownSymbol n => SingI (n :: Symbol) Source # 
Instance details

Defined in Debug.RecoverRTTI.Util.TypeLevel

Methods

sing :: Sing n Source #

SingI 'Z Source # 
Instance details

Defined in Debug.RecoverRTTI.Util.TypeLevel

Methods

sing :: Sing 'Z Source #

SingI n => SingI ('S n :: Nat) Source # 
Instance details

Defined in Debug.RecoverRTTI.Util.TypeLevel

Methods

sing :: Sing ('S n) Source #

KnownConstr c => SingI (c :: Constr Symbol) Source # 
Instance details

Defined in Debug.RecoverRTTI.Constr

Methods

sing :: Sing c Source #

SingI ('[] :: [k]) Source # 
Instance details

Defined in Debug.RecoverRTTI.Util.TypeLevel

Methods

sing :: Sing '[] Source #

(SingI x, SingI xs) => SingI (x ': xs :: [a]) Source # 
Instance details

Defined in Debug.RecoverRTTI.Util.TypeLevel

Methods

sing :: Sing (x ': xs) Source #

class DecidableEquality k where Source #

Methods

decideEquality :: Sing (a :: k) -> Sing (b :: k) -> Maybe (a :~: b) Source #

Instances

Instances details
DecidableEquality Symbol Source # 
Instance details

Defined in Debug.RecoverRTTI.Util.TypeLevel

Methods

decideEquality :: forall (a :: Symbol) (b :: Symbol). Sing a -> Sing b -> Maybe (a :~: b) Source #

DecidableEquality (Constr Symbol) Source # 
Instance details

Defined in Debug.RecoverRTTI.Constr

Methods

decideEquality :: forall (a :: Constr Symbol) (b :: Constr Symbol). Sing a -> Sing b -> Maybe (a :~: b) Source #

Natural numbers

data Nat Source #

Constructors

Z 
S Nat 

Instances

Instances details
SingI 'Z Source # 
Instance details

Defined in Debug.RecoverRTTI.Util.TypeLevel

Methods

sing :: Sing 'Z Source #

SingI n => SingI ('S n :: Nat) Source # 
Instance details

Defined in Debug.RecoverRTTI.Util.TypeLevel

Methods

sing :: Sing ('S n) Source #

data Sing (n :: Nat) Source # 
Instance details

Defined in Debug.RecoverRTTI.Util.TypeLevel

data Sing (n :: Nat) where

knownNat :: Sing (n :: Nat) -> Int Source #

type family Length (xs :: [k]) :: Nat where ... Source #

Equations

Length '[] = 'Z 
Length (_ ': xs) = 'S (Length xs) 

General purpose type level functions

type family Or (a :: Bool) (b :: Bool) where ... Source #

Equations

Or 'True b = 'True 
Or a 'True = 'True 
Or _ _ = 'False 

type family Equal (x :: k) (y :: k) where ... Source #

Equations

Equal x x = 'True 
Equal x y = 'False 

type family Elem (x :: k) (xs :: [k]) where ... Source #

Equations

Elem x '[] = 'False 
Elem x (y ': ys) = Or (Equal x y) (Elem x ys) 

type family Assert (b :: Bool) (err :: ErrorMessage) :: Constraint where ... Source #

Assert type-level predicate

We cannot define this in terms of a more general If construct, because ghc's type-level language has an undefined reduction order and so we get no short-circuiting.

Equations

Assert 'True err = () 
Assert 'False err = TypeError err 

Type-level membership check

data IsElem (x :: k) (xs :: [k]) where Source #

Constructors

IsElem :: Elem x xs ~ 'True => IsElem x xs 

checkIsElem :: DecidableEquality k => Sing (x :: k) -> Sing (xs :: [k]) -> Maybe (IsElem x xs) Source #

Phantom type parameters

class Phantom (f :: k -> Type) where Source #

Functors with phantom arguments

Methods

phantom :: forall a b. f a -> f b Source #

Similar to phantom, but without requiring Functor or Contravariant

data Poly (f :: k -> Type) Source #

Constructors

Poly (forall (a :: k). f a) 

maybePoly :: Phantom f => Maybe (f a) -> Maybe (Poly f) Source #

Commute Maybe and forall