-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/
-- | Basic singleton types and definitions
--
-- singletons contains the basic types and definitions needed to
-- support dependently typed programming techniques in Haskell. This
-- library was originally presented in Dependently Typed Programming
-- with Singletons, published at the Haskell Symposium, 2012.
-- (https://richarde.dev/papers/2012/singletons/paper.pdf)
--
-- singletons is intended to be a small, foundational library on
-- which other projects can build. As such, singletons has a
-- minimal dependency footprint and supports GHCs dating back to GHC 8.0.
-- For more information, consult the singletons
-- README.
--
-- You may also be interested in the following related libraries:
--
--
-- - The singletons-th library defines Template Haskell
-- functionality that allows promotion of term-level functions to
-- type-level equivalents and singling functions to dependently
-- typed equivalents.
-- - The singletons-base library uses singletons-th
-- to define promoted and singled functions from the base
-- library, including the Prelude.
--
@package singletons
@version 3.0.2
-- | This module exports the basic definitions to use singletons. See also
-- Prelude.Singletons from the singletons-base library,
-- which re-exports this module alongside many singled definitions based
-- on the Prelude.
--
-- You may also want to read the original papers presenting this library,
-- available at
-- https://richarde.dev/papers/2012/singletons/paper.pdf and
-- https://richarde.dev/papers/2014/promotion/promotion.pdf.
module Data.Singletons
-- | The singleton kind-indexed type family.
type family Sing :: k -> Type
newtype SLambda (f :: k1 ~> k2)
SLambda :: (forall t. Sing t -> Sing (f @@ t)) -> SLambda (f :: k1 ~> k2)
[applySing] :: SLambda (f :: k1 ~> k2) -> forall t. Sing t -> Sing (f @@ t)
-- | An infix synonym for applySing
(@@) :: forall k1 k2 (f :: k1 ~> k2) (t :: k1). Sing f -> Sing t -> Sing (f @@ t)
infixl 9 @@
-- | A SingI constraint is essentially an implicitly-passed
-- singleton. If you need to satisfy this constraint with an explicit
-- singleton, please see withSingI or the Sing pattern
-- synonym.
class SingI a
-- | Produce the singleton explicitly. You will likely need the
-- ScopedTypeVariables extension to use this method the way you
-- want.
sing :: SingI a => Sing a
-- | A version of the SingI class lifted to unary type constructors.
class (forall x. SingI x => SingI (f x)) => SingI1 f
-- | Lift an explicit singleton through a unary type constructor. You will
-- likely need the ScopedTypeVariables extension to use this
-- method the way you want.
liftSing :: SingI1 f => Sing x -> Sing (f x)
-- | Produce a singleton explicitly using implicit SingI1 and
-- SingI constraints. You will likely need the
-- ScopedTypeVariables extension to use this method the way you
-- want.
sing1 :: (SingI1 f, SingI x) => Sing (f x)
-- | A version of the SingI class lifted to binary type
-- constructors.
class (forall x y. (SingI x, SingI y) => SingI (f x y)) => SingI2 f
-- | Lift explicit singletons through a binary type constructor. You will
-- likely need the ScopedTypeVariables extension to use this
-- method the way you want.
liftSing2 :: SingI2 f => Sing x -> Sing y -> Sing (f x y)
-- | Produce a singleton explicitly using implicit SingI2 and
-- SingI constraints. You will likely need the
-- ScopedTypeVariables extension to use this method the way you
-- want.
sing2 :: (SingI2 f, SingI x, SingI y) => Sing (f x y)
-- | The SingKind class is a kind class. It classifies all
-- kinds for which singletons are defined. The class supports converting
-- between a singleton type and the base (unrefined) type which it is
-- built from.
--
-- For a SingKind instance to be well behaved, it should obey the
-- following laws:
--
--
-- toSing . fromSing ≡ SomeSing
-- (\x -> withSomeSing x fromSing) ≡ id
--
--
-- The final law can also be expressed in terms of the FromSing
-- pattern synonym:
--
--
-- (\(FromSing sing) -> FromSing sing) ≡ id
--
class SingKind k where {
-- | Get a base type from the promoted kind. For example, Demote
-- Bool will be the type Bool. Rarely, the type and kind do
-- not match. For example, Demote Nat is Natural.
type family Demote k = (r :: Type) | r -> k;
}
-- | Convert a singleton to its unrefined version.
fromSing :: SingKind k => Sing (a :: k) -> Demote k
-- | Convert an unrefined type to an existentially-quantified singleton
-- type.
toSing :: SingKind k => Demote k -> SomeSing k
-- | Convenient synonym to refer to the kind of a type variable: type
-- KindOf (a :: k) = k
type KindOf (a :: k) = k
-- | Force GHC to unify the kinds of a and b. Note that
-- SameKind a b is different from KindOf a ~ KindOf b
-- in that the former makes the kinds unify immediately, whereas the
-- latter is a proposition that GHC considers as possibly false.
type SameKind (a :: k) (b :: k) = (() :: Constraint)
-- | A SingInstance wraps up a SingI instance for explicit
-- handling.
data SingInstance (a :: k)
[SingInstance] :: SingI a => SingInstance a
-- | An existentially-quantified singleton. This type is useful when
-- you want a singleton type, but there is no way of knowing, at
-- compile-time, what the type index will be. To make use of this type,
-- you will generally have to use a pattern-match:
--
--
-- foo :: Bool -> ...
-- foo b = case toSing b of
-- SomeSing sb -> {- fancy dependently-typed code with sb -}
--
--
-- An example like the one above may be easier to write using
-- withSomeSing.
data SomeSing k
[SomeSing] :: Sing (a :: k) -> SomeSing k
-- | Get an implicit singleton (a SingI instance) from an explicit
-- one.
singInstance :: forall k (a :: k). Sing a -> SingInstance a
-- | An explicitly bidirectional pattern synonym for implicit singletons.
--
-- As an expression: Constructs a singleton Sing a given
-- a implicit singleton constraint SingI a.
--
-- As a pattern: Matches on an explicit Sing a witness
-- bringing an implicit SingI a constraint into scope.
pattern Sing :: forall k (a :: k). () => SingI a => Sing a
-- | Convenience function for creating a context with an implicit singleton
-- available.
withSingI :: Sing n -> (SingI n => r) -> r
-- | Convert a normal datatype (like Bool) to a singleton for that
-- datatype, passing it into a continuation.
withSomeSing :: forall k r. SingKind k => Demote k -> (forall (a :: k). Sing a -> r) -> r
-- | An explicitly bidirectional pattern synonym for going between a
-- singleton and the corresponding demoted term.
--
-- As an expression: this takes a singleton to its demoted (base)
-- type.
--
--
-- >>> :t FromSing \@Bool
-- FromSing \@Bool :: Sing a -> Bool
--
-- >>> FromSing SFalse
-- False
--
--
-- As a pattern: It extracts a singleton from its demoted (base)
-- type.
--
--
-- singAnd :: Bool -> Bool -> SomeSing Bool
-- singAnd (FromSing singBool1) (FromSing singBool2) =
-- SomeSing (singBool1 %&& singBool2)
--
--
-- instead of writing it with withSomeSing:
--
--
-- singAnd bool1 bool2 =
-- withSomeSing bool1 $ singBool1 ->
-- withSomeSing bool2 $ singBool2 ->
-- SomeSing (singBool1 %&& singBool2)
--
pattern FromSing :: SingKind k => forall (a :: k). Sing a -> Demote k
-- | Convert a group of SingI1 and SingI constraints
-- (representing a function to apply and its argument, respectively) into
-- a single SingI constraint representing the application. You
-- will likely need the ScopedTypeVariables extension to use
-- this method the way you want.
usingSingI1 :: forall f x r. (SingI1 f, SingI x) => (SingI (f x) => r) -> r
-- | Convert a group of SingI2 and SingI constraints
-- (representing a function to apply and its arguments, respectively)
-- into a single SingI constraint representing the application.
-- You will likely need the ScopedTypeVariables extension to use
-- this method the way you want.
usingSingI2 :: forall f x y r. (SingI2 f, SingI x, SingI y) => (SingI (f x y) => r) -> r
-- | Allows creation of a singleton when a proxy is at hand.
singByProxy :: SingI a => proxy a -> Sing a
-- | Allows creation of a singleton for a unary type constructor when a
-- proxy is at hand.
singByProxy1 :: (SingI1 f, SingI x) => proxy (f x) -> Sing (f x)
-- | Allows creation of a singleton for a binary type constructor when a
-- proxy is at hand.
singByProxy2 :: (SingI2 f, SingI x, SingI y) => proxy (f x y) -> Sing (f x y)
-- | A convenience function that takes a type as input and demotes it to
-- its value-level counterpart as output. This uses SingKind and
-- SingI behind the scenes, so demote = fromSing
-- sing.
--
-- This function is intended to be used with TypeApplications.
-- For example:
--
--
-- >>> demote @True
-- True
--
--
--
-- >>> demote @(Nothing :: Maybe Ordering)
-- Nothing
--
--
--
-- >>> demote @(Just EQ)
-- Just EQ
--
--
--
-- >>> demote @'(True,EQ)
-- (True,EQ)
--
demote :: forall a. (SingKind (KindOf a), SingI a) => Demote (KindOf a)
-- | A convenience function that takes a unary type constructor and its
-- argument as input, applies them, and demotes the result to its
-- value-level counterpart as output. This uses SingKind,
-- SingI1, and SingI behind the scenes, so
-- demote1 = fromSing sing1.
--
-- This function is intended to be used with TypeApplications.
-- For example:
--
--
-- >>> demote1 @Just @EQ
-- Just EQ
--
--
--
-- >>> demote1 @('(,) True) @EQ
-- (True,EQ)
--
demote1 :: forall f x. (SingKind (KindOf (f x)), SingI1 f, SingI x) => Demote (KindOf (f x))
-- | A convenience function that takes a binary type constructor and its
-- arguments as input, applies them, and demotes the result to its
-- value-level counterpart as output. This uses SingKind,
-- SingI2, and SingI behind the scenes, so
-- demote2 = fromSing sing2.
--
-- This function is intended to be used with TypeApplications.
-- For example:
--
--
-- >>> demote2 @'(,) @True @EQ
-- (True,EQ)
--
demote2 :: forall f x y. (SingKind (KindOf (f x y)), SingI2 f, SingI x, SingI y) => Demote (KindOf (f x y))
-- | Allows creation of a singleton when a proxy# is at hand.
singByProxy# :: SingI a => Proxy# a -> Sing a
-- | Allows creation of a singleton for a unary type constructor when a
-- proxy# is at hand.
singByProxy1# :: (SingI1 f, SingI x) => Proxy# (f x) -> Sing (f x)
-- | Allows creation of a singleton for a binary type constructor when a
-- proxy# is at hand.
singByProxy2# :: (SingI2 f, SingI x, SingI y) => Proxy# (f x y) -> Sing (f x y)
-- | A convenience function useful when we need to name a singleton value
-- multiple times. Without this function, each use of sing could
-- potentially refer to a different singleton, and one has to use type
-- signatures (often with ScopedTypeVariables) to ensure that
-- they are the same.
withSing :: SingI a => (Sing a -> b) -> b
-- | A convenience function useful when we need to name a singleton value
-- for a unary type constructor multiple times. Without this function,
-- each use of sing1 could potentially refer to a different
-- singleton, and one has to use type signatures (often with
-- ScopedTypeVariables) to ensure that they are the same.
withSing1 :: (SingI1 f, SingI x) => (Sing (f x) -> b) -> b
-- | A convenience function useful when we need to name a singleton value
-- for a binary type constructor multiple times. Without this function,
-- each use of sing1 could potentially refer to a different
-- singleton, and one has to use type signatures (often with
-- ScopedTypeVariables) to ensure that they are the same.
withSing2 :: (SingI2 f, SingI x, SingI y) => (Sing (f x y) -> b) -> b
-- | A convenience function that names a singleton satisfying a certain
-- property. If the singleton does not satisfy the property, then the
-- function returns Nothing. The property is expressed in terms of
-- the underlying representation of the singleton.
singThat :: forall k (a :: k). (SingKind k, SingI a) => (Demote k -> Bool) -> Maybe (Sing a)
-- | A convenience function that names a singleton for a unary type
-- constructor satisfying a certain property. If the singleton does not
-- satisfy the property, then the function returns Nothing. The
-- property is expressed in terms of the underlying representation of the
-- singleton.
singThat1 :: forall k1 k2 (f :: k1 -> k2) (x :: k1). (SingKind k2, SingI1 f, SingI x) => (Demote k2 -> Bool) -> Maybe (Sing (f x))
-- | A convenience function that names a singleton for a binary type
-- constructor satisfying a certain property. If the singleton does not
-- satisfy the property, then the function returns Nothing. The
-- property is expressed in terms of the underlying representation of the
-- singleton.
singThat2 :: forall k1 k2 k3 (f :: k1 -> k2 -> k3) (x :: k1) (y :: k2). (SingKind k3, SingI2 f, SingI x, SingI y) => (Demote k3 -> Bool) -> Maybe (Sing (f x y))
-- | A newtype around Sing.
--
-- Since Sing is a type family, it cannot be used directly in type
-- class instances. As one example, one cannot write a catch-all
-- instance SDecide k => TestEquality
-- (Sing k). On the other hand, WrappedSing is a
-- perfectly ordinary data type, which means that it is quite possible to
-- define an instance SDecide k => TestEquality
-- (WrappedSing k).
newtype WrappedSing :: forall k. k -> Type
[WrapSing] :: forall k (a :: k). {unwrapSing :: Sing a} -> WrappedSing a
-- | The singleton for WrappedSings. Informally, this is the
-- singleton type for other singletons.
newtype SWrappedSing :: forall k (a :: k). WrappedSing a -> Type
[SWrapSing] :: forall k (a :: k) (ws :: WrappedSing a). {sUnwrapSing :: Sing a} -> SWrappedSing ws
type family UnwrapSing (ws :: WrappedSing (a :: k)) :: Sing a
-- | Representation of the kind of a type-level function. The difference
-- between term-level arrows and this type-level arrow is that at the
-- term level applications can be unsaturated, whereas at the type level
-- all applications have to be fully saturated.
data TyFun :: Type -> Type -> Type
-- | Something of kind a ~> b is a defunctionalized type
-- function that is not necessarily generative or injective.
-- Defunctionalized type functions (also called "defunctionalization
-- symbols") can be partially applied, even if the original type function
-- cannot be. For more information on how this works, see the "Promotion
-- and partial application" section of the README.
--
-- Normal type-level arrows (->) can be converted into
-- defunctionalization arrows (~>) by the use of the
-- TyCon family of types. (Refer to the Haddocks for TyCon1
-- to see an example of this in practice.) For this reason, we do not
-- make an effort to define defunctionalization symbols for most type
-- constructors of kind a -> b, as they can be used in
-- defunctionalized settings by simply applying TyCon{N} with an
-- appropriate N.
--
-- This includes the (->) type constructor itself, which is
-- of kind Type -> Type -> Type. One
-- can turn it into something of kind Type ~>
-- Type ~> Type by writing TyCon2
-- (->), or something of kind Type -> Type
-- ~> Type by writing TyCon1 ((->)
-- t) (where t :: Type).
type a ~> b = TyFun a b -> Type
infixr 0 ~>
-- | Wrapper for converting the normal type-level arrow into a
-- ~>. For example, given:
--
--
-- data Nat = Zero | Succ Nat
-- type family Map (a :: a ~> b) (a :: [a]) :: [b]
-- Map f '[] = '[]
-- Map f (x ': xs) = Apply f x ': Map f xs
--
--
-- We can write:
--
--
-- Map (TyCon1 Succ) [Zero, Succ Zero]
--
type TyCon1 = (TyCon :: (k1 -> k2) -> (k1 ~> k2))
-- | Similar to TyCon1, but for two-parameter type constructors.
type TyCon2 = (TyCon :: (k1 -> k2 -> k3) -> (k1 ~> k2 ~> k3))
type TyCon3 = (TyCon :: (k1 -> k2 -> k3 -> k4) -> (k1 ~> k2 ~> k3 ~> k4))
type TyCon4 = (TyCon :: (k1 -> k2 -> k3 -> k4 -> k5) -> (k1 ~> k2 ~> k3 ~> k4 ~> k5))
type TyCon5 = (TyCon :: (k1 -> k2 -> k3 -> k4 -> k5 -> k6) -> (k1 ~> k2 ~> k3 ~> k4 ~> k5 ~> k6))
type TyCon6 = (TyCon :: (k1 -> k2 -> k3 -> k4 -> k5 -> k6 -> k7) -> (k1 ~> k2 ~> k3 ~> k4 ~> k5 ~> k6 ~> k7))
type TyCon7 = (TyCon :: (k1 -> k2 -> k3 -> k4 -> k5 -> k6 -> k7 -> k8) -> (k1 ~> k2 ~> k3 ~> k4 ~> k5 ~> k6 ~> k7 ~> k8))
type TyCon8 = (TyCon :: (k1 -> k2 -> k3 -> k4 -> k5 -> k6 -> k7 -> k8 -> k9) -> (k1 ~> k2 ~> k3 ~> k4 ~> k5 ~> k6 ~> k7 ~> k8 ~> k9))
-- | Type level function application
type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
-- | An infix synonym for Apply
type a @@ b = Apply a b
infixl 9 @@
-- | Workhorse for the TyCon1, etc., types. This can be used
-- directly in place of any of the TyConN types, but it will
-- work only with monomorphic types. When GHC#14645 is fixed, this
-- should fully supersede the TyConN types.
--
-- Note that this is only defined on GHC 8.6 or later. Prior to GHC 8.6,
-- TyCon1 et al. were defined as separate data types.
data family TyCon :: (k1 -> k2) -> unmatchable_fun
-- | An "internal" definition used primary in the Apply instance for
-- TyCon.
--
-- Note that this only defined on GHC 8.6 or later.
type family ApplyTyCon :: (k1 -> k2) -> (k1 ~> unmatchable_fun)
-- | An "internal" defunctionalization symbol used primarily in the
-- definition of ApplyTyCon, as well as the SingI instances
-- for TyCon1, TyCon2, etc.
--
-- Note that this is only defined on GHC 8.6 or later.
data ApplyTyConAux1 :: (k1 -> k2) -> (k1 ~> k2)
-- | An "internal" defunctionalization symbol used primarily in the
-- definition of ApplyTyCon.
--
-- Note that this is only defined on GHC 8.6 or later.
data ApplyTyConAux2 :: (k1 -> k2 -> k3) -> (k1 ~> unmatchable_fun)
-- | Use this function when passing a function on singletons as a
-- higher-order function. You will need visible type application to get
-- this to work. For example:
--
--
-- falses = sMap (singFun1 @NotSym0 sNot)
-- (STrue `SCons` STrue `SCons` SNil)
--
--
-- There are a family of singFun... functions, keyed by the
-- number of parameters of the function.
singFun1 :: forall f. SingFunction1 f -> Sing f
singFun2 :: forall f. SingFunction2 f -> Sing f
singFun3 :: forall f. SingFunction3 f -> Sing f
singFun4 :: forall f. SingFunction4 f -> Sing f
singFun5 :: forall f. SingFunction5 f -> Sing f
singFun6 :: forall f. SingFunction6 f -> Sing f
singFun7 :: forall f. SingFunction7 f -> Sing f
singFun8 :: forall f. SingFunction8 f -> Sing f
-- | This is the inverse of singFun1, and likewise for the other
-- unSingFun... functions.
unSingFun1 :: forall f. Sing f -> SingFunction1 f
unSingFun2 :: forall f. Sing f -> SingFunction2 f
unSingFun3 :: forall f. Sing f -> SingFunction3 f
unSingFun4 :: forall f. Sing f -> SingFunction4 f
unSingFun5 :: forall f. Sing f -> SingFunction5 f
unSingFun6 :: forall f. Sing f -> SingFunction6 f
unSingFun7 :: forall f. Sing f -> SingFunction7 f
unSingFun8 :: forall f. Sing f -> SingFunction8 f
pattern SLambda2 :: forall f. SingFunction2 f -> Sing f
applySing2 :: forall a1 a2 b (f :: a1 ~> (a2 ~> b)). Sing f -> forall (t1 :: a1) (t2 :: a2). () => Sing t1 -> Sing t2 -> Sing ((f @@ t1) @@ t2)
pattern SLambda3 :: forall f. SingFunction3 f -> Sing f
applySing3 :: forall a1 a2 a3 b (f :: a1 ~> (a2 ~> (a3 ~> b))). Sing f -> forall (t1 :: a1) (t2 :: a2) (t3 :: a3). () => Sing t1 -> Sing t2 -> Sing t3 -> Sing (((f @@ t1) @@ t2) @@ t3)
pattern SLambda4 :: forall f. SingFunction4 f -> Sing f
applySing4 :: forall a1 a2 a3 a4 b (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> b)))). Sing f -> forall (t1 :: a1) (t2 :: a2) (t3 :: a3) (t4 :: a4). () => Sing t1 -> Sing t2 -> Sing t3 -> Sing t4 -> Sing ((((f @@ t1) @@ t2) @@ t3) @@ t4)
pattern SLambda5 :: forall f. SingFunction5 f -> Sing f
applySing5 :: forall a1 a2 a3 a4 a5 b (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> b))))). Sing f -> forall (t1 :: a1) (t2 :: a2) (t3 :: a3) (t4 :: a4) (t5 :: a5). () => Sing t1 -> Sing t2 -> Sing t3 -> Sing t4 -> Sing t5 -> Sing (((((f @@ t1) @@ t2) @@ t3) @@ t4) @@ t5)
pattern SLambda6 :: forall f. SingFunction6 f -> Sing f
applySing6 :: forall a1 a2 a3 a4 a5 a6 b (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> (a6 ~> b)))))). Sing f -> forall (t1 :: a1) (t2 :: a2) (t3 :: a3) (t4 :: a4) (t5 :: a5) (t6 :: a6). () => Sing t1 -> Sing t2 -> Sing t3 -> Sing t4 -> Sing t5 -> Sing t6 -> Sing ((((((f @@ t1) @@ t2) @@ t3) @@ t4) @@ t5) @@ t6)
pattern SLambda7 :: forall f. SingFunction7 f -> Sing f
applySing7 :: forall a1 a2 a3 a4 a5 a6 a7 b (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> (a6 ~> (a7 ~> b))))))). Sing f -> forall (t1 :: a1) (t2 :: a2) (t3 :: a3) (t4 :: a4) (t5 :: a5) (t6 :: a6) (t7 :: a7). () => Sing t1 -> Sing t2 -> Sing t3 -> Sing t4 -> Sing t5 -> Sing t6 -> Sing t7 -> Sing (((((((f @@ t1) @@ t2) @@ t3) @@ t4) @@ t5) @@ t6) @@ t7)
pattern SLambda8 :: forall f. SingFunction8 f -> Sing f
applySing8 :: forall a1 a2 a3 a4 a5 a6 a7 a8 b (f :: a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> (a6 ~> (a7 ~> (a8 ~> b)))))))). Sing f -> forall (t1 :: a1) (t2 :: a2) (t3 :: a3) (t4 :: a4) (t5 :: a5) (t6 :: a6) (t7 :: a7) (t8 :: a8). () => Sing t1 -> Sing t2 -> Sing t3 -> Sing t4 -> Sing t5 -> Sing t6 -> Sing t7 -> Sing t8 -> Sing ((((((((f @@ t1) @@ t2) @@ t3) @@ t4) @@ t5) @@ t6) @@ t7) @@ t8)
type SingFunction1 (f :: a1 ~> b) = forall t. Sing t -> Sing (f @@ t)
type SingFunction2 (f :: a1 ~> a2 ~> b) = forall t1 t2. Sing t1 -> Sing t2 -> Sing (f @@ t1 @@ t2)
type SingFunction3 (f :: a1 ~> a2 ~> a3 ~> b) = forall t1 t2 t3. Sing t1 -> Sing t2 -> Sing t3 -> Sing (f @@ t1 @@ t2 @@ t3)
type SingFunction4 (f :: a1 ~> a2 ~> a3 ~> a4 ~> b) = forall t1 t2 t3 t4. Sing t1 -> Sing t2 -> Sing t3 -> Sing t4 -> Sing (f @@ t1 @@ t2 @@ t3 @@ t4)
type SingFunction5 (f :: a1 ~> a2 ~> a3 ~> a4 ~> a5 ~> b) = forall t1 t2 t3 t4 t5. Sing t1 -> Sing t2 -> Sing t3 -> Sing t4 -> Sing t5 -> Sing (f @@ t1 @@ t2 @@ t3 @@ t4 @@ t5)
type SingFunction6 (f :: a1 ~> a2 ~> a3 ~> a4 ~> a5 ~> a6 ~> b) = forall t1 t2 t3 t4 t5 t6. Sing t1 -> Sing t2 -> Sing t3 -> Sing t4 -> Sing t5 -> Sing t6 -> Sing (f @@ t1 @@ t2 @@ t3 @@ t4 @@ t5 @@ t6)
type SingFunction7 (f :: a1 ~> a2 ~> a3 ~> a4 ~> a5 ~> a6 ~> a7 ~> b) = forall t1 t2 t3 t4 t5 t6 t7. Sing t1 -> Sing t2 -> Sing t3 -> Sing t4 -> Sing t5 -> Sing t6 -> Sing t7 -> Sing (f @@ t1 @@ t2 @@ t3 @@ t4 @@ t5 @@ t6 @@ t7)
type SingFunction8 (f :: a1 ~> a2 ~> a3 ~> a4 ~> a5 ~> a6 ~> a7 ~> a8 ~> b) = forall t1 t2 t3 t4 t5 t6 t7 t8. Sing t1 -> Sing t2 -> Sing t3 -> Sing t4 -> Sing t5 -> Sing t6 -> Sing t7 -> Sing t8 -> Sing (f @@ t1 @@ t2 @@ t3 @@ t4 @@ t5 @@ t6 @@ t7 @@ t8)
-- | Proxy is a type that holds no data, but has a phantom parameter
-- of arbitrary type (or even kind). Its use is to provide type
-- information, even though there is no value available of that type (or
-- it may be too costly to create one).
--
-- Historically, Proxy :: Proxy a is a safer
-- alternative to the undefined :: a idiom.
--
--
-- >>> Proxy :: Proxy (Void, Int -> Int)
-- Proxy
--
--
-- Proxy can even hold types of higher kinds,
--
--
-- >>> Proxy :: Proxy Either
-- Proxy
--
--
--
-- >>> Proxy :: Proxy Functor
-- Proxy
--
--
--
-- >>> Proxy :: Proxy complicatedStructure
-- Proxy
--
data Proxy (t :: k)
Proxy :: Proxy (t :: k)
data DemoteSym0 :: Type ~> Type
type DemoteSym1 x = Demote x
data SameKindSym0 :: forall k. k ~> k ~> Constraint
data SameKindSym1 :: forall k. k -> k ~> Constraint
type SameKindSym2 (x :: k) (y :: k) = SameKind x y
data KindOfSym0 :: forall k. k ~> Type
type KindOfSym1 (x :: k) = KindOf x
data (~>@#@$) :: Type ~> Type ~> Type
infixr 0 ~>@#@$
data (~>@#@$$) :: Type -> Type ~> Type
infixr 0 ~>@#@$$
type x ~>@#@$$$ y = x ~> y
infixr 0 ~>@#@$$$
data ApplySym0 :: forall a b. (a ~> b) ~> a ~> b
data ApplySym1 :: forall a b. (a ~> b) -> a ~> b
type ApplySym2 (f :: a ~> b) (x :: a) = Apply f x
data (@@@#@$) :: forall a b. (a ~> b) ~> a ~> b
infixl 9 @@@#@$
data (@@@#@$$) :: forall a b. (a ~> b) -> a ~> b
infixl 9 @@@#@$$
type (f :: a ~> b) @@@#@$$$ (x :: a) = f @@ x
infixl 9 @@@#@$$$
instance (Data.Singletons.SingKind k1, Data.Singletons.SingKind k2) => Data.Singletons.SingKind (k1 Data.Singletons.~> k2)
instance forall k1 k2 k3 k4 k5 k6 k7 k8 kr (f :: k1 -> k2 -> k3 -> k4 -> k5 -> k6 -> k7 -> k8 -> kr). (forall (a :: k1) (b :: k2) (c :: k3) (d :: k4) (e :: k5) (f' :: k6) (g :: k7) (h :: k8). (Data.Singletons.SingI a, Data.Singletons.SingI b, Data.Singletons.SingI c, Data.Singletons.SingI d, Data.Singletons.SingI e, Data.Singletons.SingI f', Data.Singletons.SingI g, Data.Singletons.SingI h) => Data.Singletons.SingI (f a b c d e f' g h), Data.Singletons.ApplyTyCon GHC.Types.~ Data.Singletons.ApplyTyConAux1) => Data.Singletons.SingI (Data.Singletons.TyCon8 f)
instance forall k1 k2 k3 k4 k5 k6 k7 kr (f :: k1 -> k2 -> k3 -> k4 -> k5 -> k6 -> k7 -> kr). (forall (a :: k1) (b :: k2) (c :: k3) (d :: k4) (e :: k5) (f' :: k6) (g :: k7). (Data.Singletons.SingI a, Data.Singletons.SingI b, Data.Singletons.SingI c, Data.Singletons.SingI d, Data.Singletons.SingI e, Data.Singletons.SingI f', Data.Singletons.SingI g) => Data.Singletons.SingI (f a b c d e f' g), Data.Singletons.ApplyTyCon GHC.Types.~ Data.Singletons.ApplyTyConAux1) => Data.Singletons.SingI (Data.Singletons.TyCon7 f)
instance forall k1 k2 k3 k4 k5 k6 kr (f :: k1 -> k2 -> k3 -> k4 -> k5 -> k6 -> kr). (forall (a :: k1) (b :: k2) (c :: k3) (d :: k4) (e :: k5) (f' :: k6). (Data.Singletons.SingI a, Data.Singletons.SingI b, Data.Singletons.SingI c, Data.Singletons.SingI d, Data.Singletons.SingI e, Data.Singletons.SingI f') => Data.Singletons.SingI (f a b c d e f'), Data.Singletons.ApplyTyCon GHC.Types.~ Data.Singletons.ApplyTyConAux1) => Data.Singletons.SingI (Data.Singletons.TyCon6 f)
instance forall k1 k2 k3 k4 k5 kr (f :: k1 -> k2 -> k3 -> k4 -> k5 -> kr). (forall (a :: k1) (b :: k2) (c :: k3) (d :: k4) (e :: k5). (Data.Singletons.SingI a, Data.Singletons.SingI b, Data.Singletons.SingI c, Data.Singletons.SingI d, Data.Singletons.SingI e) => Data.Singletons.SingI (f a b c d e), Data.Singletons.ApplyTyCon GHC.Types.~ Data.Singletons.ApplyTyConAux1) => Data.Singletons.SingI (Data.Singletons.TyCon5 f)
instance forall k1 k2 k3 k4 kr (f :: k1 -> k2 -> k3 -> k4 -> kr). (forall (a :: k1) (b :: k2) (c :: k3) (d :: k4). (Data.Singletons.SingI a, Data.Singletons.SingI b, Data.Singletons.SingI c, Data.Singletons.SingI d) => Data.Singletons.SingI (f a b c d), Data.Singletons.ApplyTyCon GHC.Types.~ Data.Singletons.ApplyTyConAux1) => Data.Singletons.SingI (Data.Singletons.TyCon4 f)
instance forall k1 k2 k3 kr (f :: k1 -> k2 -> k3 -> kr). (forall (a :: k1) (b :: k2) (c :: k3). (Data.Singletons.SingI a, Data.Singletons.SingI b, Data.Singletons.SingI c) => Data.Singletons.SingI (f a b c), Data.Singletons.ApplyTyCon GHC.Types.~ Data.Singletons.ApplyTyConAux1) => Data.Singletons.SingI (Data.Singletons.TyCon3 f)
instance forall k1 k2 kr (f :: k1 -> k2 -> kr). (forall (a :: k1) (b :: k2). (Data.Singletons.SingI a, Data.Singletons.SingI b) => Data.Singletons.SingI (f a b), Data.Singletons.ApplyTyCon GHC.Types.~ Data.Singletons.ApplyTyConAux1) => Data.Singletons.SingI (Data.Singletons.TyCon2 f)
instance forall k1 kr (f :: k1 -> kr). (forall (a :: k1). Data.Singletons.SingI a => Data.Singletons.SingI (f a), Data.Singletons.ApplyTyCon GHC.Types.~ Data.Singletons.ApplyTyConAux1) => Data.Singletons.SingI (Data.Singletons.TyCon1 f)
instance forall k (a :: k). Data.Singletons.SingKind (Data.Singletons.WrappedSing a)
instance forall k (a :: k) (s :: Data.Singletons.Sing a). Data.Singletons.SingI a => Data.Singletons.SingI ('Data.Singletons.WrapSing s)
-- | Defines the class SDecide, allowing for decidable equality over
-- singletons.
module Data.Singletons.Decide
-- | Members of the SDecide "kind" class support decidable equality.
-- Instances of this class are generated alongside singleton definitions
-- for datatypes that derive an Eq instance.
class SDecide k
-- | Compute a proof or disproof of equality, given two singletons.
(%~) :: forall (a :: k) (b :: k). SDecide k => Sing a -> Sing b -> Decision (a :~: b)
infix 4 %~
-- | Propositional equality. If a :~: b is inhabited by some
-- terminating value, then the type a is the same as the type
-- b. To use this equality in practice, pattern-match on the
-- a :~: b to get out the Refl constructor; in the body
-- of the pattern-match, the compiler knows that a ~ b.
data (a :: k) :~: (b :: k)
[Refl] :: forall k (a :: k). a :~: a
infix 4 :~:
-- | Uninhabited data type
data Void
-- | Because we can never create a value of type Void, a function
-- that type-checks at a -> Void shows that objects of type
-- a can never exist. Thus, we say that a is
-- Refuted
type Refuted a = (a -> Void)
-- | A Decision about a type a is either a proof of
-- existence or a proof that a cannot exist.
data Decision a
-- | Witness for a
Proved :: a -> Decision a
-- | Proof that no a exists
Disproved :: Refuted a -> Decision a
-- | A suitable default implementation for testEquality that
-- leverages SDecide.
decideEquality :: forall k (a :: k) (b :: k). SDecide k => Sing a -> Sing b -> Maybe (a :~: b)
-- | A suitable default implementation for testCoercion that
-- leverages SDecide.
decideCoercion :: forall k (a :: k) (b :: k). SDecide k => Sing a -> Sing b -> Maybe (Coercion a b)
instance Data.Singletons.Decide.SDecide k => Data.Type.Equality.TestEquality Data.Singletons.WrappedSing
instance Data.Singletons.Decide.SDecide k => Data.Type.Coercion.TestCoercion Data.Singletons.WrappedSing
-- | Defines the class ShowSing which is useful for defining
-- Show instances for singleton types. Because ShowSing
-- crucially relies on QuantifiedConstraints, it is only defined
-- if this library is built with GHC 8.6 or later.
module Data.Singletons.ShowSing
-- | In addition to the promoted and singled versions of the Show
-- class that singletons-base provides, it is also useful to be
-- able to directly define Show instances for singleton types
-- themselves. Doing so is almost entirely straightforward, as a derived
-- Show instance does 90 percent of the work. The last 10
-- percent—getting the right instance context—is a bit tricky, and that's
-- where ShowSing comes into play.
--
-- As an example, let's consider the singleton type for lists. We want to
-- write an instance with the following shape:
--
--
-- instance ??? => Show (SList (z :: [k])) where
-- showsPrec p SNil = showString "SNil"
-- showsPrec p (SCons sx sxs) =
-- showParen (p > 10) $ showString "SCons " . showsPrec 11 sx
-- . showSpace . showsPrec 11 sxs
--
--
-- To figure out what should go in place of ???, observe that we
-- require the type of each field to also be Show instances. In
-- other words, we need something like (Show (Sing (a
-- :: k))). But this isn't quite right, as the type variable
-- a doesn't appear in the instance head. In fact, this
-- a type is really referring to an existentially quantified
-- type variable in the SCons constructor, so it doesn't make
-- sense to try and use it like this.
--
-- Luckily, the QuantifiedConstraints language extension
-- provides a solution to this problem. This lets you write a context of
-- the form (forall a. Show (Sing (a :: k))),
-- which demands that there be an instance for Show
-- (Sing (a :: k)) that is parametric in the use of
-- a. This lets us write something closer to this:
--
--
-- instance (forall a. Show (Sing (a :: k))) => SList (Sing (z :: [k])) where ...
--
--
-- The ShowSing class is a thin wrapper around (forall a.
-- Show (Sing (a :: k))). With ShowSing, our
-- final instance declaration becomes this:
--
--
-- instance ShowSing k => Show (SList (z :: [k])) where ...
--
--
-- In fact, this instance can be derived:
--
--
-- deriving instance ShowSing k => Show (SList (z :: [k]))
--
--
-- (Note that the actual definition of ShowSing is slightly more
-- complicated than what this documentation might suggest. For the full
-- story, refer to the documentation for ShowSing`.)
--
-- When singling a derived Show instance, singletons-th
-- will also generate a Show instance for the corresponding
-- singleton type using ShowSing. In other words, if you give
-- singletons-th a derived Show instance, then you'll
-- receive the following in return:
--
--
-- - A promoted (PShow) instance
-- - A singled (SShow) instance
-- - A Show instance for the singleton type
--
--
-- What a bargain!
class (forall (z :: k). ShowSing' z) => ShowSing (k :: Type)
-- | The workhorse that powers ShowSing. The only reason that
-- ShowSing` exists is to work around GHC's inability to put type
-- families in the head of a quantified constraint (see this GHC
-- issue for more details on this point). In other words, GHC will
-- not let you define ShowSing like so:
--
--
-- class (forall (z :: k). Show (Sing z)) => ShowSing k
--
--
-- By replacing Show (Sing z) with ShowSing'
-- z, we are able to avoid this restriction for the most part.
--
-- The superclass of ShowSing` is a bit peculiar:
--
--
-- class (forall (sing :: k -> Type). sing ~ Sing => Show (sing z)) => ShowSing` (z :: k)
--
--
-- One might wonder why this superclass is used instead of this seemingly
-- more direct equivalent:
--
--
-- class Show (Sing z) => ShowSing` (z :: k)
--
--
-- Actually, these aren't equivalent! The latter's superclass mentions a
-- type family in its head, and this gives GHC's constraint solver
-- trouble when trying to match this superclass against other
-- constraints. (See the discussion beginning at
-- https://gitlab.haskell.org/ghc/ghc/-/issues/16365#note_189057
-- for more on this point). The former's superclass, on the other hand,
-- does not mention a type family in its head, which allows it to
-- match other constraints more easily. It may sound like a small
-- difference, but it's the only reason that ShowSing is able to
-- work at all without a significant amount of additional workarounds.
--
-- The quantified superclass has one major downside. Although the head of
-- the quantified superclass is more eager to match, which is usually a
-- good thing, it can bite under certain circumstances. Because
-- Show (sing z) will match a Show instance for
-- any types sing :: k -> Type and z :: k,
-- (where k is a kind variable), it is possible for GHC's
-- constraint solver to get into a situation where multiple instances
-- match Show (sing z), and GHC will get confused as a
-- result. Consider this example:
--
--
-- -- As in Data.Singletons
-- newtype WrappedSing :: forall k. k -> Type where
-- WrapSing :: forall k (a :: k). { unwrapSing :: Sing a } -> WrappedSing a
--
-- instance ShowSing k => Show (WrappedSing (a :: k)) where
-- showsPrec _ s = showString "WrapSing {unwrapSing = " . showsPrec 0 s . showChar '}'
--
--
-- When typechecking the Show instance for WrappedSing, GHC
-- must fill in a default definition show = defaultShow,
-- where defaultShow :: Show (WrappedSing a) =>
-- WrappedSing a -> String. GHC's constraint solver
-- has two possible ways to satisfy the Show
-- (WrappedSing a) constraint for defaultShow:
--
--
-- - The top-level instance declaration for Show
-- (WrappedSing (a :: k)) itself, and
-- - Show (sing (z :: k)) from the head of the
-- quantified constraint arising from ShowSing k.
--
--
-- In practice, GHC will choose (2), as local quantified constraints
-- shadow global constraints. This confuses GHC greatly, causing it to
-- error out with an error akin to Couldn't match type Sing with
-- WrappedSing. See
-- https://gitlab.haskell.org/ghc/ghc/-/issues/17934 for a full
-- diagnosis of the issue.
--
-- The bad news is that because of GHC#17934, we have to manually define
-- show (and showList) in the Show instance for
-- WrappedSing in order to avoid confusing GHC's constraint
-- solver. In other words, deriving Show is a no-go for
-- WrappedSing. The good news is that situations like
-- WrappedSing are quite rare in the world of
-- singletons—most of the time, Show instances for
-- singleton types do not have the shape Show (sing (z
-- :: k)), where k is a polymorphic kind variable. Rather,
-- most such instances instantiate k to a specific kind (e.g.,
-- Bool, or [a]), which means that they will not
-- overlap the head of the quantified superclass in ShowSing` as
-- observed above.
--
-- Note that we define the single instance for ShowSing` without
-- the use of a quantified constraint in the instance context:
--
--
-- instance Show (Sing z) => ShowSing` (z :: k)
--
--
-- We could define this instance with a quantified constraint in
-- the instance context, and it would be equally as expressive. But it
-- doesn't provide any additional functionality that the non-quantified
-- version gives, so we opt for the non-quantified version, which is
-- easier to read.
class (forall (sing :: k -> Type). sing ~ Sing => Show (sing z)) => ShowSing' (z :: k)
instance forall k (a :: k) (ws :: Data.Singletons.WrappedSing a). Data.Singletons.ShowSing.ShowSing k => GHC.Show.Show (Data.Singletons.SWrappedSing ws)
instance (forall (z :: k). Data.Singletons.ShowSing.ShowSing' z) => Data.Singletons.ShowSing.ShowSing k
instance forall k (a :: k). Data.Singletons.ShowSing.ShowSing k => GHC.Show.Show (Data.Singletons.WrappedSing a)
instance forall k (z :: k). GHC.Show.Show (Data.Singletons.Sing z) => Data.Singletons.ShowSing.ShowSing' z
-- | Defines Sigma, a dependent pair data type, and related
-- functions.
module Data.Singletons.Sigma
-- | A dependent pair.
data Sigma (s :: Type) :: (s ~> Type) -> Type
[:&:] :: forall s t fst. Sing (fst :: s) -> (t @@ fst) -> Sigma s t
infixr 4 :&:
-- | Unicode shorthand for Sigma.
type Σ = Sigma
-- | The singleton kind-indexed type family.
type family Sing :: k -> Type
-- | The singleton type for Sigma.
data SSigma :: forall s t. Sigma s t -> Type
[:%&:] :: forall s t (fst :: s) (sfst :: Sing fst) (snd :: t @@ fst). Sing ('WrapSing sfst) -> Sing snd -> SSigma (sfst :&: snd :: Sigma s t)
infixr 4 :%&:
-- | Unicode shorthand for SSigma.
type SΣ = SSigma
-- | Project the first element out of a dependent pair.
fstSigma :: forall s t. SingKind s => Sigma s t -> Demote s
-- | Project the first element out of a dependent pair.
type family FstSigma (sig :: Sigma s t) :: s
-- | Project the second element out of a dependent pair.
sndSigma :: forall s t (sig :: Sigma s t). SingKind (t @@ FstSigma sig) => SSigma sig -> Demote (t @@ FstSigma sig)
-- | Project the second element out of a dependent pair.
type family SndSigma (sig :: Sigma s t) :: t @@ FstSigma sig
-- | Project the first element out of a dependent pair using
-- continuation-passing style.
projSigma1 :: (forall (fst :: s). Sing fst -> r) -> Sigma s t -> r
-- | Project the second element out of a dependent pair using
-- continuation-passing style.
projSigma2 :: forall s t r. (forall (fst :: s). (t @@ fst) -> r) -> Sigma s t -> r
-- | Map across a Sigma value in a dependent fashion.
mapSigma :: Sing (f :: a ~> b) -> (forall (x :: a). (p @@ x) -> q @@ (f @@ x)) -> Sigma a p -> Sigma b q
-- | Zip two Sigma values together in a dependent fashion.
zipSigma :: Sing (f :: a ~> (b ~> c)) -> (forall (x :: a) (y :: b). (p @@ x) -> (q @@ y) -> r @@ ((f @@ x) @@ y)) -> Sigma a p -> Sigma b q -> Sigma c r
-- | Convert an uncurried function on Sigma to a curried one.
--
-- Together, currySigma and uncurrySigma witness an
-- isomorphism such that the following identities hold:
--
--
-- id1 :: forall a (b :: a ~> Type) (c :: Sigma a b ~> Type).
-- (forall (p :: Sigma a b). SSigma p -> c @ p)
-- -> (forall (p :: Sigma a b). SSigma p -> c p)
-- id1 f = uncurrySigma a b c (currySigma a b c f)
--
-- id2 :: forall a (b :: a ~> Type) (c :: Sigma a b ~> Type).
-- (forall (x :: a) (sx :: Sing x) (y :: b x). Sing (WrapSing sx) -> Sing y -> c (sx :&: y))
-- -> (forall (x :: a) (sx :: Sing x) (y :: b x). Sing (WrapSing sx) -> Sing y -> c (sx :&: y))
-- id2 f = currySigma a b c (uncurrySigma a b @c f)
--
currySigma :: forall a (b :: a ~> Type) (c :: Sigma a b ~> Type). (forall (p :: Sigma a b). SSigma p -> c @@ p) -> forall (x :: a) (sx :: Sing x) (y :: b @@ x). Sing ('WrapSing sx) -> Sing y -> c @@ (sx :&: y)
-- | Convert a curried function on Sigma to an uncurried one.
--
-- Together, currySigma and uncurrySigma witness an
-- isomorphism. (Refer to the documentation for currySigma for
-- more details.)
uncurrySigma :: forall a (b :: a ~> Type) (c :: Sigma a b ~> Type). (forall (x :: a) (sx :: Sing x) (y :: b @@ x). Sing ('WrapSing sx) -> Sing y -> c @@ (sx :&: y)) -> forall (p :: Sigma a b). SSigma p -> c @@ p
class (forall (x :: a). ShowApply' f x) => ShowApply (f :: a ~> Type)
class (forall (x :: a) (z :: Apply f x). ShowSingApply' f x z) => ShowSingApply (f :: a ~> Type)
class Show (Apply f x) => ShowApply' (f :: a ~> Type) (x :: a)
class Show (Sing z) => ShowSingApply' (f :: a ~> Type) (x :: a) (z :: Apply f x)
instance forall s (t :: s Data.Singletons.~> *) (sig :: Data.Singletons.Sigma.Sigma s t). (Data.Singletons.ShowSing.ShowSing s, Data.Singletons.Sigma.ShowSingApply t) => GHC.Show.Show (Data.Singletons.Sigma.SSigma sig)
instance forall a (f :: a Data.Singletons.~> *). (forall (x :: a) (z :: Data.Singletons.Apply f x). Data.Singletons.Sigma.ShowSingApply' f x z) => Data.Singletons.Sigma.ShowSingApply f
instance forall a (f :: a Data.Singletons.~> *) (x :: a) (z :: Data.Singletons.Apply f x). GHC.Show.Show (Data.Singletons.Sing z) => Data.Singletons.Sigma.ShowSingApply' f x z
instance forall s (t :: s Data.Singletons.~> *). (Data.Singletons.ShowSing.ShowSing s, Data.Singletons.Sigma.ShowApply t) => GHC.Show.Show (Data.Singletons.Sigma.Sigma s t)
instance forall a (f :: a Data.Singletons.~> *). (forall (x :: a). Data.Singletons.Sigma.ShowApply' f x) => Data.Singletons.Sigma.ShowApply f
instance forall a (f :: a Data.Singletons.~> *) (x :: a). GHC.Show.Show (Data.Singletons.Apply f x) => Data.Singletons.Sigma.ShowApply' f x
instance forall s (t :: s Data.Singletons.~> *) (fst :: s) (a :: Data.Singletons.Sing fst) (b :: t Data.Singletons.@@ fst). (Data.Singletons.SingI fst, Data.Singletons.SingI b) => Data.Singletons.SingI (a 'Data.Singletons.Sigma.:&: b)