Copyright	(C) 2018 Ryan Scott
License	BSD-style (see LICENSE)
Maintainer	Ryan Scott
Stability	experimental
Portability	non-portable
Safe Haskell	None
Language	Haskell2010

Data.Singletons.Prelude.Applicative

Contents

Defunctionalization symbols
Orphan instances

Description

Defines the promoted and singled versions of the Applicative type class.

Synopsis

class PFunctor f => PApplicative (f :: Type -> Type) where
- type Pure (arg :: a) :: f a
- type (arg :: f ((~>) a b)) <*> (arg :: f a) :: f b
- type LiftA2 (arg :: (~>) a ((~>) b c)) (arg :: f a) (arg :: f b) :: f c
- type (arg :: f a) *> (arg :: f b) :: f b
- type (arg :: f a) <* (arg :: f b) :: f a
class SFunctor f => SApplicative (f :: Type -> Type) where
- sPure :: forall a (t :: a). Sing t -> Sing (Apply PureSym0 t :: f a)
- (%<*>) :: forall a b (t :: f ((~>) a b)) (t :: f a). Sing t -> Sing t -> Sing (Apply (Apply (<*>@#@$) t) t :: f b)
- sLiftA2 :: forall a b c (t :: (~>) a ((~>) b c)) (t :: f a) (t :: f b). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply LiftA2Sym0 t) t) t :: f c)
- (%*>) :: forall a b (t :: f a) (t :: f b). Sing t -> Sing t -> Sing (Apply (Apply (*>@#@$) t) t :: f b)
- (%<*) :: forall a b (t :: f a) (t :: f b). Sing t -> Sing t -> Sing (Apply (Apply (<*@#@$) t) t :: f a)
class PApplicative f => PAlternative (f :: Type -> Type) where
- type Empty :: f a
- type (arg :: f a) <|> (arg :: f a) :: f a
class SApplicative f => SAlternative (f :: Type -> Type) where
- sEmpty :: forall a. Sing (EmptySym0 :: f a)
- (%<|>) :: forall a (t :: f a) (t :: f a). Sing t -> Sing t -> Sing (Apply (Apply (<|>@#@$) t) t :: f a)
data family Sing :: k -> Type
type SConst = (Sing :: Const a b -> Type)
data Const a (b :: k) :: forall k. Type -> k -> Type
type family GetConst (x :: Const a b) :: a where ...
type family (a :: (~>) a b) <$> (a :: f a) :: f b where ...
(%<$>) :: forall f a b (t :: (~>) a b) (t :: f a). SFunctor f => Sing t -> Sing t -> Sing (Apply (Apply (<$>@#@$) t) t :: f b)
type family (arg :: a) <$ (arg :: f b) :: f a
(%<$) :: forall a b (t :: a) (t :: f b). SFunctor f => Sing t -> Sing t -> Sing (Apply (Apply (<$@#@$) t) t :: f a)
type family (a :: f a) <**> (a :: f ((~>) a b)) :: f b where ...
(%<**>) :: forall f a b (t :: f a) (t :: f ((~>) a b)). SApplicative f => Sing t -> Sing t -> Sing (Apply (Apply (<**>@#@$) t) t :: f b)
type family LiftA (a :: (~>) a b) (a :: f a) :: f b where ...
sLiftA :: forall f a b (t :: (~>) a b) (t :: f a). SApplicative f => Sing t -> Sing t -> Sing (Apply (Apply LiftASym0 t) t :: f b)
type family LiftA3 (a :: (~>) a ((~>) b ((~>) c d))) (a :: f a) (a :: f b) (a :: f c) :: f d where ...
sLiftA3 :: forall f a b c d (t :: (~>) a ((~>) b ((~>) c d))) (t :: f a) (t :: f b) (t :: f c). SApplicative f => Sing t -> Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply (Apply LiftA3Sym0 t) t) t) t :: f d)
type family Optional (a :: f a) :: f (Maybe a) where ...
sOptional :: forall f a (t :: f a). SAlternative f => Sing t -> Sing (Apply OptionalSym0 t :: f (Maybe a))
data PureSym0 :: forall a6989586621679563428 f6989586621679563427. (~>) a6989586621679563428 (f6989586621679563427 a6989586621679563428)
type PureSym1 (arg6989586621679563840 :: a6989586621679563428) = Pure arg6989586621679563840
data (<*>@#@$) :: forall a6989586621679563429 b6989586621679563430 f6989586621679563427. (~>) (f6989586621679563427 ((~>) a6989586621679563429 b6989586621679563430)) ((~>) (f6989586621679563427 a6989586621679563429) (f6989586621679563427 b6989586621679563430))
data (<*>@#@$$) (arg6989586621679563842 :: f6989586621679563427 ((~>) a6989586621679563429 b6989586621679563430)) :: (~>) (f6989586621679563427 a6989586621679563429) (f6989586621679563427 b6989586621679563430)
type (<*>@#@$$$) (arg6989586621679563842 :: f6989586621679563427 ((~>) a6989586621679563429 b6989586621679563430)) (arg6989586621679563843 :: f6989586621679563427 a6989586621679563429) = (<*>) arg6989586621679563842 arg6989586621679563843
data (*>@#@$) :: forall a6989586621679563434 b6989586621679563435 f6989586621679563427. (~>) (f6989586621679563427 a6989586621679563434) ((~>) (f6989586621679563427 b6989586621679563435) (f6989586621679563427 b6989586621679563435))
data (*>@#@$$) (arg6989586621679563852 :: f6989586621679563427 a6989586621679563434) :: forall b6989586621679563435. (~>) (f6989586621679563427 b6989586621679563435) (f6989586621679563427 b6989586621679563435)
type (*>@#@$$$) (arg6989586621679563852 :: f6989586621679563427 a6989586621679563434) (arg6989586621679563853 :: f6989586621679563427 b6989586621679563435) = (*>) arg6989586621679563852 arg6989586621679563853
data (<*@#@$) :: forall a6989586621679563436 b6989586621679563437 f6989586621679563427. (~>) (f6989586621679563427 a6989586621679563436) ((~>) (f6989586621679563427 b6989586621679563437) (f6989586621679563427 a6989586621679563436))
data (<*@#@$$) (arg6989586621679563856 :: f6989586621679563427 a6989586621679563436) :: forall b6989586621679563437. (~>) (f6989586621679563427 b6989586621679563437) (f6989586621679563427 a6989586621679563436)
type (<*@#@$$$) (arg6989586621679563856 :: f6989586621679563427 a6989586621679563436) (arg6989586621679563857 :: f6989586621679563427 b6989586621679563437) = (<*) arg6989586621679563856 arg6989586621679563857
type EmptySym0 = Empty
data (<|>@#@$) :: forall a6989586621679563506 f6989586621679563504. (~>) (f6989586621679563504 a6989586621679563506) ((~>) (f6989586621679563504 a6989586621679563506) (f6989586621679563504 a6989586621679563506))
data (<|>@#@$$) (arg6989586621679563973 :: f6989586621679563504 a6989586621679563506) :: (~>) (f6989586621679563504 a6989586621679563506) (f6989586621679563504 a6989586621679563506)
type (<|>@#@$$$) (arg6989586621679563973 :: f6989586621679563504 a6989586621679563506) (arg6989586621679563974 :: f6989586621679563504 a6989586621679563506) = (<|>) arg6989586621679563973 arg6989586621679563974
data ConstSym0 :: forall (a6989586621679093209 :: Type) k6989586621679093208 (b6989586621679093210 :: k6989586621679093208). (~>) a6989586621679093209 (Const (a6989586621679093209 :: Type) (b6989586621679093210 :: k6989586621679093208))
type ConstSym1 (t6989586621680750415 :: a6989586621679093209) = Const t6989586621680750415
data GetConstSym0 :: forall a6989586621680750730 b6989586621680750731. (~>) (Const a6989586621680750730 b6989586621680750731) a6989586621680750730
type GetConstSym1 (x6989586621680750732 :: Const a6989586621680750730 b6989586621680750731) = GetConst x6989586621680750732
data (<$>@#@$) :: forall a6989586621679735752 b6989586621679735753 f6989586621679735751. (~>) ((~>) a6989586621679735752 b6989586621679735753) ((~>) (f6989586621679735751 a6989586621679735752) (f6989586621679735751 b6989586621679735753))
data (<$>@#@$$) (a6989586621679735832 :: (~>) a6989586621679735752 b6989586621679735753) :: forall f6989586621679735751. (~>) (f6989586621679735751 a6989586621679735752) (f6989586621679735751 b6989586621679735753)
type (<$>@#@$$$) (a6989586621679735832 :: (~>) a6989586621679735752 b6989586621679735753) (a6989586621679735833 :: f6989586621679735751 a6989586621679735752) = (<$>) a6989586621679735832 a6989586621679735833
data (<$@#@$) :: forall a6989586621679563425 b6989586621679563426 f6989586621679563422. (~>) a6989586621679563425 ((~>) (f6989586621679563422 b6989586621679563426) (f6989586621679563422 a6989586621679563425))
data (<$@#@$$) (arg6989586621679563820 :: a6989586621679563425) :: forall b6989586621679563426 f6989586621679563422. (~>) (f6989586621679563422 b6989586621679563426) (f6989586621679563422 a6989586621679563425)
type (<$@#@$$$) (arg6989586621679563820 :: a6989586621679563425) (arg6989586621679563821 :: f6989586621679563422 b6989586621679563426) = (<$) arg6989586621679563820 arg6989586621679563821
data (<**>@#@$) :: forall a6989586621679563387 b6989586621679563388 f6989586621679563386. (~>) (f6989586621679563386 a6989586621679563387) ((~>) (f6989586621679563386 ((~>) a6989586621679563387 b6989586621679563388)) (f6989586621679563386 b6989586621679563388))
data (<**>@#@$$) (a6989586621679563800 :: f6989586621679563386 a6989586621679563387) :: forall b6989586621679563388. (~>) (f6989586621679563386 ((~>) a6989586621679563387 b6989586621679563388)) (f6989586621679563386 b6989586621679563388)
type (<**>@#@$$$) (a6989586621679563800 :: f6989586621679563386 a6989586621679563387) (a6989586621679563801 :: f6989586621679563386 ((~>) a6989586621679563387 b6989586621679563388)) = (<**>) a6989586621679563800 a6989586621679563801
data LiftASym0 :: forall a6989586621679563384 b6989586621679563385 f6989586621679563383. (~>) ((~>) a6989586621679563384 b6989586621679563385) ((~>) (f6989586621679563383 a6989586621679563384) (f6989586621679563383 b6989586621679563385))
data LiftASym1 (a6989586621679563790 :: (~>) a6989586621679563384 b6989586621679563385) :: forall f6989586621679563383. (~>) (f6989586621679563383 a6989586621679563384) (f6989586621679563383 b6989586621679563385)
type LiftASym2 (a6989586621679563790 :: (~>) a6989586621679563384 b6989586621679563385) (a6989586621679563791 :: f6989586621679563383 a6989586621679563384) = LiftA a6989586621679563790 a6989586621679563791
data LiftA2Sym0 :: forall a6989586621679563431 b6989586621679563432 c6989586621679563433 f6989586621679563427. (~>) ((~>) a6989586621679563431 ((~>) b6989586621679563432 c6989586621679563433)) ((~>) (f6989586621679563427 a6989586621679563431) ((~>) (f6989586621679563427 b6989586621679563432) (f6989586621679563427 c6989586621679563433)))
data LiftA2Sym1 (arg6989586621679563846 :: (~>) a6989586621679563431 ((~>) b6989586621679563432 c6989586621679563433)) :: forall f6989586621679563427. (~>) (f6989586621679563427 a6989586621679563431) ((~>) (f6989586621679563427 b6989586621679563432) (f6989586621679563427 c6989586621679563433))
data LiftA2Sym2 (arg6989586621679563846 :: (~>) a6989586621679563431 ((~>) b6989586621679563432 c6989586621679563433)) (arg6989586621679563847 :: f6989586621679563427 a6989586621679563431) :: (~>) (f6989586621679563427 b6989586621679563432) (f6989586621679563427 c6989586621679563433)
type LiftA2Sym3 (arg6989586621679563846 :: (~>) a6989586621679563431 ((~>) b6989586621679563432 c6989586621679563433)) (arg6989586621679563847 :: f6989586621679563427 a6989586621679563431) (arg6989586621679563848 :: f6989586621679563427 b6989586621679563432) = LiftA2 arg6989586621679563846 arg6989586621679563847 arg6989586621679563848
data LiftA3Sym0 :: forall a6989586621679563379 b6989586621679563380 c6989586621679563381 d6989586621679563382 f6989586621679563378. (~>) ((~>) a6989586621679563379 ((~>) b6989586621679563380 ((~>) c6989586621679563381 d6989586621679563382))) ((~>) (f6989586621679563378 a6989586621679563379) ((~>) (f6989586621679563378 b6989586621679563380) ((~>) (f6989586621679563378 c6989586621679563381) (f6989586621679563378 d6989586621679563382))))
data LiftA3Sym1 (a6989586621679563778 :: (~>) a6989586621679563379 ((~>) b6989586621679563380 ((~>) c6989586621679563381 d6989586621679563382))) :: forall f6989586621679563378. (~>) (f6989586621679563378 a6989586621679563379) ((~>) (f6989586621679563378 b6989586621679563380) ((~>) (f6989586621679563378 c6989586621679563381) (f6989586621679563378 d6989586621679563382)))
data LiftA3Sym2 (a6989586621679563778 :: (~>) a6989586621679563379 ((~>) b6989586621679563380 ((~>) c6989586621679563381 d6989586621679563382))) (a6989586621679563779 :: f6989586621679563378 a6989586621679563379) :: (~>) (f6989586621679563378 b6989586621679563380) ((~>) (f6989586621679563378 c6989586621679563381) (f6989586621679563378 d6989586621679563382))
data LiftA3Sym3 (a6989586621679563778 :: (~>) a6989586621679563379 ((~>) b6989586621679563380 ((~>) c6989586621679563381 d6989586621679563382))) (a6989586621679563779 :: f6989586621679563378 a6989586621679563379) (a6989586621679563780 :: f6989586621679563378 b6989586621679563380) :: (~>) (f6989586621679563378 c6989586621679563381) (f6989586621679563378 d6989586621679563382)
data OptionalSym0 :: forall a6989586621681250517 f6989586621681250516. (~>) (f6989586621681250516 a6989586621681250517) (f6989586621681250516 (Maybe a6989586621681250517))
type OptionalSym1 (a6989586621681250556 :: f6989586621681250516 a6989586621681250517) = Optional a6989586621681250556

Documentation

class PFunctor f => PApplicative (f :: Type -> Type) #

Associated Types

type Pure (arg :: a) :: f a #

type (arg :: f ((~>) a b)) <*> (arg :: f a) :: f b infixl 4 #

type LiftA2 (arg :: (~>) a ((~>) b c)) (arg :: f a) (arg :: f b) :: f c #

type (arg :: f a) *> (arg :: f b) :: f b infixl 4 #

type (arg :: f a) <* (arg :: f b) :: f a infixl 4 #

Instances

PApplicative [] #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Associated Types type Pure arg :: f a # type arg <> arg :: f b # type LiftA2 arg arg arg :: f c # type arg > arg :: f b # type arg <* arg :: f a #
PApplicative Maybe #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Associated Types type Pure arg :: f a # type arg <> arg :: f b # type LiftA2 arg arg arg :: f c # type arg > arg :: f b # type arg <* arg :: f a #
PApplicative Min #
Instance details Defined in Data.Singletons.Prelude.Semigroup Associated Types type Pure arg :: f a # type arg <> arg :: f b # type LiftA2 arg arg arg :: f c # type arg > arg :: f b # type arg <* arg :: f a #
PApplicative Max #
Instance details Defined in Data.Singletons.Prelude.Semigroup Associated Types type Pure arg :: f a # type arg <> arg :: f b # type LiftA2 arg arg arg :: f c # type arg > arg :: f b # type arg <* arg :: f a #
PApplicative First #
Instance details Defined in Data.Singletons.Prelude.Semigroup Associated Types type Pure arg :: f a # type arg <> arg :: f b # type LiftA2 arg arg arg :: f c # type arg > arg :: f b # type arg <* arg :: f a #
PApplicative Last #
Instance details Defined in Data.Singletons.Prelude.Semigroup Associated Types type Pure arg :: f a # type arg <> arg :: f b # type LiftA2 arg arg arg :: f c # type arg > arg :: f b # type arg <* arg :: f a #
PApplicative Option #
Instance details Defined in Data.Singletons.Prelude.Semigroup Associated Types type Pure arg :: f a # type arg <> arg :: f b # type LiftA2 arg arg arg :: f c # type arg > arg :: f b # type arg <* arg :: f a #
PApplicative Identity #
Instance details Defined in Data.Singletons.Prelude.Identity Associated Types type Pure arg :: f a # type arg <> arg :: f b # type LiftA2 arg arg arg :: f c # type arg > arg :: f b # type arg <* arg :: f a #
PApplicative First #
Instance details Defined in Data.Singletons.Prelude.Monoid Associated Types type Pure arg :: f a # type arg <> arg :: f b # type LiftA2 arg arg arg :: f c # type arg > arg :: f b # type arg <* arg :: f a #
PApplicative Last #
Instance details Defined in Data.Singletons.Prelude.Monoid Associated Types type Pure arg :: f a # type arg <> arg :: f b # type LiftA2 arg arg arg :: f c # type arg > arg :: f b # type arg <* arg :: f a #
PApplicative Dual #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Associated Types type Pure arg :: f a # type arg <> arg :: f b # type LiftA2 arg arg arg :: f c # type arg > arg :: f b # type arg <* arg :: f a #
PApplicative Sum #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Associated Types type Pure arg :: f a # type arg <> arg :: f b # type LiftA2 arg arg arg :: f c # type arg > arg :: f b # type arg <* arg :: f a #
PApplicative Product #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Associated Types type Pure arg :: f a # type arg <> arg :: f b # type LiftA2 arg arg arg :: f c # type arg > arg :: f b # type arg <* arg :: f a #
PApplicative Down #
Instance details Defined in Data.Singletons.Prelude.Applicative Associated Types type Pure arg :: f a # type arg <> arg :: f b # type LiftA2 arg arg arg :: f c # type arg > arg :: f b # type arg <* arg :: f a #
PApplicative NonEmpty #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Associated Types type Pure arg :: f a # type arg <> arg :: f b # type LiftA2 arg arg arg :: f c # type arg > arg :: f b # type arg <* arg :: f a #
PApplicative (Either e) #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Associated Types type Pure arg :: f a # type arg <> arg :: f b # type LiftA2 arg arg arg :: f c # type arg > arg :: f b # type arg <* arg :: f a #
PApplicative ((,) a) #
Instance details Defined in Data.Singletons.Prelude.Applicative Associated Types type Pure arg :: f a # type arg <> arg :: f b # type LiftA2 arg arg arg :: f c # type arg > arg :: f b # type arg <* arg :: f a #
PApplicative (Const m :: Type -> Type) #
Instance details Defined in Data.Singletons.Prelude.Const Associated Types type Pure arg :: f a # type arg <> arg :: f b # type LiftA2 arg arg arg :: f c # type arg > arg :: f b # type arg <* arg :: f a #

class SFunctor f => SApplicative (f :: Type -> Type) where #

Minimal complete definition

sPure

Methods

sPure :: forall a (t :: a). Sing t -> Sing (Apply PureSym0 t :: f a) #

(%<*>) :: forall a b (t :: f ((~>) a b)) (t :: f a). Sing t -> Sing t -> Sing (Apply (Apply (<*>@#@$) t) t :: f b) infixl 4 #

sLiftA2 :: forall a b c (t :: (~>) a ((~>) b c)) (t :: f a) (t :: f b). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply LiftA2Sym0 t) t) t :: f c) #

(%*>) :: forall a b (t :: f a) (t :: f b). Sing t -> Sing t -> Sing (Apply (Apply (*>@#@$) t) t :: f b) infixl 4 #

(%<*) :: forall a b (t :: f a) (t :: f b). Sing t -> Sing t -> Sing (Apply (Apply (<*@#@$) t) t :: f a) infixl 4 #

(%<*>) :: forall a b (t :: f ((~>) a b)) (t :: f a). (Apply (Apply (<*>@#@$) t) t :: f b) ~ Apply (Apply TFHelper_6989586621679563872Sym0 t) t => Sing t -> Sing t -> Sing (Apply (Apply (<*>@#@$) t) t :: f b) infixl 4 #

sLiftA2 :: forall a b c (t :: (~>) a ((~>) b c)) (t :: f a) (t :: f b). (Apply (Apply (Apply LiftA2Sym0 t) t) t :: f c) ~ Apply (Apply (Apply LiftA2_6989586621679563890Sym0 t) t) t => Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply LiftA2Sym0 t) t) t :: f c) #

(%*>) :: forall a b (t :: f a) (t :: f b). (Apply (Apply (*>@#@$) t) t :: f b) ~ Apply (Apply TFHelper_6989586621679563903Sym0 t) t => Sing t -> Sing t -> Sing (Apply (Apply (*>@#@$) t) t :: f b) infixl 4 #

(%<*) :: forall a b (t :: f a) (t :: f b). (Apply (Apply (<*@#@$) t) t :: f a) ~ Apply (Apply TFHelper_6989586621679563919Sym0 t) t => Sing t -> Sing t -> Sing (Apply (Apply (<*@#@$) t) t :: f a) infixl 4 #

Instances

SApplicative [] #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sPure :: Sing t -> Sing (Apply PureSym0 t) # (%<>) :: Sing t -> Sing t -> Sing (Apply (Apply (<>@#@$) t) t) # sLiftA2 :: Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply LiftA2Sym0 t) t) t) # (%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) # (%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) #
SApplicative Maybe #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sPure :: Sing t -> Sing (Apply PureSym0 t) # (%<>) :: Sing t -> Sing t -> Sing (Apply (Apply (<>@#@$) t) t) # sLiftA2 :: Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply LiftA2Sym0 t) t) t) # (%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) # (%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) #
SApplicative Min #
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods sPure :: Sing t -> Sing (Apply PureSym0 t) # (%<>) :: Sing t -> Sing t -> Sing (Apply (Apply (<>@#@$) t) t) # sLiftA2 :: Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply LiftA2Sym0 t) t) t) # (%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) # (%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) #
SApplicative Max #
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods sPure :: Sing t -> Sing (Apply PureSym0 t) # (%<>) :: Sing t -> Sing t -> Sing (Apply (Apply (<>@#@$) t) t) # sLiftA2 :: Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply LiftA2Sym0 t) t) t) # (%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) # (%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) #
SApplicative First #
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods sPure :: Sing t -> Sing (Apply PureSym0 t) # (%<>) :: Sing t -> Sing t -> Sing (Apply (Apply (<>@#@$) t) t) # sLiftA2 :: Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply LiftA2Sym0 t) t) t) # (%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) # (%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) #
SApplicative Last #
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods sPure :: Sing t -> Sing (Apply PureSym0 t) # (%<>) :: Sing t -> Sing t -> Sing (Apply (Apply (<>@#@$) t) t) # sLiftA2 :: Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply LiftA2Sym0 t) t) t) # (%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) # (%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) #
SApplicative Option #
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods sPure :: Sing t -> Sing (Apply PureSym0 t) # (%<>) :: Sing t -> Sing t -> Sing (Apply (Apply (<>@#@$) t) t) # sLiftA2 :: Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply LiftA2Sym0 t) t) t) # (%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) # (%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) #
SApplicative Identity #
Instance details Defined in Data.Singletons.Prelude.Identity Methods sPure :: Sing t -> Sing (Apply PureSym0 t) # (%<>) :: Sing t -> Sing t -> Sing (Apply (Apply (<>@#@$) t) t) # sLiftA2 :: Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply LiftA2Sym0 t) t) t) # (%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) # (%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) #
SApplicative First #
Instance details Defined in Data.Singletons.Prelude.Monoid Methods sPure :: Sing t -> Sing (Apply PureSym0 t) # (%<>) :: Sing t -> Sing t -> Sing (Apply (Apply (<>@#@$) t) t) # sLiftA2 :: Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply LiftA2Sym0 t) t) t) # (%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) # (%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) #
SApplicative Last #
Instance details Defined in Data.Singletons.Prelude.Monoid Methods sPure :: Sing t -> Sing (Apply PureSym0 t) # (%<>) :: Sing t -> Sing t -> Sing (Apply (Apply (<>@#@$) t) t) # sLiftA2 :: Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply LiftA2Sym0 t) t) t) # (%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) # (%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) #
SApplicative Dual #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sPure :: Sing t -> Sing (Apply PureSym0 t) # (%<>) :: Sing t -> Sing t -> Sing (Apply (Apply (<>@#@$) t) t) # sLiftA2 :: Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply LiftA2Sym0 t) t) t) # (%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) # (%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) #
SApplicative Sum #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sPure :: Sing t -> Sing (Apply PureSym0 t) # (%<>) :: Sing t -> Sing t -> Sing (Apply (Apply (<>@#@$) t) t) # sLiftA2 :: Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply LiftA2Sym0 t) t) t) # (%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) # (%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) #
SApplicative Product #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sPure :: Sing t -> Sing (Apply PureSym0 t) # (%<>) :: Sing t -> Sing t -> Sing (Apply (Apply (<>@#@$) t) t) # sLiftA2 :: Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply LiftA2Sym0 t) t) t) # (%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) # (%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) #
SApplicative Down #
Instance details Defined in Data.Singletons.Prelude.Applicative Methods sPure :: Sing t -> Sing (Apply PureSym0 t) # (%<>) :: Sing t -> Sing t -> Sing (Apply (Apply (<>@#@$) t) t) # sLiftA2 :: Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply LiftA2Sym0 t) t) t) # (%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) # (%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) #
SApplicative NonEmpty #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sPure :: Sing t -> Sing (Apply PureSym0 t) # (%<>) :: Sing t -> Sing t -> Sing (Apply (Apply (<>@#@$) t) t) # sLiftA2 :: Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply LiftA2Sym0 t) t) t) # (%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) # (%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) #
SApplicative (Either e) #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sPure :: Sing t -> Sing (Apply PureSym0 t) # (%<>) :: Sing t -> Sing t -> Sing (Apply (Apply (<>@#@$) t) t) # sLiftA2 :: Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply LiftA2Sym0 t) t) t) # (%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) # (%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) #
SMonoid a => SApplicative ((,) a) #
Instance details Defined in Data.Singletons.Prelude.Applicative Methods sPure :: Sing t -> Sing (Apply PureSym0 t) # (%<>) :: Sing t -> Sing t -> Sing (Apply (Apply (<>@#@$) t) t) # sLiftA2 :: Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply LiftA2Sym0 t) t) t) # (%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) # (%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) #
SMonoid m => SApplicative (Const m :: Type -> Type) #
Instance details Defined in Data.Singletons.Prelude.Const Methods sPure :: Sing t -> Sing (Apply PureSym0 t) # (%<>) :: Sing t -> Sing t -> Sing (Apply (Apply (<>@#@$) t) t) # sLiftA2 :: Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply LiftA2Sym0 t) t) t) # (%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) # (%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) #

class PApplicative f => PAlternative (f :: Type -> Type) #

Associated Types

type Empty :: f a #

type (arg :: f a) <|> (arg :: f a) :: f a infixl 3 #

Instances

PAlternative [] #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Associated Types type Empty :: f a # type arg <\|> arg :: f a #
PAlternative Maybe #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Associated Types type Empty :: f a # type arg <\|> arg :: f a #
PAlternative Option #
Instance details Defined in Data.Singletons.Prelude.Semigroup Associated Types type Empty :: f a # type arg <\|> arg :: f a #

class SApplicative f => SAlternative (f :: Type -> Type) where #

Methods

sEmpty :: forall a. Sing (EmptySym0 :: f a) #

(%<|>) :: forall a (t :: f a) (t :: f a). Sing t -> Sing t -> Sing (Apply (Apply (<|>@#@$) t) t :: f a) infixl 3 #

Instances

SAlternative [] #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sEmpty :: Sing EmptySym0 # (%<\|>) :: Sing t -> Sing t -> Sing (Apply (Apply (<\|>@#@$) t) t) #
SAlternative Maybe #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sEmpty :: Sing EmptySym0 # (%<\|>) :: Sing t -> Sing t -> Sing (Apply (Apply (<\|>@#@$) t) t) #
SAlternative Option #
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods sEmpty :: Sing EmptySym0 # (%<\|>) :: Sing t -> Sing t -> Sing (Apply (Apply (<\|>@#@$) t) t) #

data family Sing :: k -> Type #

The singleton kind-indexed data family.

Instances

SDecide k => TestCoercion (Sing :: k -> Type) #
Instance details Defined in Data.Singletons.Decide Methods testCoercion :: Sing a -> Sing b -> Maybe (Coercion a b) #
SDecide k => TestEquality (Sing :: k -> Type) #
Instance details Defined in Data.Singletons.Decide Methods testEquality :: Sing a -> Sing b -> Maybe (a :~: b) #
Show (SSymbol s) #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> SSymbol s -> ShowS # show :: SSymbol s -> String # showList :: [SSymbol s] -> ShowS #
Show (SNat n) #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> SNat n -> ShowS # show :: SNat n -> String # showList :: [SNat n] -> ShowS #
Eq (Sing a) #
Instance details Defined in Data.Singletons.TypeRepTYPE Methods (==) :: Sing a -> Sing a -> Bool # (/=) :: Sing a -> Sing a -> Bool #
Ord (Sing a) #
Instance details Defined in Data.Singletons.TypeRepTYPE Methods compare :: Sing a -> Sing a -> Ordering # (<) :: Sing a -> Sing a -> Bool # (<=) :: Sing a -> Sing a -> Bool # (>) :: Sing a -> Sing a -> Bool # (>=) :: Sing a -> Sing a -> Bool # max :: Sing a -> Sing a -> Sing a # min :: Sing a -> Sing a -> Sing a #
Show (Sing z) #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
(ShowSing a, ShowSing [a]) => Show (Sing z) #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
ShowSing a => Show (Sing z) #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
Show (Sing z) #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
(ShowSing a, ShowSing b) => Show (Sing z) #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
Show (Sing a) #
Instance details Defined in Data.Singletons.TypeRepTYPE Methods showsPrec :: Int -> Sing a -> ShowS # show :: Sing a -> String # showList :: [Sing a] -> ShowS #
Show (Sing z) #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
(ShowSing a, ShowSing b) => Show (Sing z) #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
(ShowSing a, ShowSing b, ShowSing c) => Show (Sing z) #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
(ShowSing a, ShowSing b, ShowSing c, ShowSing d) => Show (Sing z) #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
(ShowSing a, ShowSing b, ShowSing c, ShowSing d, ShowSing e) => Show (Sing z) #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
(ShowSing a, ShowSing b, ShowSing c, ShowSing d, ShowSing e, ShowSing f) => Show (Sing z) #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
(ShowSing a, ShowSing b, ShowSing c, ShowSing d, ShowSing e, ShowSing f, ShowSing g) => Show (Sing z) #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
Show (Sing z) #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
ShowSing a => Show (Sing z) #
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
ShowSing a => Show (Sing z) #
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
(ShowSing a, ShowSing b) => Show (Sing z) #
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
ShowSing a => Show (Sing z) #
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
ShowSing a => Show (Sing z) #
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
ShowSing m => Show (Sing z) #
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
ShowSing (Maybe a) => Show (Sing z) #
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
ShowSing a => Show (Sing z) #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
ShowSing (Maybe a) => Show (Sing z) #
Instance details Defined in Data.Singletons.Prelude.Monoid Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
ShowSing (Maybe a) => Show (Sing z) #
Instance details Defined in Data.Singletons.Prelude.Monoid Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
ShowSing a => Show (Sing z) #
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
ShowSing Bool => Show (Sing z) #
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
ShowSing Bool => Show (Sing z) #
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
ShowSing a => Show (Sing z) #
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
ShowSing a => Show (Sing z) #
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
(ShowSing a, ShowSing [a]) => Show (Sing z) #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
data Sing (a :: Bool) #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (a :: Bool) where SFalse :: forall (a :: Bool). Sing False STrue :: forall (a :: Bool). Sing True
data Sing (a :: Ordering) #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (a :: Ordering) where SLT :: forall (a :: Ordering). Sing LT SEQ :: forall (a :: Ordering). Sing EQ SGT :: forall (a :: Ordering). Sing GT
data Sing (n :: Nat) #
Instance details Defined in Data.Singletons.TypeLits.Internal data Sing (n :: Nat) where SNat :: forall (n :: Nat). KnownNat n => Sing n
data Sing (n :: Symbol) #
Instance details Defined in Data.Singletons.TypeLits.Internal data Sing (n :: Symbol) where SSym :: forall (n :: Symbol). KnownSymbol n => Sing n
data Sing (a :: ()) #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (a :: ()) where STuple0 :: forall (a :: ()). Sing ()
data Sing (a :: Void) #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (a :: Void)
data Sing (a :: All) #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (a :: All) where SAll :: forall (a :: All) (n :: Bool). {..} -> Sing (All n)
data Sing (a :: Any) #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (a :: Any) where SAny :: forall (a :: Any) (n :: Bool). {..} -> Sing (Any n)
data Sing (a :: PErrorMessage) #
Instance details Defined in Data.Singletons.TypeError data Sing (a :: PErrorMessage) where SText :: forall (a :: PErrorMessage) (t :: Symbol). Sing t -> Sing (Text t) SShowType :: forall (a :: PErrorMessage) t (ty :: t). Sing ty -> Sing (ShowType ty :: ErrorMessage' Symbol) (:%<>:) :: forall (a :: PErrorMessage) (e1 :: ErrorMessage' Symbol) (e2 :: ErrorMessage' Symbol). Sing e1 -> Sing e2 -> Sing (e1 :<>: e2) (:%$$:) :: forall (a :: PErrorMessage) (e1 :: ErrorMessage' Symbol) (e2 :: ErrorMessage' Symbol). Sing e1 -> Sing e2 -> Sing (e1 :$$: e2)
data Sing (b :: [a]) #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (b :: [a]) where SNil :: forall k (b :: [k]). Sing ([] :: [k]) SCons :: forall a (b :: [a]) (n :: a) (n :: [a]). Sing n -> Sing n -> Sing (n ': n)
data Sing (b :: Maybe a) #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (b :: Maybe a) where SNothing :: forall a (b :: Maybe a). Sing (Nothing :: Maybe a) SJust :: forall a (b :: Maybe a) (n :: a). Sing n -> Sing (Just n)
newtype Sing (a :: TYPE rep) #	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 -> Type` 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.
Instance details Defined in Data.Singletons.TypeRepTYPE newtype Sing (a :: TYPE rep) = STypeRep (TypeRep a)
data Sing (b :: Min a) #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (b :: Min a) where SMin :: forall a (b :: Min a) (n :: a). {..} -> Sing (Min n)
data Sing (b :: Max a) #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (b :: Max a) where SMax :: forall a (b :: Max a) (n :: a). {..} -> Sing (Max n)
data Sing (b :: First a) #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (b :: First a) where SFirst :: forall a (b :: First a) (n :: a). {..} -> Sing (First n)
data Sing (b :: Last a) #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (b :: Last a) where SLast :: forall a (b :: Last a) (n :: a). {..} -> Sing (Last n)
data Sing (a :: WrappedMonoid m) #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (a :: WrappedMonoid m) where SWrapMonoid :: forall m (a :: WrappedMonoid m) (n :: m). {..} -> Sing (WrapMonoid n)
data Sing (b :: Option a) #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (b :: Option a) where SOption :: forall a (b :: Option a) (n :: Maybe a). {..} -> Sing (Option n)
data Sing (b :: Identity a) #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (b :: Identity a) where SIdentity :: forall a (b :: Identity a) (n :: a). {..} -> Sing (Identity n)
data Sing (b :: First a) #
Instance details Defined in Data.Singletons.Prelude.Monoid data Sing (b :: First a) where SFirst :: forall a (b :: First a) (n :: Maybe a). {..} -> Sing (First n)
data Sing (b :: Last a) #
Instance details Defined in Data.Singletons.Prelude.Monoid data Sing (b :: Last a) where SLast :: forall a (b :: Last a) (n :: Maybe a). {..} -> Sing (Last n)
data Sing (b :: Dual a) #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (b :: Dual a) where SDual :: forall a (b :: Dual a) (n :: a). {..} -> Sing (Dual n)
data Sing (b :: Sum a) #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (b :: Sum a) where SSum :: forall a (b :: Sum a) (n :: a). {..} -> Sing (Sum n)
data Sing (b :: Product a) #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (b :: Product a) where SProduct :: forall a (b :: Product a) (n :: a). {..} -> Sing (Product n)
data Sing (b :: Down a) #
Instance details Defined in Data.Singletons.Prelude.Ord data Sing (b :: Down a) where SDown :: forall a (b :: Down a) (n :: a). Sing n -> Sing (Down n)
data Sing (b :: NonEmpty a) #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (b :: NonEmpty a) where (:%\|) :: forall a (b :: NonEmpty a) (n :: a) (n :: [a]). Sing n -> Sing n -> Sing (n :\| n)
data Sing (c :: Either a b) #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (c :: Either a b) where SLeft :: forall a b (c :: Either a b) (n :: a). Sing n -> Sing (Left n :: Either a b) SRight :: forall a b (c :: Either a b) (n :: b). Sing n -> Sing (Right n :: Either a b)
data Sing (c :: (a, b)) #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (c :: (a, b)) where STuple2 :: forall a b (c :: (a, b)) (n :: a) (n :: b). Sing n -> Sing n -> Sing ((,) n n)
data Sing (c :: Arg a b) #
Instance details Defined in Data.Singletons.Prelude.Semigroup data Sing (c :: Arg a b) where SArg :: forall a b (c :: Arg a b) (n :: a) (n :: b). Sing n -> Sing n -> Sing (Arg n n)
newtype Sing (f :: k1 ~> k2) #
Instance details Defined in Data.Singletons.Internal newtype Sing (f :: k1 ~> k2) = SLambda { applySing :: forall (t :: k1). Sing t -> Sing (f @@ t) }
data Sing (d :: (a, b, c)) #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (d :: (a, b, c)) where STuple3 :: forall a b c (d :: (a, b, c)) (n :: a) (n :: b) (n :: c). Sing n -> Sing n -> Sing n -> Sing ((,,) n n n)
data Sing (c :: Const a b) #
Instance details Defined in Data.Singletons.Prelude.Const data Sing (c :: Const a b) where SConst :: forall k a (b :: k) (c :: Const a b) (a :: a). {..} -> Sing (Const a :: Const a b)
data Sing (e :: (a, b, c, d)) #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (e :: (a, b, c, d)) where STuple4 :: forall a b c d (e :: (a, b, c, d)) (n :: a) (n :: b) (n :: c) (n :: d). Sing n -> Sing n -> Sing n -> Sing n -> Sing ((,,,) n n n n)
data Sing (f :: (a, b, c, d, e)) #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (f :: (a, b, c, d, e)) where STuple5 :: forall a b c d e (f :: (a, b, c, d, e)) (n :: a) (n :: b) (n :: c) (n :: d) (n :: e). Sing n -> Sing n -> Sing n -> Sing n -> Sing n -> Sing ((,,,,) n n n n n)
data Sing (g :: (a, b, c, d, e, f)) #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (g :: (a, b, c, d, e, f)) where STuple6 :: forall a b c d e f (g :: (a, b, c, d, e, f)) (n :: a) (n :: b) (n :: c) (n :: d) (n :: e) (n :: f). Sing n -> Sing n -> Sing n -> Sing n -> Sing n -> Sing n -> Sing ((,,,,,) n n n n n n)
data Sing (h :: (a, b, c, d, e, f, g)) #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (h :: (a, b, c, d, e, f, g)) where STuple7 :: forall a b c d e f g (h :: (a, b, c, d, e, f, g)) (n :: a) (n :: b) (n :: c) (n :: d) (n :: e) (n :: f) (n :: g). Sing n -> Sing n -> Sing n -> Sing n -> Sing n -> Sing n -> Sing n -> Sing ((,,,,,,) n n n n n n n)

type SConst = (Sing :: Const a b -> Type) #

data Const a (b :: k) :: forall k. Type -> k -> Type #

The Const functor.

Instances

Generic1 (Const a :: k -> Type)
Instance details Defined in Data.Functor.Const Associated Types type Rep1 (Const a) :: k -> Type # Methods from1 :: Const a a0 -> Rep1 (Const a) a0 # to1 :: Rep1 (Const a) a0 -> Const a a0 #
Bifunctor (Const :: Type -> Type -> Type)	Since: base-4.8.0.0
Instance details Defined in Data.Bifunctor Methods bimap :: (a -> b) -> (c -> d) -> Const a c -> Const b d # first :: (a -> b) -> Const a c -> Const b c # second :: (b -> c) -> Const a b -> Const a c #
Eq2 (Const :: Type -> Type -> Type)	Since: base-4.9.0.0
Instance details Defined in Data.Functor.Classes Methods liftEq2 :: (a -> b -> Bool) -> (c -> d -> Bool) -> Const a c -> Const b d -> Bool #
Ord2 (Const :: Type -> Type -> Type)	Since: base-4.9.0.0
Instance details Defined in Data.Functor.Classes Methods liftCompare2 :: (a -> b -> Ordering) -> (c -> d -> Ordering) -> Const a c -> Const b d -> Ordering #
Read2 (Const :: Type -> Type -> Type)	Since: base-4.9.0.0
Instance details Defined in Data.Functor.Classes Methods liftReadsPrec2 :: (Int -> ReadS a) -> ReadS [a] -> (Int -> ReadS b) -> ReadS [b] -> Int -> ReadS (Const a b) # liftReadList2 :: (Int -> ReadS a) -> ReadS [a] -> (Int -> ReadS b) -> ReadS [b] -> ReadS [Const a b] # liftReadPrec2 :: ReadPrec a -> ReadPrec [a] -> ReadPrec b -> ReadPrec [b] -> ReadPrec (Const a b) # liftReadListPrec2 :: ReadPrec a -> ReadPrec [a] -> ReadPrec b -> ReadPrec [b] -> ReadPrec [Const a b] #
Show2 (Const :: Type -> Type -> Type)	Since: base-4.9.0.0
Instance details Defined in Data.Functor.Classes Methods liftShowsPrec2 :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> (Int -> b -> ShowS) -> ([b] -> ShowS) -> Int -> Const a b -> ShowS # liftShowList2 :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> (Int -> b -> ShowS) -> ([b] -> ShowS) -> [Const a b] -> ShowS #
Functor (Const m :: Type -> Type)	Since: base-2.1
Instance details Defined in Data.Functor.Const Methods fmap :: (a -> b) -> Const m a -> Const m b # (<$) :: a -> Const m b -> Const m a #
Monoid m => Applicative (Const m :: Type -> Type)	Since: base-2.0.1
Instance details Defined in Data.Functor.Const Methods pure :: a -> Const m a # (<>) :: Const m (a -> b) -> Const m a -> Const m b # liftA2 :: (a -> b -> c) -> Const m a -> Const m b -> Const m c # (>) :: Const m a -> Const m b -> Const m b # (<*) :: Const m a -> Const m b -> Const m a #
Foldable (Const m :: Type -> Type)	Since: base-4.7.0.0
Instance details Defined in Data.Functor.Const Methods fold :: Monoid m0 => Const m m0 -> m0 # foldMap :: Monoid m0 => (a -> m0) -> Const m a -> m0 # foldr :: (a -> b -> b) -> b -> Const m a -> b # foldr' :: (a -> b -> b) -> b -> Const m a -> b # foldl :: (b -> a -> b) -> b -> Const m a -> b # foldl' :: (b -> a -> b) -> b -> Const m a -> b # foldr1 :: (a -> a -> a) -> Const m a -> a # foldl1 :: (a -> a -> a) -> Const m a -> a # toList :: Const m a -> [a] # null :: Const m a -> Bool # length :: Const m a -> Int # elem :: Eq a => a -> Const m a -> Bool # maximum :: Ord a => Const m a -> a # minimum :: Ord a => Const m a -> a # sum :: Num a => Const m a -> a # product :: Num a => Const m a -> a #
Traversable (Const m :: Type -> Type)	Since: base-4.7.0.0
Instance details Defined in Data.Traversable Methods traverse :: Applicative f => (a -> f b) -> Const m a -> f (Const m b) # sequenceA :: Applicative f => Const m (f a) -> f (Const m a) # mapM :: Monad m0 => (a -> m0 b) -> Const m a -> m0 (Const m b) # sequence :: Monad m0 => Const m (m0 a) -> m0 (Const m a) #
Eq a => Eq1 (Const a :: Type -> Type)	Since: base-4.9.0.0
Instance details Defined in Data.Functor.Classes Methods liftEq :: (a0 -> b -> Bool) -> Const a a0 -> Const a b -> Bool #
Ord a => Ord1 (Const a :: Type -> Type)	Since: base-4.9.0.0
Instance details Defined in Data.Functor.Classes Methods liftCompare :: (a0 -> b -> Ordering) -> Const a a0 -> Const a b -> Ordering #
Read a => Read1 (Const a :: Type -> Type)	Since: base-4.9.0.0
Instance details Defined in Data.Functor.Classes Methods liftReadsPrec :: (Int -> ReadS a0) -> ReadS [a0] -> Int -> ReadS (Const a a0) # liftReadList :: (Int -> ReadS a0) -> ReadS [a0] -> ReadS [Const a a0] # liftReadPrec :: ReadPrec a0 -> ReadPrec [a0] -> ReadPrec (Const a a0) # liftReadListPrec :: ReadPrec a0 -> ReadPrec [a0] -> ReadPrec [Const a a0] #
Show a => Show1 (Const a :: Type -> Type)	Since: base-4.9.0.0
Instance details Defined in Data.Functor.Classes Methods liftShowsPrec :: (Int -> a0 -> ShowS) -> ([a0] -> ShowS) -> Int -> Const a a0 -> ShowS # liftShowList :: (Int -> a0 -> ShowS) -> ([a0] -> ShowS) -> [Const a a0] -> ShowS #
SMonoid m => SApplicative (Const m :: Type -> Type) #
Instance details Defined in Data.Singletons.Prelude.Const Methods sPure :: Sing t -> Sing (Apply PureSym0 t) # (%<>) :: Sing t -> Sing t -> Sing (Apply (Apply (<>@#@$) t) t) # sLiftA2 :: Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply LiftA2Sym0 t) t) t) # (%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) # (%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) #
SFunctor (Const m :: Type -> Type) #
Instance details Defined in Data.Singletons.Prelude.Const Methods sFmap :: Sing t -> Sing t -> Sing (Apply (Apply FmapSym0 t) t) # (%<$) :: Sing t -> Sing t -> Sing (Apply (Apply (<$@#@$) t) t) #
PApplicative (Const m :: Type -> Type) #
Instance details Defined in Data.Singletons.Prelude.Const Associated Types type Pure arg :: f a # type arg <> arg :: f b # type LiftA2 arg arg arg :: f c # type arg > arg :: f b # type arg <* arg :: f a #
PFunctor (Const m :: Type -> Type) #
Instance details Defined in Data.Singletons.Prelude.Const Associated Types type Fmap arg arg :: f b # type arg <$ arg :: f a #
SFoldable (Const m :: Type -> Type) #
Instance details Defined in Data.Singletons.Prelude.Const Methods sFold :: SMonoid m0 => Sing t -> Sing (Apply FoldSym0 t) # sFoldMap :: SMonoid m0 => Sing t -> Sing t -> Sing (Apply (Apply FoldMapSym0 t) t) # sFoldr :: Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply FoldrSym0 t) t) t) # sFoldr' :: Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply Foldr'Sym0 t) t) t) # sFoldl :: Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply FoldlSym0 t) t) t) # sFoldl' :: Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply Foldl'Sym0 t) t) t) # sFoldr1 :: Sing t -> Sing t -> Sing (Apply (Apply Foldr1Sym0 t) t) # sFoldl1 :: Sing t -> Sing t -> Sing (Apply (Apply Foldl1Sym0 t) t) # sToList :: Sing t -> Sing (Apply ToListSym0 t) # sNull :: Sing t -> Sing (Apply NullSym0 t) # sLength :: Sing t -> Sing (Apply LengthSym0 t) # sElem :: SEq a => Sing t -> Sing t -> Sing (Apply (Apply ElemSym0 t) t) # sMaximum :: SOrd a => Sing t -> Sing (Apply MaximumSym0 t) # sMinimum :: SOrd a => Sing t -> Sing (Apply MinimumSym0 t) # sSum :: SNum a => Sing t -> Sing (Apply SumSym0 t) # sProduct :: SNum a => Sing t -> Sing (Apply ProductSym0 t) #
PFoldable (Const m :: Type -> Type) #
Instance details Defined in Data.Singletons.Prelude.Const Associated Types type Fold arg :: m # type FoldMap arg arg :: m # type Foldr arg arg arg :: b # type Foldr' arg arg arg :: b # type Foldl arg arg arg :: b # type Foldl' arg arg arg :: b # type Foldr1 arg arg :: a # type Foldl1 arg arg :: a # type ToList arg :: [a] # type Null arg :: Bool # type Length arg :: Nat # type Elem arg arg :: Bool # type Maximum arg :: a # type Minimum arg :: a # type Sum arg :: a # type Product arg :: a #
STraversable (Const m :: Type -> Type) #
Instance details Defined in Data.Singletons.Prelude.Traversable Methods sTraverse :: SApplicative f => Sing t -> Sing t -> Sing (Apply (Apply TraverseSym0 t) t) # sSequenceA :: SApplicative f => Sing t -> Sing (Apply SequenceASym0 t) # sMapM :: SMonad m0 => Sing t -> Sing t -> Sing (Apply (Apply MapMSym0 t) t) # sSequence :: SMonad m0 => Sing t -> Sing (Apply SequenceSym0 t) #
PTraversable (Const m :: Type -> Type) #
Instance details Defined in Data.Singletons.Prelude.Traversable Associated Types type Traverse arg arg :: f (t b) # type SequenceA arg :: f (t a) # type MapM arg arg :: m (t b) # type Sequence arg :: m (t a) #
SingI (TyCon1 (Const :: k1 -> Const k1 b) :: k1 ~> Const k1 b) #
Instance details Defined in Data.Singletons.Prelude.Const Methods sing :: Sing (TyCon1 Const0) #
SingI (ConstSym0 :: TyFun a6989586621679093209 (Const a6989586621679093209 b6989586621679093210) -> Type) #
Instance details Defined in Data.Singletons.Prelude.Const Methods sing :: Sing ConstSym0 #
SuppressUnusedWarnings (ConstSym0 :: TyFun a6989586621679093209 (Const a6989586621679093209 b6989586621679093210) -> Type) #
Instance details Defined in Data.Singletons.Prelude.Const Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (GetConstSym0 :: TyFun (Const a6989586621680750730 b6989586621680750731) a6989586621680750730 -> Type) #
Instance details Defined in Data.Singletons.Prelude.Const Methods suppressUnusedWarnings :: () #
Bounded a => Bounded (Const a b)	Since: base-4.9.0.0
Instance details Defined in Data.Functor.Const Methods minBound :: Const a b # maxBound :: Const a b #
Enum a => Enum (Const a b)	Since: base-4.9.0.0
Instance details Defined in Data.Functor.Const Methods succ :: Const a b -> Const a b # pred :: Const a b -> Const a b # toEnum :: Int -> Const a b # fromEnum :: Const a b -> Int # enumFrom :: Const a b -> [Const a b] # enumFromThen :: Const a b -> Const a b -> [Const a b] # enumFromTo :: Const a b -> Const a b -> [Const a b] # enumFromThenTo :: Const a b -> Const a b -> Const a b -> [Const a b] #
Eq a => Eq (Const a b)	Since: base-4.9.0.0
Instance details Defined in Data.Functor.Const Methods (==) :: Const a b -> Const a b -> Bool # (/=) :: Const a b -> Const a b -> Bool #
Floating a => Floating (Const a b)	Since: base-4.9.0.0
Instance details Defined in Data.Functor.Const Methods pi :: Const a b # exp :: Const a b -> Const a b # log :: Const a b -> Const a b # sqrt :: Const a b -> Const a b # (**) :: Const a b -> Const a b -> Const a b # logBase :: Const a b -> Const a b -> Const a b # sin :: Const a b -> Const a b # cos :: Const a b -> Const a b # tan :: Const a b -> Const a b # asin :: Const a b -> Const a b # acos :: Const a b -> Const a b # atan :: Const a b -> Const a b # sinh :: Const a b -> Const a b # cosh :: Const a b -> Const a b # tanh :: Const a b -> Const a b # asinh :: Const a b -> Const a b # acosh :: Const a b -> Const a b # atanh :: Const a b -> Const a b # log1p :: Const a b -> Const a b # expm1 :: Const a b -> Const a b # log1pexp :: Const a b -> Const a b # log1mexp :: Const a b -> Const a b #
Fractional a => Fractional (Const a b)	Since: base-4.9.0.0
Instance details Defined in Data.Functor.Const Methods (/) :: Const a b -> Const a b -> Const a b # recip :: Const a b -> Const a b # fromRational :: Rational -> Const a b #
Integral a => Integral (Const a b)	Since: base-4.9.0.0
Instance details Defined in Data.Functor.Const Methods quot :: Const a b -> Const a b -> Const a b # rem :: Const a b -> Const a b -> Const a b # div :: Const a b -> Const a b -> Const a b # mod :: Const a b -> Const a b -> Const a b # quotRem :: Const a b -> Const a b -> (Const a b, Const a b) # divMod :: Const a b -> Const a b -> (Const a b, Const a b) # toInteger :: Const a b -> Integer #
(Typeable k, Data a, Typeable b) => Data (Const a b)	Since: base-4.10.0.0
Instance details Defined in Data.Data Methods gfoldl :: (forall d b0. Data d => c (d -> b0) -> d -> c b0) -> (forall g. g -> c g) -> Const a b -> c (Const a b) # gunfold :: (forall b0 r. Data b0 => c (b0 -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Const a b) # toConstr :: Const a b -> Constr # dataTypeOf :: Const a b -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Const a b)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Const a b)) # gmapT :: (forall b0. Data b0 => b0 -> b0) -> Const a b -> Const a b # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Const a b -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Const a b -> r # gmapQ :: (forall d. Data d => d -> u) -> Const a b -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Const a b -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Const a b -> m (Const a b) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Const a b -> m (Const a b) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Const a b -> m (Const a b) #
Num a => Num (Const a b)	Since: base-4.9.0.0
Instance details Defined in Data.Functor.Const Methods (+) :: Const a b -> Const a b -> Const a b # (-) :: Const a b -> Const a b -> Const a b # (*) :: Const a b -> Const a b -> Const a b # negate :: Const a b -> Const a b # abs :: Const a b -> Const a b # signum :: Const a b -> Const a b # fromInteger :: Integer -> Const a b #
Ord a => Ord (Const a b)	Since: base-4.9.0.0
Instance details Defined in Data.Functor.Const Methods compare :: Const a b -> Const a b -> Ordering # (<) :: Const a b -> Const a b -> Bool # (<=) :: Const a b -> Const a b -> Bool # (>) :: Const a b -> Const a b -> Bool # (>=) :: Const a b -> Const a b -> Bool # max :: Const a b -> Const a b -> Const a b # min :: Const a b -> Const a b -> Const a b #
Read a => Read (Const a b)	This instance would be equivalent to the derived instances of the `Const` newtype if the `runConst` field were removed Since: base-4.8.0.0
Instance details Defined in Data.Functor.Const Methods readsPrec :: Int -> ReadS (Const a b) # readList :: ReadS [Const a b] # readPrec :: ReadPrec (Const a b) # readListPrec :: ReadPrec [Const a b] #
Real a => Real (Const a b)	Since: base-4.9.0.0
Instance details Defined in Data.Functor.Const Methods toRational :: Const a b -> Rational #
RealFloat a => RealFloat (Const a b)	Since: base-4.9.0.0
Instance details Defined in Data.Functor.Const Methods floatRadix :: Const a b -> Integer # floatDigits :: Const a b -> Int # floatRange :: Const a b -> (Int, Int) # decodeFloat :: Const a b -> (Integer, Int) # encodeFloat :: Integer -> Int -> Const a b # exponent :: Const a b -> Int # significand :: Const a b -> Const a b # scaleFloat :: Int -> Const a b -> Const a b # isNaN :: Const a b -> Bool # isInfinite :: Const a b -> Bool # isDenormalized :: Const a b -> Bool # isNegativeZero :: Const a b -> Bool # isIEEE :: Const a b -> Bool # atan2 :: Const a b -> Const a b -> Const a b #
RealFrac a => RealFrac (Const a b)	Since: base-4.9.0.0
Instance details Defined in Data.Functor.Const Methods properFraction :: Integral b0 => Const a b -> (b0, Const a b) # truncate :: Integral b0 => Const a b -> b0 # round :: Integral b0 => Const a b -> b0 # ceiling :: Integral b0 => Const a b -> b0 # floor :: Integral b0 => Const a b -> b0 #
Show a => Show (Const a b)	This instance would be equivalent to the derived instances of the `Const` newtype if the `runConst` field were removed Since: base-4.8.0.0
Instance details Defined in Data.Functor.Const Methods showsPrec :: Int -> Const a b -> ShowS # show :: Const a b -> String # showList :: [Const a b] -> ShowS #
Ix a => Ix (Const a b)	Since: base-4.9.0.0
Instance details Defined in Data.Functor.Const Methods range :: (Const a b, Const a b) -> [Const a b] # index :: (Const a b, Const a b) -> Const a b -> Int # unsafeIndex :: (Const a b, Const a b) -> Const a b -> Int inRange :: (Const a b, Const a b) -> Const a b -> Bool # rangeSize :: (Const a b, Const a b) -> Int # unsafeRangeSize :: (Const a b, Const a b) -> Int
IsString a => IsString (Const a b)	Since: base-4.9.0.0
Instance details Defined in Data.String Methods fromString :: String -> Const a b #
Generic (Const a b)
Instance details Defined in Data.Functor.Const Associated Types type Rep (Const a b) :: Type -> Type # Methods from :: Const a b -> Rep (Const a b) x # to :: Rep (Const a b) x -> Const a b #
Semigroup a => Semigroup (Const a b)	Since: base-4.9.0.0
Instance details Defined in Data.Functor.Const Methods (<>) :: Const a b -> Const a b -> Const a b # sconcat :: NonEmpty (Const a b) -> Const a b # stimes :: Integral b0 => b0 -> Const a b -> Const a b #
Monoid a => Monoid (Const a b)	Since: base-4.9.0.0
Instance details Defined in Data.Functor.Const Methods mempty :: Const a b # mappend :: Const a b -> Const a b -> Const a b # mconcat :: [Const a b] -> Const a b #
Storable a => Storable (Const a b)	Since: base-4.9.0.0
Instance details Defined in Data.Functor.Const Methods sizeOf :: Const a b -> Int # alignment :: Const a b -> Int # peekElemOff :: Ptr (Const a b) -> Int -> IO (Const a b) # pokeElemOff :: Ptr (Const a b) -> Int -> Const a b -> IO () # peekByteOff :: Ptr b0 -> Int -> IO (Const a b) # pokeByteOff :: Ptr b0 -> Int -> Const a b -> IO () # peek :: Ptr (Const a b) -> IO (Const a b) # poke :: Ptr (Const a b) -> Const a b -> IO () #
Bits a => Bits (Const a b)	Since: base-4.9.0.0
Instance details Defined in Data.Functor.Const Methods (.&.) :: Const a b -> Const a b -> Const a b # (.\|.) :: Const a b -> Const a b -> Const a b # xor :: Const a b -> Const a b -> Const a b # complement :: Const a b -> Const a b # shift :: Const a b -> Int -> Const a b # rotate :: Const a b -> Int -> Const a b # zeroBits :: Const a b # bit :: Int -> Const a b # setBit :: Const a b -> Int -> Const a b # clearBit :: Const a b -> Int -> Const a b # complementBit :: Const a b -> Int -> Const a b # testBit :: Const a b -> Int -> Bool # bitSizeMaybe :: Const a b -> Maybe Int # bitSize :: Const a b -> Int # isSigned :: Const a b -> Bool # shiftL :: Const a b -> Int -> Const a b # unsafeShiftL :: Const a b -> Int -> Const a b # shiftR :: Const a b -> Int -> Const a b # unsafeShiftR :: Const a b -> Int -> Const a b # rotateL :: Const a b -> Int -> Const a b # rotateR :: Const a b -> Int -> Const a b # popCount :: Const a b -> Int #
FiniteBits a => FiniteBits (Const a b)	Since: base-4.9.0.0
Instance details Defined in Data.Functor.Const Methods finiteBitSize :: Const a b -> Int # countLeadingZeros :: Const a b -> Int # countTrailingZeros :: Const a b -> Int #
SingKind a => SingKind (Const a b) #
Instance details Defined in Data.Singletons.Prelude.Const Associated Types type Demote (Const a b) = (r :: Type) # Methods fromSing :: Sing a0 -> Demote (Const a b) # toSing :: Demote (Const a b) -> SomeSing (Const a b) #
SDecide a => SDecide (Const a b) #
Instance details Defined in Data.Singletons.Prelude.Const Methods (%~) :: Sing a0 -> Sing b0 -> Decision (a0 :~: b0) #
PEq (Const a b) #
Instance details Defined in Data.Singletons.Prelude.Const Associated Types type x == y :: Bool # type x /= y :: Bool #
SEq a => SEq (Const a b) #
Instance details Defined in Data.Singletons.Prelude.Const Methods (%==) :: Sing a0 -> Sing b0 -> Sing (a0 == b0) # (%/=) :: Sing a0 -> Sing b0 -> Sing (a0 /= b0) #
SOrd a => SOrd (Const a b) #
Instance details Defined in Data.Singletons.Prelude.Const Methods sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) # (%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) # (%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) # (%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) # (%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) # sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) # sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) #
POrd (Const a b) #
Instance details Defined in Data.Singletons.Prelude.Const Associated Types type Compare arg arg :: Ordering # type arg < arg :: Bool # type arg <= arg :: Bool # type arg > arg :: Bool # type arg >= arg :: Bool # type Max arg arg :: a # type Min arg arg :: a #
SNum a => SNum (Const a b) #
Instance details Defined in Data.Singletons.Prelude.Const Methods (%+) :: Sing t -> Sing t -> Sing (Apply (Apply (+@#@$) t) t) # (%-) :: Sing t -> Sing t -> Sing (Apply (Apply (-@#@$) t) t) # (%) :: Sing t -> Sing t -> Sing (Apply (Apply (@#@$) t) t) # sNegate :: Sing t -> Sing (Apply NegateSym0 t) # sAbs :: Sing t -> Sing (Apply AbsSym0 t) # sSignum :: Sing t -> Sing (Apply SignumSym0 t) # sFromInteger :: Sing t -> Sing (Apply FromIntegerSym0 t) #
PNum (Const a b) #
Instance details Defined in Data.Singletons.Prelude.Const Associated Types type arg + arg :: a # type arg - arg :: a # type arg * arg :: a # type Negate arg :: a # type Abs arg :: a # type Signum arg :: a # type FromInteger arg :: a #
SBounded a => SBounded (Const a b) #
Instance details Defined in Data.Singletons.Prelude.Const Methods sMinBound :: Sing MinBoundSym0 # sMaxBound :: Sing MaxBoundSym0 #
PBounded (Const a b) #
Instance details Defined in Data.Singletons.Prelude.Const Associated Types type MinBound :: a # type MaxBound :: a #
SEnum a => SEnum (Const a b) #
Instance details Defined in Data.Singletons.Prelude.Const Methods sSucc :: Sing t -> Sing (Apply SuccSym0 t) # sPred :: Sing t -> Sing (Apply PredSym0 t) # sToEnum :: Sing t -> Sing (Apply ToEnumSym0 t) # sFromEnum :: Sing t -> Sing (Apply FromEnumSym0 t) # sEnumFromTo :: Sing t -> Sing t -> Sing (Apply (Apply EnumFromToSym0 t) t) # sEnumFromThenTo :: Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply EnumFromThenToSym0 t) t) t) #
PEnum (Const a b) #
Instance details Defined in Data.Singletons.Prelude.Const Associated Types type Succ arg :: a # type Pred arg :: a # type ToEnum arg :: a # type FromEnum arg :: Nat # type EnumFromTo arg arg :: [a] # type EnumFromThenTo arg arg arg :: [a] #
SSemigroup a => SSemigroup (Const a b) #
Instance details Defined in Data.Singletons.Prelude.Const Methods (%<>) :: Sing t -> Sing t -> Sing (Apply (Apply (<>@#@$) t) t) # sSconcat :: Sing t -> Sing (Apply SconcatSym0 t) #
PSemigroup (Const a b) #
Instance details Defined in Data.Singletons.Prelude.Const Associated Types type arg <> arg :: a # type Sconcat arg :: a #
SShow a => SShow (Const a b) #
Instance details Defined in Data.Singletons.Prelude.Const Methods sShowsPrec :: Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply ShowsPrecSym0 t) t) t) # sShow_ :: Sing t -> Sing (Apply Show_Sym0 t) # sShowList :: Sing t -> Sing t -> Sing (Apply (Apply ShowListSym0 t) t) #
PShow (Const a b) #
Instance details Defined in Data.Singletons.Prelude.Const Associated Types type ShowsPrec arg arg arg :: Symbol # type Show_ arg :: Symbol # type ShowList arg arg :: Symbol #
SMonoid a => SMonoid (Const a b) #
Instance details Defined in Data.Singletons.Prelude.Const Methods sMempty :: Sing MemptySym0 # sMappend :: Sing t -> Sing t -> Sing (Apply (Apply MappendSym0 t) t) # sMconcat :: Sing t -> Sing (Apply MconcatSym0 t) #
PMonoid (Const a b) #
Instance details Defined in Data.Singletons.Prelude.Const Associated Types type Mempty :: a # type Mappend arg arg :: a # type Mconcat arg :: a #
SIsString a => SIsString (Const a b) #
Instance details Defined in Data.Singletons.Prelude.IsString Methods sFromString :: Sing t -> Sing (Apply FromStringSym0 t) #
PIsString (Const a b) #
Instance details Defined in Data.Singletons.Prelude.IsString Associated Types type FromString arg :: a #
SingI a2 => SingI (Const a2 :: Const a1 b) #
Instance details Defined in Data.Singletons.Prelude.Const Methods sing :: Sing (Const0 a2) #
type Rep1 (Const a :: k -> Type)	Since: base-4.9.0.0
Instance details Defined in Data.Functor.Const type Rep1 (Const a :: k -> Type) = D1 (MetaData "Const" "Data.Functor.Const" "base" True) (C1 (MetaCons "Const" PrefixI True) (S1 (MetaSel (Just "getConst") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a)))
type Apply (GetConstSym0 :: TyFun (Const a b) a -> Type) (x6989586621680750732 :: Const a b) #
Instance details Defined in Data.Singletons.Prelude.Const type Apply (GetConstSym0 :: TyFun (Const a b) a -> Type) (x6989586621680750732 :: Const a b) = GetConst x6989586621680750732
type Pure (a :: k1) #
Instance details Defined in Data.Singletons.Prelude.Const type Pure (a :: k1)
type Fold (arg :: Const m1 m2) #
Instance details Defined in Data.Singletons.Prelude.Const type Fold (arg :: Const m1 m2)
type ToList (arg :: Const m a) #
Instance details Defined in Data.Singletons.Prelude.Const type ToList (arg :: Const m a)
type Null (arg :: Const m a) #
Instance details Defined in Data.Singletons.Prelude.Const type Null (arg :: Const m a)
type Length (arg :: Const m a) #
Instance details Defined in Data.Singletons.Prelude.Const type Length (arg :: Const m a)
type Maximum (arg :: Const m a) #
Instance details Defined in Data.Singletons.Prelude.Const type Maximum (arg :: Const m a)
type Minimum (arg :: Const m a) #
Instance details Defined in Data.Singletons.Prelude.Const type Minimum (arg :: Const m a)
type Sum (arg :: Const m a) #
Instance details Defined in Data.Singletons.Prelude.Const type Sum (arg :: Const m a)
type Product (arg :: Const m a) #
Instance details Defined in Data.Singletons.Prelude.Const type Product (arg :: Const m a)
type Foldr1 (arg1 :: a ~> (a ~> a)) (arg2 :: Const m a) #
Instance details Defined in Data.Singletons.Prelude.Const type Foldr1 (arg1 :: a ~> (a ~> a)) (arg2 :: Const m a)
type Foldl1 (arg1 :: a ~> (a ~> a)) (arg2 :: Const m a) #
Instance details Defined in Data.Singletons.Prelude.Const type Foldl1 (arg1 :: a ~> (a ~> a)) (arg2 :: Const m a)
type Elem (arg1 :: a) (arg2 :: Const m a) #
Instance details Defined in Data.Singletons.Prelude.Const type Elem (arg1 :: a) (arg2 :: Const m a)
type SequenceA (arg :: Const m (f a)) #
Instance details Defined in Data.Singletons.Prelude.Traversable type SequenceA (arg :: Const m (f a))
type Sequence (arg :: Const m1 (m2 a)) #
Instance details Defined in Data.Singletons.Prelude.Traversable type Sequence (arg :: Const m1 (m2 a))
type (a1 :: Const m (a6989586621679563429 ~> b6989586621679563430)) <*> (a2 :: Const m a6989586621679563429) #
Instance details Defined in Data.Singletons.Prelude.Const type (a1 :: Const m (a6989586621679563429 ~> b6989586621679563430)) <*> (a2 :: Const m a6989586621679563429)
type (arg1 :: Const m a) *> (arg2 :: Const m b) #
Instance details Defined in Data.Singletons.Prelude.Const type (arg1 :: Const m a) *> (arg2 :: Const m b)
type (arg1 :: Const m a) <* (arg2 :: Const m b) #
Instance details Defined in Data.Singletons.Prelude.Const type (arg1 :: Const m a) <* (arg2 :: Const m b)
type Fmap (a1 :: a6989586621679563423 ~> b6989586621679563424) (a2 :: Const m a6989586621679563423) #
Instance details Defined in Data.Singletons.Prelude.Const type Fmap (a1 :: a6989586621679563423 ~> b6989586621679563424) (a2 :: Const m a6989586621679563423)
type (a1 :: k1) <$ (a2 :: Const m b6989586621679563426) #
Instance details Defined in Data.Singletons.Prelude.Const type (a1 :: k1) <$ (a2 :: Const m b6989586621679563426)
type FoldMap (a1 :: a6989586621680486187 ~> k2) (a2 :: Const m a6989586621680486187) #
Instance details Defined in Data.Singletons.Prelude.Const type FoldMap (a1 :: a6989586621680486187 ~> k2) (a2 :: Const m a6989586621680486187)
type Foldr (a1 :: a6989586621680486188 ~> (k2 ~> k2)) (a2 :: k2) (a3 :: Const m a6989586621680486188) #
Instance details Defined in Data.Singletons.Prelude.Const type Foldr (a1 :: a6989586621680486188 ~> (k2 ~> k2)) (a2 :: k2) (a3 :: Const m a6989586621680486188)
type Foldr' (arg1 :: a ~> (b ~> b)) (arg2 :: b) (arg3 :: Const m a) #
Instance details Defined in Data.Singletons.Prelude.Const type Foldr' (arg1 :: a ~> (b ~> b)) (arg2 :: b) (arg3 :: Const m a)
type Foldl (arg1 :: b ~> (a ~> b)) (arg2 :: b) (arg3 :: Const m a) #
Instance details Defined in Data.Singletons.Prelude.Const type Foldl (arg1 :: b ~> (a ~> b)) (arg2 :: b) (arg3 :: Const m a)
type Foldl' (arg1 :: b ~> (a ~> b)) (arg2 :: b) (arg3 :: Const m a) #
Instance details Defined in Data.Singletons.Prelude.Const type Foldl' (arg1 :: b ~> (a ~> b)) (arg2 :: b) (arg3 :: Const m a)
type Traverse (a1 :: a6989586621680790270 ~> f6989586621680790269 b6989586621680790271) (a2 :: Const m a6989586621680790270) #
Instance details Defined in Data.Singletons.Prelude.Traversable type Traverse (a1 :: a6989586621680790270 ~> f6989586621680790269 b6989586621680790271) (a2 :: Const m a6989586621680790270)
type MapM (arg1 :: a ~> m1 b) (arg2 :: Const m2 a) #
Instance details Defined in Data.Singletons.Prelude.Traversable type MapM (arg1 :: a ~> m1 b) (arg2 :: Const m2 a)
type LiftA2 (a1 :: a6989586621679563431 ~> (b6989586621679563432 ~> c6989586621679563433)) (a2 :: Const m a6989586621679563431) (a3 :: Const m b6989586621679563432) #
Instance details Defined in Data.Singletons.Prelude.Const type LiftA2 (a1 :: a6989586621679563431 ~> (b6989586621679563432 ~> c6989586621679563433)) (a2 :: Const m a6989586621679563431) (a3 :: Const m b6989586621679563432)
type Rep (Const a b)	Since: base-4.9.0.0
Instance details Defined in Data.Functor.Const type Rep (Const a b) = D1 (MetaData "Const" "Data.Functor.Const" "base" True) (C1 (MetaCons "Const" PrefixI True) (S1 (MetaSel (Just "getConst") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a)))
type Demote (Const a b) #
Instance details Defined in Data.Singletons.Prelude.Const type Demote (Const a b) = Const (Demote a) b
data Sing (c :: Const a b) #
Instance details Defined in Data.Singletons.Prelude.Const data Sing (c :: Const a b) where SConst :: forall k a (b :: k) (c :: Const a b) (a :: a). {..} -> Sing (Const a :: Const a b)
type MinBound #
Instance details Defined in Data.Singletons.Prelude.Const type MinBound
type MaxBound #
Instance details Defined in Data.Singletons.Prelude.Const type MaxBound
type Mempty #
Instance details Defined in Data.Singletons.Prelude.Const type Mempty
type Negate (a2 :: Const a1 b) #
Instance details Defined in Data.Singletons.Prelude.Const type Negate (a2 :: Const a1 b)
type Abs (a2 :: Const a1 b) #
Instance details Defined in Data.Singletons.Prelude.Const type Abs (a2 :: Const a1 b)
type Signum (a2 :: Const a1 b) #
Instance details Defined in Data.Singletons.Prelude.Const type Signum (a2 :: Const a1 b)
type FromInteger a2 #
Instance details Defined in Data.Singletons.Prelude.Const type FromInteger a2
type Succ (a2 :: Const a1 b) #
Instance details Defined in Data.Singletons.Prelude.Const type Succ (a2 :: Const a1 b)
type Pred (a2 :: Const a1 b) #
Instance details Defined in Data.Singletons.Prelude.Const type Pred (a2 :: Const a1 b)
type ToEnum a2 #
Instance details Defined in Data.Singletons.Prelude.Const type ToEnum a2
type FromEnum (a2 :: Const a1 b) #
Instance details Defined in Data.Singletons.Prelude.Const type FromEnum (a2 :: Const a1 b)
type Sconcat (arg :: NonEmpty (Const a b)) #
Instance details Defined in Data.Singletons.Prelude.Const type Sconcat (arg :: NonEmpty (Const a b))
type Show_ (arg :: Const a b) #
Instance details Defined in Data.Singletons.Prelude.Const type Show_ (arg :: Const a b)
type Mconcat (arg :: [Const a b]) #
Instance details Defined in Data.Singletons.Prelude.Const type Mconcat (arg :: [Const a b])
type FromString a2 #
Instance details Defined in Data.Singletons.Prelude.IsString type FromString a2
type (a2 :: Const a1 b1) == (b2 :: Const a1 b1) #
Instance details Defined in Data.Singletons.Prelude.Const type (a2 :: Const a1 b1) == (b2 :: Const a1 b1)
type (x :: Const a b) /= (y :: Const a b) #
Instance details Defined in Data.Singletons.Prelude.Const type (x :: Const a b) /= (y :: Const a b) = Not (x == y)
type Compare (a2 :: Const a1 b) (a3 :: Const a1 b) #
Instance details Defined in Data.Singletons.Prelude.Const type Compare (a2 :: Const a1 b) (a3 :: Const a1 b)
type (arg1 :: Const a b) < (arg2 :: Const a b) #
Instance details Defined in Data.Singletons.Prelude.Const type (arg1 :: Const a b) < (arg2 :: Const a b)
type (arg1 :: Const a b) <= (arg2 :: Const a b) #
Instance details Defined in Data.Singletons.Prelude.Const type (arg1 :: Const a b) <= (arg2 :: Const a b)
type (arg1 :: Const a b) > (arg2 :: Const a b) #
Instance details Defined in Data.Singletons.Prelude.Const type (arg1 :: Const a b) > (arg2 :: Const a b)
type (arg1 :: Const a b) >= (arg2 :: Const a b) #
Instance details Defined in Data.Singletons.Prelude.Const type (arg1 :: Const a b) >= (arg2 :: Const a b)
type Max (arg1 :: Const a b) (arg2 :: Const a b) #
Instance details Defined in Data.Singletons.Prelude.Const type Max (arg1 :: Const a b) (arg2 :: Const a b)
type Min (arg1 :: Const a b) (arg2 :: Const a b) #
Instance details Defined in Data.Singletons.Prelude.Const type Min (arg1 :: Const a b) (arg2 :: Const a b)
type (a2 :: Const a1 b) + (a3 :: Const a1 b) #
Instance details Defined in Data.Singletons.Prelude.Const type (a2 :: Const a1 b) + (a3 :: Const a1 b)
type (a2 :: Const a1 b) - (a3 :: Const a1 b) #
Instance details Defined in Data.Singletons.Prelude.Const type (a2 :: Const a1 b) - (a3 :: Const a1 b)
type (a2 :: Const a1 b) * (a3 :: Const a1 b) #
Instance details Defined in Data.Singletons.Prelude.Const type (a2 :: Const a1 b) * (a3 :: Const a1 b)
type EnumFromTo (a2 :: Const a1 b) (a3 :: Const a1 b) #
Instance details Defined in Data.Singletons.Prelude.Const type EnumFromTo (a2 :: Const a1 b) (a3 :: Const a1 b)
type (a2 :: Const a1 b) <> (a3 :: Const a1 b) #
Instance details Defined in Data.Singletons.Prelude.Const type (a2 :: Const a1 b) <> (a3 :: Const a1 b)
type ShowList (arg1 :: [Const a b]) arg2 #
Instance details Defined in Data.Singletons.Prelude.Const type ShowList (arg1 :: [Const a b]) arg2
type Mappend (arg1 :: Const a b) (arg2 :: Const a b) #
Instance details Defined in Data.Singletons.Prelude.Const type Mappend (arg1 :: Const a b) (arg2 :: Const a b)
type EnumFromThenTo (a2 :: Const a1 b) (a3 :: Const a1 b) (a4 :: Const a1 b) #
Instance details Defined in Data.Singletons.Prelude.Const type EnumFromThenTo (a2 :: Const a1 b) (a3 :: Const a1 b) (a4 :: Const a1 b)
type ShowsPrec a2 (a3 :: Const a1 b) a4 #
Instance details Defined in Data.Singletons.Prelude.Const type ShowsPrec a2 (a3 :: Const a1 b) a4
type Apply (ConstSym0 :: TyFun a (Const a b6989586621679093210) -> Type) (t6989586621680750415 :: a) #
Instance details Defined in Data.Singletons.Prelude.Const type Apply (ConstSym0 :: TyFun a (Const a b6989586621679093210) -> Type) (t6989586621680750415 :: a) = (Const t6989586621680750415 :: Const a b6989586621679093210)

type family GetConst (x :: Const a b) :: a where ... #

Equations

GetConst (Const x) = x

type family (a :: (~>) a b) <$> (a :: f a) :: f b where ... infixl 4 #

Equations

a_6989586621679735828 <$> a_6989586621679735830 = Apply (Apply FmapSym0 a_6989586621679735828) a_6989586621679735830

(%<$>) :: forall f a b (t :: (~>) a b) (t :: f a). SFunctor f => Sing t -> Sing t -> Sing (Apply (Apply (<$>@#@$) t) t :: f b) infixl 4 #

type family (arg :: a) <$ (arg :: f b) :: f a infixl 4 #

Instances

type (a1 :: k1) <$ (a2 :: [b6989586621679563426]) #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal type (a1 :: k1) <$ (a2 :: [b6989586621679563426])
type (a1 :: k1) <$ (a2 :: Maybe b6989586621679563426) #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal type (a1 :: k1) <$ (a2 :: Maybe b6989586621679563426)
type (a1 :: k1) <$ (a2 :: Min b6989586621679563426) #
Instance details Defined in Data.Singletons.Prelude.Semigroup type (a1 :: k1) <$ (a2 :: Min b6989586621679563426)
type (a1 :: k1) <$ (a2 :: Max b6989586621679563426) #
Instance details Defined in Data.Singletons.Prelude.Semigroup type (a1 :: k1) <$ (a2 :: Max b6989586621679563426)
type (a1 :: k1) <$ (a2 :: First b6989586621679563426) #
Instance details Defined in Data.Singletons.Prelude.Semigroup type (a1 :: k1) <$ (a2 :: First b6989586621679563426)
type (a1 :: k1) <$ (a2 :: Last b6989586621679563426) #
Instance details Defined in Data.Singletons.Prelude.Semigroup type (a1 :: k1) <$ (a2 :: Last b6989586621679563426)
type (a1 :: k1) <$ (a2 :: Option b6989586621679563426) #
Instance details Defined in Data.Singletons.Prelude.Semigroup type (a1 :: k1) <$ (a2 :: Option b6989586621679563426)
type (a1 :: k1) <$ (a2 :: Identity b6989586621679563426) #
Instance details Defined in Data.Singletons.Prelude.Identity type (a1 :: k1) <$ (a2 :: Identity b6989586621679563426)
type (a1 :: k1) <$ (a2 :: First b6989586621679563426) #
Instance details Defined in Data.Singletons.Prelude.Monoid type (a1 :: k1) <$ (a2 :: First b6989586621679563426)
type (a1 :: k1) <$ (a2 :: Last b6989586621679563426) #
Instance details Defined in Data.Singletons.Prelude.Monoid type (a1 :: k1) <$ (a2 :: Last b6989586621679563426)
type (a1 :: k1) <$ (a2 :: Dual b6989586621679563426) #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type (a1 :: k1) <$ (a2 :: Dual b6989586621679563426)
type (a1 :: k1) <$ (a2 :: Sum b6989586621679563426) #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type (a1 :: k1) <$ (a2 :: Sum b6989586621679563426)
type (a1 :: k1) <$ (a2 :: Product b6989586621679563426) #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type (a1 :: k1) <$ (a2 :: Product b6989586621679563426)
type (a1 :: k1) <$ (a2 :: Down b6989586621679563426) #
Instance details Defined in Data.Singletons.Prelude.Functor type (a1 :: k1) <$ (a2 :: Down b6989586621679563426)
type (a1 :: k1) <$ (a2 :: NonEmpty b6989586621679563426) #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal type (a1 :: k1) <$ (a2 :: NonEmpty b6989586621679563426)
type (a2 :: k1) <$ (a3 :: Either a1 b6989586621679563426) #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal type (a2 :: k1) <$ (a3 :: Either a1 b6989586621679563426)
type (a2 :: k1) <$ (a3 :: (a1, b6989586621679563426)) #
Instance details Defined in Data.Singletons.Prelude.Functor type (a2 :: k1) <$ (a3 :: (a1, b6989586621679563426))
type (a2 :: k1) <$ (a3 :: Arg a1 b6989586621679563426) #
Instance details Defined in Data.Singletons.Prelude.Semigroup type (a2 :: k1) <$ (a3 :: Arg a1 b6989586621679563426)
type (a1 :: k1) <$ (a2 :: Const m b6989586621679563426) #
Instance details Defined in Data.Singletons.Prelude.Const type (a1 :: k1) <$ (a2 :: Const m b6989586621679563426)

(%<$) :: forall a b (t :: a) (t :: f b). SFunctor f => Sing t -> Sing t -> Sing (Apply (Apply (<$@#@$) t) t :: f a) infixl 4 #

type family (a :: f a) <**> (a :: f ((~>) a b)) :: f b where ... infixl 4 #

Equations

a_6989586621679563796 <**> a_6989586621679563798 = Apply (Apply (Apply LiftA2Sym0 (Apply (Apply Lambda_6989586621679563806Sym0 a_6989586621679563796) a_6989586621679563798)) a_6989586621679563796) a_6989586621679563798

(%<**>) :: forall f a b (t :: f a) (t :: f ((~>) a b)). SApplicative f => Sing t -> Sing t -> Sing (Apply (Apply (<**>@#@$) t) t :: f b) infixl 4 #

type family LiftA (a :: (~>) a b) (a :: f a) :: f b where ... #

Equations

LiftA f a = Apply (Apply (<*>@#@$) (Apply PureSym0 f)) a

sLiftA :: forall f a b (t :: (~>) a b) (t :: f a). SApplicative f => Sing t -> Sing t -> Sing (Apply (Apply LiftASym0 t) t :: f b) #

type family LiftA3 (a :: (~>) a ((~>) b ((~>) c d))) (a :: f a) (a :: f b) (a :: f c) :: f d where ... #

Equations

LiftA3 f a b c = Apply (Apply (<*>@#@$) (Apply (Apply (Apply LiftA2Sym0 f) a) b)) c

sLiftA3 :: forall f a b c d (t :: (~>) a ((~>) b ((~>) c d))) (t :: f a) (t :: f b) (t :: f c). SApplicative f => Sing t -> Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply (Apply LiftA3Sym0 t) t) t) t :: f d) #

type family Optional (a :: f a) :: f (Maybe a) where ... #

Equations

Optional v = Apply (Apply (<|>@#@$) (Apply (Apply (<$>@#@$) JustSym0) v)) (Apply PureSym0 NothingSym0)

sOptional :: forall f a (t :: f a). SAlternative f => Sing t -> Sing (Apply OptionalSym0 t :: f (Maybe a)) #

Defunctionalization symbols

data PureSym0 :: forall a6989586621679563428 f6989586621679563427. (~>) a6989586621679563428 (f6989586621679563427 a6989586621679563428) #

Instances

SApplicative f => SingI (PureSym0 :: TyFun a (f a) -> Type) #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing PureSym0 #
SuppressUnusedWarnings (PureSym0 :: TyFun a6989586621679563428 (f6989586621679563427 a6989586621679563428) -> Type) #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods suppressUnusedWarnings :: () #
type Apply (PureSym0 :: TyFun a (f6989586621679563427 a) -> Type) (arg6989586621679563840 :: a) #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal type Apply (PureSym0 :: TyFun a (f6989586621679563427 a) -> Type) (arg6989586621679563840 :: a) = (Pure arg6989586621679563840 :: f6989586621679563427 a)

type PureSym1 (arg6989586621679563840 :: a6989586621679563428) = Pure arg6989586621679563840 #

data (<*>@#@$) :: forall a6989586621679563429 b6989586621679563430 f6989586621679563427. (~>) (f6989586621679563427 ((~>) a6989586621679563429 b6989586621679563430)) ((~>) (f6989586621679563427 a6989586621679563429) (f6989586621679563427 b6989586621679563430)) infixl 4 #

Instances

SApplicative f => SingI ((<*>@#@$) :: TyFun (f (a ~> b)) (f a ~> f b) -> Type) #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing (<*>@#@$) #
SuppressUnusedWarnings ((<*>@#@$) :: TyFun (f6989586621679563427 (a6989586621679563429 ~> b6989586621679563430)) (f6989586621679563427 a6989586621679563429 ~> f6989586621679563427 b6989586621679563430) -> Type) #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods suppressUnusedWarnings :: () #
type Apply ((<*>@#@$) :: TyFun (f6989586621679563427 (a6989586621679563429 ~> b6989586621679563430)) (f6989586621679563427 a6989586621679563429 ~> f6989586621679563427 b6989586621679563430) -> Type) (arg6989586621679563842 :: f6989586621679563427 (a6989586621679563429 ~> b6989586621679563430)) #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal type Apply ((<>@#@$) :: TyFun (f6989586621679563427 (a6989586621679563429 ~> b6989586621679563430)) (f6989586621679563427 a6989586621679563429 ~> f6989586621679563427 b6989586621679563430) -> Type) (arg6989586621679563842 :: f6989586621679563427 (a6989586621679563429 ~> b6989586621679563430)) = (<>@#@$$) arg6989586621679563842

data (<*>@#@$$) (arg6989586621679563842 :: f6989586621679563427 ((~>) a6989586621679563429 b6989586621679563430)) :: (~>) (f6989586621679563427 a6989586621679563429) (f6989586621679563427 b6989586621679563430) infixl 4 #

Instances

(SApplicative f, SingI d) => SingI ((<*>@#@$$) d :: TyFun (f a) (f b) -> Type) #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing ((<*>@#@$$) d) #
SuppressUnusedWarnings ((<*>@#@$$) arg6989586621679563842 :: TyFun (f6989586621679563427 a6989586621679563429) (f6989586621679563427 b6989586621679563430) -> Type) #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods suppressUnusedWarnings :: () #
type Apply ((<*>@#@$$) arg6989586621679563842 :: TyFun (f a) (f b) -> Type) (arg6989586621679563843 :: f a) #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal type Apply ((<>@#@$$) arg6989586621679563842 :: TyFun (f a) (f b) -> Type) (arg6989586621679563843 :: f a) = arg6989586621679563842 <> arg6989586621679563843

type (<*>@#@$$$) (arg6989586621679563842 :: f6989586621679563427 ((~>) a6989586621679563429 b6989586621679563430)) (arg6989586621679563843 :: f6989586621679563427 a6989586621679563429) = (<*>) arg6989586621679563842 arg6989586621679563843 #

data (*>@#@$) :: forall a6989586621679563434 b6989586621679563435 f6989586621679563427. (~>) (f6989586621679563427 a6989586621679563434) ((~>) (f6989586621679563427 b6989586621679563435) (f6989586621679563427 b6989586621679563435)) infixl 4 #

Instances

SApplicative f => SingI ((*>@#@$) :: TyFun (f a) (f b ~> f b) -> Type) #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing (*>@#@$) #
SuppressUnusedWarnings ((*>@#@$) :: TyFun (f6989586621679563427 a6989586621679563434) (f6989586621679563427 b6989586621679563435 ~> f6989586621679563427 b6989586621679563435) -> Type) #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods suppressUnusedWarnings :: () #
type Apply ((*>@#@$) :: TyFun (f6989586621679563427 a6989586621679563434) (f6989586621679563427 b6989586621679563435 ~> f6989586621679563427 b6989586621679563435) -> Type) (arg6989586621679563852 :: f6989586621679563427 a6989586621679563434) #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal type Apply ((>@#@$) :: TyFun (f6989586621679563427 a6989586621679563434) (f6989586621679563427 b6989586621679563435 ~> f6989586621679563427 b6989586621679563435) -> Type) (arg6989586621679563852 :: f6989586621679563427 a6989586621679563434) = (arg6989586621679563852 >@#@$$ b6989586621679563435 :: TyFun (f6989586621679563427 b6989586621679563435) (f6989586621679563427 b6989586621679563435) -> Type)

data (*>@#@$$) (arg6989586621679563852 :: f6989586621679563427 a6989586621679563434) :: forall b6989586621679563435. (~>) (f6989586621679563427 b6989586621679563435) (f6989586621679563427 b6989586621679563435) infixl 4 #

Instances

(SApplicative f, SingI d) => SingI (d *>@#@$$ b :: TyFun (f b) (f b) -> Type) #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing (d *>@#@$$ b) #
SuppressUnusedWarnings (arg6989586621679563852 *>@#@$$ b6989586621679563435 :: TyFun (f6989586621679563427 b6989586621679563435) (f6989586621679563427 b6989586621679563435) -> Type) #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods suppressUnusedWarnings :: () #
type Apply (arg6989586621679563852 *>@#@$$ b :: TyFun (f b) (f b) -> Type) (arg6989586621679563853 :: f b) #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal type Apply (arg6989586621679563852 >@#@$$ b :: TyFun (f b) (f b) -> Type) (arg6989586621679563853 :: f b) = arg6989586621679563852 > arg6989586621679563853

type (*>@#@$$$) (arg6989586621679563852 :: f6989586621679563427 a6989586621679563434) (arg6989586621679563853 :: f6989586621679563427 b6989586621679563435) = (*>) arg6989586621679563852 arg6989586621679563853 #

data (<*@#@$) :: forall a6989586621679563436 b6989586621679563437 f6989586621679563427. (~>) (f6989586621679563427 a6989586621679563436) ((~>) (f6989586621679563427 b6989586621679563437) (f6989586621679563427 a6989586621679563436)) infixl 4 #

Instances

SApplicative f => SingI ((<*@#@$) :: TyFun (f a) (f b ~> f a) -> Type) #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing (<*@#@$) #
SuppressUnusedWarnings ((<*@#@$) :: TyFun (f6989586621679563427 a6989586621679563436) (f6989586621679563427 b6989586621679563437 ~> f6989586621679563427 a6989586621679563436) -> Type) #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods suppressUnusedWarnings :: () #
type Apply ((<*@#@$) :: TyFun (f6989586621679563427 a6989586621679563436) (f6989586621679563427 b6989586621679563437 ~> f6989586621679563427 a6989586621679563436) -> Type) (arg6989586621679563856 :: f6989586621679563427 a6989586621679563436) #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal type Apply ((<@#@$) :: TyFun (f6989586621679563427 a6989586621679563436) (f6989586621679563427 b6989586621679563437 ~> f6989586621679563427 a6989586621679563436) -> Type) (arg6989586621679563856 :: f6989586621679563427 a6989586621679563436) = (arg6989586621679563856 <@#@$$ b6989586621679563437 :: TyFun (f6989586621679563427 b6989586621679563437) (f6989586621679563427 a6989586621679563436) -> Type)

data (<*@#@$$) (arg6989586621679563856 :: f6989586621679563427 a6989586621679563436) :: forall b6989586621679563437. (~>) (f6989586621679563427 b6989586621679563437) (f6989586621679563427 a6989586621679563436) infixl 4 #

Instances

(SApplicative f, SingI d) => SingI (d <*@#@$$ b :: TyFun (f b) (f a) -> Type) #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing (d <*@#@$$ b) #
SuppressUnusedWarnings (arg6989586621679563856 <*@#@$$ b6989586621679563437 :: TyFun (f6989586621679563427 b6989586621679563437) (f6989586621679563427 a6989586621679563436) -> Type) #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods suppressUnusedWarnings :: () #
type Apply (arg6989586621679563856 <*@#@$$ b :: TyFun (f b) (f a) -> Type) (arg6989586621679563857 :: f b) #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal type Apply (arg6989586621679563856 <@#@$$ b :: TyFun (f b) (f a) -> Type) (arg6989586621679563857 :: f b) = arg6989586621679563856 < arg6989586621679563857

type (<*@#@$$$) (arg6989586621679563856 :: f6989586621679563427 a6989586621679563436) (arg6989586621679563857 :: f6989586621679563427 b6989586621679563437) = (<*) arg6989586621679563856 arg6989586621679563857 #

type EmptySym0 = Empty #

data (<|>@#@$) :: forall a6989586621679563506 f6989586621679563504. (~>) (f6989586621679563504 a6989586621679563506) ((~>) (f6989586621679563504 a6989586621679563506) (f6989586621679563504 a6989586621679563506)) infixl 3 #

Instances

SAlternative f => SingI ((<\|>@#@$) :: TyFun (f a) (f a ~> f a) -> Type) #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing (<\|>@#@$) #
SuppressUnusedWarnings ((<\|>@#@$) :: TyFun (f6989586621679563504 a6989586621679563506) (f6989586621679563504 a6989586621679563506 ~> f6989586621679563504 a6989586621679563506) -> Type) #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods suppressUnusedWarnings :: () #
type Apply ((<\|>@#@$) :: TyFun (f6989586621679563504 a6989586621679563506) (f6989586621679563504 a6989586621679563506 ~> f6989586621679563504 a6989586621679563506) -> Type) (arg6989586621679563973 :: f6989586621679563504 a6989586621679563506) #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal type Apply ((<\|>@#@$) :: TyFun (f6989586621679563504 a6989586621679563506) (f6989586621679563504 a6989586621679563506 ~> f6989586621679563504 a6989586621679563506) -> Type) (arg6989586621679563973 :: f6989586621679563504 a6989586621679563506) = (<\|>@#@$$) arg6989586621679563973

data (<|>@#@$$) (arg6989586621679563973 :: f6989586621679563504 a6989586621679563506) :: (~>) (f6989586621679563504 a6989586621679563506) (f6989586621679563504 a6989586621679563506) infixl 3 #

Instances

(SAlternative f, SingI d) => SingI ((<\|>@#@$$) d :: TyFun (f a) (f a) -> Type) #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing ((<\|>@#@$$) d) #
SuppressUnusedWarnings ((<\|>@#@$$) arg6989586621679563973 :: TyFun (f6989586621679563504 a6989586621679563506) (f6989586621679563504 a6989586621679563506) -> Type) #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods suppressUnusedWarnings :: () #
type Apply ((<\|>@#@$$) arg6989586621679563973 :: TyFun (f a) (f a) -> Type) (arg6989586621679563974 :: f a) #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal type Apply ((<\|>@#@$$) arg6989586621679563973 :: TyFun (f a) (f a) -> Type) (arg6989586621679563974 :: f a) = arg6989586621679563973 <\|> arg6989586621679563974

type (<|>@#@$$$) (arg6989586621679563973 :: f6989586621679563504 a6989586621679563506) (arg6989586621679563974 :: f6989586621679563504 a6989586621679563506) = (<|>) arg6989586621679563973 arg6989586621679563974 #

data ConstSym0 :: forall (a6989586621679093209 :: Type) k6989586621679093208 (b6989586621679093210 :: k6989586621679093208). (~>) a6989586621679093209 (Const (a6989586621679093209 :: Type) (b6989586621679093210 :: k6989586621679093208)) #

Instances

SingI (ConstSym0 :: TyFun a6989586621679093209 (Const a6989586621679093209 b6989586621679093210) -> Type) #
Instance details Defined in Data.Singletons.Prelude.Const Methods sing :: Sing ConstSym0 #
SuppressUnusedWarnings (ConstSym0 :: TyFun a6989586621679093209 (Const a6989586621679093209 b6989586621679093210) -> Type) #
Instance details Defined in Data.Singletons.Prelude.Const Methods suppressUnusedWarnings :: () #
type Apply (ConstSym0 :: TyFun a (Const a b6989586621679093210) -> Type) (t6989586621680750415 :: a) #
Instance details Defined in Data.Singletons.Prelude.Const type Apply (ConstSym0 :: TyFun a (Const a b6989586621679093210) -> Type) (t6989586621680750415 :: a) = (Const t6989586621680750415 :: Const a b6989586621679093210)

type ConstSym1 (t6989586621680750415 :: a6989586621679093209) = Const t6989586621680750415 #

data GetConstSym0 :: forall a6989586621680750730 b6989586621680750731. (~>) (Const a6989586621680750730 b6989586621680750731) a6989586621680750730 #

Instances

SuppressUnusedWarnings (GetConstSym0 :: TyFun (Const a6989586621680750730 b6989586621680750731) a6989586621680750730 -> Type) #
Instance details Defined in Data.Singletons.Prelude.Const Methods suppressUnusedWarnings :: () #
type Apply (GetConstSym0 :: TyFun (Const a b) a -> Type) (x6989586621680750732 :: Const a b) #
Instance details Defined in Data.Singletons.Prelude.Const type Apply (GetConstSym0 :: TyFun (Const a b) a -> Type) (x6989586621680750732 :: Const a b) = GetConst x6989586621680750732

type GetConstSym1 (x6989586621680750732 :: Const a6989586621680750730 b6989586621680750731) = GetConst x6989586621680750732 #

data (<$>@#@$) :: forall a6989586621679735752 b6989586621679735753 f6989586621679735751. (~>) ((~>) a6989586621679735752 b6989586621679735753) ((~>) (f6989586621679735751 a6989586621679735752) (f6989586621679735751 b6989586621679735753)) infixl 4 #

Instances

SFunctor f => SingI ((<$>@#@$) :: TyFun (a ~> b) (f a ~> f b) -> Type) #
Instance details Defined in Data.Singletons.Prelude.Functor Methods sing :: Sing (<$>@#@$) #
SuppressUnusedWarnings ((<$>@#@$) :: TyFun (a6989586621679735752 ~> b6989586621679735753) (f6989586621679735751 a6989586621679735752 ~> f6989586621679735751 b6989586621679735753) -> Type) #
Instance details Defined in Data.Singletons.Prelude.Functor Methods suppressUnusedWarnings :: () #
type Apply ((<$>@#@$) :: TyFun (a6989586621679735752 ~> b6989586621679735753) (f6989586621679735751 a6989586621679735752 ~> f6989586621679735751 b6989586621679735753) -> Type) (a6989586621679735832 :: a6989586621679735752 ~> b6989586621679735753) #
Instance details Defined in Data.Singletons.Prelude.Functor type Apply ((<$>@#@$) :: TyFun (a6989586621679735752 ~> b6989586621679735753) (f6989586621679735751 a6989586621679735752 ~> f6989586621679735751 b6989586621679735753) -> Type) (a6989586621679735832 :: a6989586621679735752 ~> b6989586621679735753) = (a6989586621679735832 <$>@#@$$ f6989586621679735751 :: TyFun (f6989586621679735751 a6989586621679735752) (f6989586621679735751 b6989586621679735753) -> Type)

data (<$>@#@$$) (a6989586621679735832 :: (~>) a6989586621679735752 b6989586621679735753) :: forall f6989586621679735751. (~>) (f6989586621679735751 a6989586621679735752) (f6989586621679735751 b6989586621679735753) infixl 4 #

Instances

(SFunctor f, SingI d) => SingI (d <$>@#@$$ f :: TyFun (f a) (f b) -> Type) #
Instance details Defined in Data.Singletons.Prelude.Functor Methods sing :: Sing (d <$>@#@$$ f) #
SuppressUnusedWarnings (a6989586621679735832 <$>@#@$$ f6989586621679735751 :: TyFun (f6989586621679735751 a6989586621679735752) (f6989586621679735751 b6989586621679735753) -> Type) #
Instance details Defined in Data.Singletons.Prelude.Functor Methods suppressUnusedWarnings :: () #
type Apply (a6989586621679735832 <$>@#@$$ f :: TyFun (f a) (f b) -> Type) (a6989586621679735833 :: f a) #
Instance details Defined in Data.Singletons.Prelude.Functor type Apply (a6989586621679735832 <$>@#@$$ f :: TyFun (f a) (f b) -> Type) (a6989586621679735833 :: f a) = a6989586621679735832 <$> a6989586621679735833

type (<$>@#@$$$) (a6989586621679735832 :: (~>) a6989586621679735752 b6989586621679735753) (a6989586621679735833 :: f6989586621679735751 a6989586621679735752) = (<$>) a6989586621679735832 a6989586621679735833 #

data (<$@#@$) :: forall a6989586621679563425 b6989586621679563426 f6989586621679563422. (~>) a6989586621679563425 ((~>) (f6989586621679563422 b6989586621679563426) (f6989586621679563422 a6989586621679563425)) infixl 4 #

Instances

SFunctor f => SingI ((<$@#@$) :: TyFun a (f b ~> f a) -> Type) #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing (<$@#@$) #
SuppressUnusedWarnings ((<$@#@$) :: TyFun a6989586621679563425 (f6989586621679563422 b6989586621679563426 ~> f6989586621679563422 a6989586621679563425) -> Type) #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods suppressUnusedWarnings :: () #
type Apply ((<$@#@$) :: TyFun a6989586621679563425 (f6989586621679563422 b6989586621679563426 ~> f6989586621679563422 a6989586621679563425) -> Type) (arg6989586621679563820 :: a6989586621679563425) #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal type Apply ((<$@#@$) :: TyFun a6989586621679563425 (f6989586621679563422 b6989586621679563426 ~> f6989586621679563422 a6989586621679563425) -> Type) (arg6989586621679563820 :: a6989586621679563425) = ((arg6989586621679563820 <$@#@$$ b6989586621679563426) f6989586621679563422 :: TyFun (f6989586621679563422 b6989586621679563426) (f6989586621679563422 a6989586621679563425) -> Type)

data (<$@#@$$) (arg6989586621679563820 :: a6989586621679563425) :: forall b6989586621679563426 f6989586621679563422. (~>) (f6989586621679563422 b6989586621679563426) (f6989586621679563422 a6989586621679563425) infixl 4 #

Instances

(SFunctor f, SingI d) => SingI ((d <$@#@$$ b) f :: TyFun (f b) (f a) -> Type) #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing ((d <$@#@$$ b) f) #
SuppressUnusedWarnings ((arg6989586621679563820 <$@#@$$ b6989586621679563426) f6989586621679563422 :: TyFun (f6989586621679563422 b6989586621679563426) (f6989586621679563422 a6989586621679563425) -> Type) #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods suppressUnusedWarnings :: () #
type Apply ((arg6989586621679563820 <$@#@$$ b) f :: TyFun (f b) (f a) -> Type) (arg6989586621679563821 :: f b) #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal type Apply ((arg6989586621679563820 <$@#@$$ b) f :: TyFun (f b) (f a) -> Type) (arg6989586621679563821 :: f b) = arg6989586621679563820 <$ arg6989586621679563821

type (<$@#@$$$) (arg6989586621679563820 :: a6989586621679563425) (arg6989586621679563821 :: f6989586621679563422 b6989586621679563426) = (<$) arg6989586621679563820 arg6989586621679563821 #

data (<**>@#@$) :: forall a6989586621679563387 b6989586621679563388 f6989586621679563386. (~>) (f6989586621679563386 a6989586621679563387) ((~>) (f6989586621679563386 ((~>) a6989586621679563387 b6989586621679563388)) (f6989586621679563386 b6989586621679563388)) infixl 4 #

Instances

SApplicative f => SingI ((<**>@#@$) :: TyFun (f a) (f (a ~> b) ~> f b) -> Type) #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing (<**>@#@$) #
SuppressUnusedWarnings ((<**>@#@$) :: TyFun (f6989586621679563386 a6989586621679563387) (f6989586621679563386 (a6989586621679563387 ~> b6989586621679563388) ~> f6989586621679563386 b6989586621679563388) -> Type) #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods suppressUnusedWarnings :: () #
type Apply ((<**>@#@$) :: TyFun (f6989586621679563386 a6989586621679563387) (f6989586621679563386 (a6989586621679563387 ~> b6989586621679563388) ~> f6989586621679563386 b6989586621679563388) -> Type) (a6989586621679563800 :: f6989586621679563386 a6989586621679563387) #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal type Apply ((<>@#@$) :: TyFun (f6989586621679563386 a6989586621679563387) (f6989586621679563386 (a6989586621679563387 ~> b6989586621679563388) ~> f6989586621679563386 b6989586621679563388) -> Type) (a6989586621679563800 :: f6989586621679563386 a6989586621679563387) = (a6989586621679563800 <>@#@$$ b6989586621679563388 :: TyFun (f6989586621679563386 (a6989586621679563387 ~> b6989586621679563388)) (f6989586621679563386 b6989586621679563388) -> Type)

data (<**>@#@$$) (a6989586621679563800 :: f6989586621679563386 a6989586621679563387) :: forall b6989586621679563388. (~>) (f6989586621679563386 ((~>) a6989586621679563387 b6989586621679563388)) (f6989586621679563386 b6989586621679563388) infixl 4 #

Instances

(SApplicative f, SingI d) => SingI (d <**>@#@$$ b :: TyFun (f (a ~> b)) (f b) -> Type) #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing (d <**>@#@$$ b) #
SuppressUnusedWarnings (a6989586621679563800 <**>@#@$$ b6989586621679563388 :: TyFun (f6989586621679563386 (a6989586621679563387 ~> b6989586621679563388)) (f6989586621679563386 b6989586621679563388) -> Type) #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods suppressUnusedWarnings :: () #
type Apply (a6989586621679563800 <**>@#@$$ b :: TyFun (f (a ~> b)) (f b) -> Type) (a6989586621679563801 :: f (a ~> b)) #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal type Apply (a6989586621679563800 <>@#@$$ b :: TyFun (f (a ~> b)) (f b) -> Type) (a6989586621679563801 :: f (a ~> b)) = a6989586621679563800 <> a6989586621679563801

type (<**>@#@$$$) (a6989586621679563800 :: f6989586621679563386 a6989586621679563387) (a6989586621679563801 :: f6989586621679563386 ((~>) a6989586621679563387 b6989586621679563388)) = (<**>) a6989586621679563800 a6989586621679563801 #

data LiftASym0 :: forall a6989586621679563384 b6989586621679563385 f6989586621679563383. (~>) ((~>) a6989586621679563384 b6989586621679563385) ((~>) (f6989586621679563383 a6989586621679563384) (f6989586621679563383 b6989586621679563385)) #

Instances

SApplicative f => SingI (LiftASym0 :: TyFun (a ~> b) (f a ~> f b) -> Type) #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing LiftASym0 #
SuppressUnusedWarnings (LiftASym0 :: TyFun (a6989586621679563384 ~> b6989586621679563385) (f6989586621679563383 a6989586621679563384 ~> f6989586621679563383 b6989586621679563385) -> Type) #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods suppressUnusedWarnings :: () #
type Apply (LiftASym0 :: TyFun (a6989586621679563384 ~> b6989586621679563385) (f6989586621679563383 a6989586621679563384 ~> f6989586621679563383 b6989586621679563385) -> Type) (a6989586621679563790 :: a6989586621679563384 ~> b6989586621679563385) #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal type Apply (LiftASym0 :: TyFun (a6989586621679563384 ~> b6989586621679563385) (f6989586621679563383 a6989586621679563384 ~> f6989586621679563383 b6989586621679563385) -> Type) (a6989586621679563790 :: a6989586621679563384 ~> b6989586621679563385) = (LiftASym1 a6989586621679563790 f6989586621679563383 :: TyFun (f6989586621679563383 a6989586621679563384) (f6989586621679563383 b6989586621679563385) -> Type)

data LiftASym1 (a6989586621679563790 :: (~>) a6989586621679563384 b6989586621679563385) :: forall f6989586621679563383. (~>) (f6989586621679563383 a6989586621679563384) (f6989586621679563383 b6989586621679563385) #

Instances

(SApplicative f, SingI d) => SingI (LiftASym1 d f :: TyFun (f a) (f b) -> Type) #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing (LiftASym1 d f) #
SuppressUnusedWarnings (LiftASym1 a6989586621679563790 f6989586621679563383 :: TyFun (f6989586621679563383 a6989586621679563384) (f6989586621679563383 b6989586621679563385) -> Type) #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods suppressUnusedWarnings :: () #
type Apply (LiftASym1 a6989586621679563790 f :: TyFun (f a) (f b) -> Type) (a6989586621679563791 :: f a) #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal type Apply (LiftASym1 a6989586621679563790 f :: TyFun (f a) (f b) -> Type) (a6989586621679563791 :: f a) = LiftA a6989586621679563790 a6989586621679563791

type LiftASym2 (a6989586621679563790 :: (~>) a6989586621679563384 b6989586621679563385) (a6989586621679563791 :: f6989586621679563383 a6989586621679563384) = LiftA a6989586621679563790 a6989586621679563791 #

data LiftA2Sym0 :: forall a6989586621679563431 b6989586621679563432 c6989586621679563433 f6989586621679563427. (~>) ((~>) a6989586621679563431 ((~>) b6989586621679563432 c6989586621679563433)) ((~>) (f6989586621679563427 a6989586621679563431) ((~>) (f6989586621679563427 b6989586621679563432) (f6989586621679563427 c6989586621679563433))) #

Instances

SApplicative f => SingI (LiftA2Sym0 :: TyFun (a ~> (b ~> c)) (f a ~> (f b ~> f c)) -> Type) #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing LiftA2Sym0 #
SuppressUnusedWarnings (LiftA2Sym0 :: TyFun (a6989586621679563431 ~> (b6989586621679563432 ~> c6989586621679563433)) (f6989586621679563427 a6989586621679563431 ~> (f6989586621679563427 b6989586621679563432 ~> f6989586621679563427 c6989586621679563433)) -> Type) #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods suppressUnusedWarnings :: () #
type Apply (LiftA2Sym0 :: TyFun (a6989586621679563431 ~> (b6989586621679563432 ~> c6989586621679563433)) (f6989586621679563427 a6989586621679563431 ~> (f6989586621679563427 b6989586621679563432 ~> f6989586621679563427 c6989586621679563433)) -> Type) (arg6989586621679563846 :: a6989586621679563431 ~> (b6989586621679563432 ~> c6989586621679563433)) #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal type Apply (LiftA2Sym0 :: TyFun (a6989586621679563431 ~> (b6989586621679563432 ~> c6989586621679563433)) (f6989586621679563427 a6989586621679563431 ~> (f6989586621679563427 b6989586621679563432 ~> f6989586621679563427 c6989586621679563433)) -> Type) (arg6989586621679563846 :: a6989586621679563431 ~> (b6989586621679563432 ~> c6989586621679563433)) = (LiftA2Sym1 arg6989586621679563846 f6989586621679563427 :: TyFun (f6989586621679563427 a6989586621679563431) (f6989586621679563427 b6989586621679563432 ~> f6989586621679563427 c6989586621679563433) -> Type)

data LiftA2Sym1 (arg6989586621679563846 :: (~>) a6989586621679563431 ((~>) b6989586621679563432 c6989586621679563433)) :: forall f6989586621679563427. (~>) (f6989586621679563427 a6989586621679563431) ((~>) (f6989586621679563427 b6989586621679563432) (f6989586621679563427 c6989586621679563433)) #

Instances

(SApplicative f, SingI d) => SingI (LiftA2Sym1 d f :: TyFun (f a) (f b ~> f c) -> Type) #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing (LiftA2Sym1 d f) #
SuppressUnusedWarnings (LiftA2Sym1 arg6989586621679563846 f6989586621679563427 :: TyFun (f6989586621679563427 a6989586621679563431) (f6989586621679563427 b6989586621679563432 ~> f6989586621679563427 c6989586621679563433) -> Type) #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods suppressUnusedWarnings :: () #
type Apply (LiftA2Sym1 arg6989586621679563846 f6989586621679563427 :: TyFun (f6989586621679563427 a6989586621679563431) (f6989586621679563427 b6989586621679563432 ~> f6989586621679563427 c6989586621679563433) -> Type) (arg6989586621679563847 :: f6989586621679563427 a6989586621679563431) #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal type Apply (LiftA2Sym1 arg6989586621679563846 f6989586621679563427 :: TyFun (f6989586621679563427 a6989586621679563431) (f6989586621679563427 b6989586621679563432 ~> f6989586621679563427 c6989586621679563433) -> Type) (arg6989586621679563847 :: f6989586621679563427 a6989586621679563431) = LiftA2Sym2 arg6989586621679563846 arg6989586621679563847

data LiftA2Sym2 (arg6989586621679563846 :: (~>) a6989586621679563431 ((~>) b6989586621679563432 c6989586621679563433)) (arg6989586621679563847 :: f6989586621679563427 a6989586621679563431) :: (~>) (f6989586621679563427 b6989586621679563432) (f6989586621679563427 c6989586621679563433) #

Instances

(SApplicative f, SingI d1, SingI d2) => SingI (LiftA2Sym2 d1 d2 :: TyFun (f b) (f c) -> Type) #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing (LiftA2Sym2 d1 d2) #
SuppressUnusedWarnings (LiftA2Sym2 arg6989586621679563847 arg6989586621679563846 :: TyFun (f6989586621679563427 b6989586621679563432) (f6989586621679563427 c6989586621679563433) -> Type) #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods suppressUnusedWarnings :: () #
type Apply (LiftA2Sym2 arg6989586621679563847 arg6989586621679563846 :: TyFun (f b) (f c) -> Type) (arg6989586621679563848 :: f b) #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal type Apply (LiftA2Sym2 arg6989586621679563847 arg6989586621679563846 :: TyFun (f b) (f c) -> Type) (arg6989586621679563848 :: f b) = LiftA2 arg6989586621679563847 arg6989586621679563846 arg6989586621679563848

type LiftA2Sym3 (arg6989586621679563846 :: (~>) a6989586621679563431 ((~>) b6989586621679563432 c6989586621679563433)) (arg6989586621679563847 :: f6989586621679563427 a6989586621679563431) (arg6989586621679563848 :: f6989586621679563427 b6989586621679563432) = LiftA2 arg6989586621679563846 arg6989586621679563847 arg6989586621679563848 #

data LiftA3Sym0 :: forall a6989586621679563379 b6989586621679563380 c6989586621679563381 d6989586621679563382 f6989586621679563378. (~>) ((~>) a6989586621679563379 ((~>) b6989586621679563380 ((~>) c6989586621679563381 d6989586621679563382))) ((~>) (f6989586621679563378 a6989586621679563379) ((~>) (f6989586621679563378 b6989586621679563380) ((~>) (f6989586621679563378 c6989586621679563381) (f6989586621679563378 d6989586621679563382)))) #

Instances

SApplicative f => SingI (LiftA3Sym0 :: TyFun (a ~> (b ~> (c ~> d))) (f a ~> (f b ~> (f c ~> f d))) -> Type) #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing LiftA3Sym0 #
SuppressUnusedWarnings (LiftA3Sym0 :: TyFun (a6989586621679563379 ~> (b6989586621679563380 ~> (c6989586621679563381 ~> d6989586621679563382))) (f6989586621679563378 a6989586621679563379 ~> (f6989586621679563378 b6989586621679563380 ~> (f6989586621679563378 c6989586621679563381 ~> f6989586621679563378 d6989586621679563382))) -> Type) #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods suppressUnusedWarnings :: () #
type Apply (LiftA3Sym0 :: TyFun (a6989586621679563379 ~> (b6989586621679563380 ~> (c6989586621679563381 ~> d6989586621679563382))) (f6989586621679563378 a6989586621679563379 ~> (f6989586621679563378 b6989586621679563380 ~> (f6989586621679563378 c6989586621679563381 ~> f6989586621679563378 d6989586621679563382))) -> Type) (a6989586621679563778 :: a6989586621679563379 ~> (b6989586621679563380 ~> (c6989586621679563381 ~> d6989586621679563382))) #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal type Apply (LiftA3Sym0 :: TyFun (a6989586621679563379 ~> (b6989586621679563380 ~> (c6989586621679563381 ~> d6989586621679563382))) (f6989586621679563378 a6989586621679563379 ~> (f6989586621679563378 b6989586621679563380 ~> (f6989586621679563378 c6989586621679563381 ~> f6989586621679563378 d6989586621679563382))) -> Type) (a6989586621679563778 :: a6989586621679563379 ~> (b6989586621679563380 ~> (c6989586621679563381 ~> d6989586621679563382))) = (LiftA3Sym1 a6989586621679563778 f6989586621679563378 :: TyFun (f6989586621679563378 a6989586621679563379) (f6989586621679563378 b6989586621679563380 ~> (f6989586621679563378 c6989586621679563381 ~> f6989586621679563378 d6989586621679563382)) -> Type)

data LiftA3Sym1 (a6989586621679563778 :: (~>) a6989586621679563379 ((~>) b6989586621679563380 ((~>) c6989586621679563381 d6989586621679563382))) :: forall f6989586621679563378. (~>) (f6989586621679563378 a6989586621679563379) ((~>) (f6989586621679563378 b6989586621679563380) ((~>) (f6989586621679563378 c6989586621679563381) (f6989586621679563378 d6989586621679563382))) #

Instances

(SApplicative f, SingI d2) => SingI (LiftA3Sym1 d2 f :: TyFun (f a) (f b ~> (f c ~> f d1)) -> Type) #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing (LiftA3Sym1 d2 f) #
SuppressUnusedWarnings (LiftA3Sym1 a6989586621679563778 f6989586621679563378 :: TyFun (f6989586621679563378 a6989586621679563379) (f6989586621679563378 b6989586621679563380 ~> (f6989586621679563378 c6989586621679563381 ~> f6989586621679563378 d6989586621679563382)) -> Type) #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods suppressUnusedWarnings :: () #
type Apply (LiftA3Sym1 a6989586621679563778 f6989586621679563378 :: TyFun (f6989586621679563378 a6989586621679563379) (f6989586621679563378 b6989586621679563380 ~> (f6989586621679563378 c6989586621679563381 ~> f6989586621679563378 d6989586621679563382)) -> Type) (a6989586621679563779 :: f6989586621679563378 a6989586621679563379) #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal type Apply (LiftA3Sym1 a6989586621679563778 f6989586621679563378 :: TyFun (f6989586621679563378 a6989586621679563379) (f6989586621679563378 b6989586621679563380 ~> (f6989586621679563378 c6989586621679563381 ~> f6989586621679563378 d6989586621679563382)) -> Type) (a6989586621679563779 :: f6989586621679563378 a6989586621679563379) = LiftA3Sym2 a6989586621679563778 a6989586621679563779

data LiftA3Sym2 (a6989586621679563778 :: (~>) a6989586621679563379 ((~>) b6989586621679563380 ((~>) c6989586621679563381 d6989586621679563382))) (a6989586621679563779 :: f6989586621679563378 a6989586621679563379) :: (~>) (f6989586621679563378 b6989586621679563380) ((~>) (f6989586621679563378 c6989586621679563381) (f6989586621679563378 d6989586621679563382)) #

Instances

(SApplicative f, SingI d2, SingI d3) => SingI (LiftA3Sym2 d2 d3 :: TyFun (f b) (f c ~> f d1) -> Type) #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing (LiftA3Sym2 d2 d3) #
SuppressUnusedWarnings (LiftA3Sym2 a6989586621679563779 a6989586621679563778 :: TyFun (f6989586621679563378 b6989586621679563380) (f6989586621679563378 c6989586621679563381 ~> f6989586621679563378 d6989586621679563382) -> Type) #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods suppressUnusedWarnings :: () #
type Apply (LiftA3Sym2 a6989586621679563779 a6989586621679563778 :: TyFun (f6989586621679563378 b6989586621679563380) (f6989586621679563378 c6989586621679563381 ~> f6989586621679563378 d6989586621679563382) -> Type) (a6989586621679563780 :: f6989586621679563378 b6989586621679563380) #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal type Apply (LiftA3Sym2 a6989586621679563779 a6989586621679563778 :: TyFun (f6989586621679563378 b6989586621679563380) (f6989586621679563378 c6989586621679563381 ~> f6989586621679563378 d6989586621679563382) -> Type) (a6989586621679563780 :: f6989586621679563378 b6989586621679563380) = LiftA3Sym3 a6989586621679563779 a6989586621679563778 a6989586621679563780

data LiftA3Sym3 (a6989586621679563778 :: (~>) a6989586621679563379 ((~>) b6989586621679563380 ((~>) c6989586621679563381 d6989586621679563382))) (a6989586621679563779 :: f6989586621679563378 a6989586621679563379) (a6989586621679563780 :: f6989586621679563378 b6989586621679563380) :: (~>) (f6989586621679563378 c6989586621679563381) (f6989586621679563378 d6989586621679563382) #

Instances

(SApplicative f, SingI d2, SingI d3, SingI d4) => SingI (LiftA3Sym3 d2 d3 d4 :: TyFun (f c) (f d1) -> Type) #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing (LiftA3Sym3 d2 d3 d4) #
SuppressUnusedWarnings (LiftA3Sym3 a6989586621679563780 a6989586621679563779 a6989586621679563778 :: TyFun (f6989586621679563378 c6989586621679563381) (f6989586621679563378 d6989586621679563382) -> Type) #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods suppressUnusedWarnings :: () #
type Apply (LiftA3Sym3 a6989586621679563780 a6989586621679563779 a6989586621679563778 :: TyFun (f c) (f d) -> Type) (a6989586621679563781 :: f c) #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal type Apply (LiftA3Sym3 a6989586621679563780 a6989586621679563779 a6989586621679563778 :: TyFun (f c) (f d) -> Type) (a6989586621679563781 :: f c) = LiftA3 a6989586621679563780 a6989586621679563779 a6989586621679563778 a6989586621679563781

data OptionalSym0 :: forall a6989586621681250517 f6989586621681250516. (~>) (f6989586621681250516 a6989586621681250517) (f6989586621681250516 (Maybe a6989586621681250517)) #

Instances

SAlternative f => SingI (OptionalSym0 :: TyFun (f a) (f (Maybe a)) -> Type) #
Instance details Defined in Data.Singletons.Prelude.Applicative Methods sing :: Sing OptionalSym0 #
SuppressUnusedWarnings (OptionalSym0 :: TyFun (f6989586621681250516 a6989586621681250517) (f6989586621681250516 (Maybe a6989586621681250517)) -> Type) #
Instance details Defined in Data.Singletons.Prelude.Applicative Methods suppressUnusedWarnings :: () #
type Apply (OptionalSym0 :: TyFun (f a) (f (Maybe a)) -> Type) (a6989586621681250556 :: f a) #
Instance details Defined in Data.Singletons.Prelude.Applicative type Apply (OptionalSym0 :: TyFun (f a) (f (Maybe a)) -> Type) (a6989586621681250556 :: f a) = Optional a6989586621681250556

type OptionalSym1 (a6989586621681250556 :: f6989586621681250516 a6989586621681250517) = Optional a6989586621681250556 #

Orphan instances

SApplicative Down #
Instance details Methods sPure :: Sing t -> Sing (Apply PureSym0 t) # (%<>) :: Sing t -> Sing t -> Sing (Apply (Apply (<>@#@$) t) t) # sLiftA2 :: Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply LiftA2Sym0 t) t) t) # (%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) # (%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) #
PApplicative Down #
Instance details Associated Types type Pure arg :: f a # type arg <> arg :: f b # type LiftA2 arg arg arg :: f c # type arg > arg :: f b # type arg <* arg :: f a #
SMonoid a => SApplicative ((,) a) #
Instance details Methods sPure :: Sing t -> Sing (Apply PureSym0 t) # (%<>) :: Sing t -> Sing t -> Sing (Apply (Apply (<>@#@$) t) t) # sLiftA2 :: Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply LiftA2Sym0 t) t) t) # (%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) # (%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) #
PApplicative ((,) a) #
Instance details Associated Types type Pure arg :: f a # type arg <> arg :: f b # type LiftA2 arg arg arg :: f c # type arg > arg :: f b # type arg <* arg :: f a #

SAlternative f => SingI ((<\|>@#@$) :: TyFun (f a) (f a ~> f a) -> Type) #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing (<\|>@#@$) #
SuppressUnusedWarnings ((<\|>@#@$) :: TyFun (f6989586621679563504 a6989586621679563506) (f6989586621679563504 a6989586621679563506 ~> f6989586621679563504 a6989586621679563506) -> Type) #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods suppressUnusedWarnings :: () #
type Apply ((<\|>@#@$) :: TyFun (f6989586621679563504 a6989586621679563506) (f6989586621679563504 a6989586621679563506 ~> f6989586621679563504 a6989586621679563506) -> Type) (arg6989586621679563973 :: f6989586621679563504 a6989586621679563506) #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal type Apply ((<\|>@#@$) :: TyFun (f6989586621679563504 a6989586621679563506) (f6989586621679563504 a6989586621679563506 ~> f6989586621679563504 a6989586621679563506) -> Type) (arg6989586621679563973 :: f6989586621679563504 a6989586621679563506) = (<\|>@#@$$) arg6989586621679563973

(SAlternative f, SingI d) => SingI ((<\|>@#@$$) d :: TyFun (f a) (f a) -> Type) #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing ((<\|>@#@$$) d) #
SuppressUnusedWarnings ((<\|>@#@$$) arg6989586621679563973 :: TyFun (f6989586621679563504 a6989586621679563506) (f6989586621679563504 a6989586621679563506) -> Type) #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods suppressUnusedWarnings :: () #
type Apply ((<\|>@#@$$) arg6989586621679563973 :: TyFun (f a) (f a) -> Type) (arg6989586621679563974 :: f a) #
Instance details Defined in Data.Singletons.Prelude.Monad.Internal type Apply ((<\|>@#@$$) arg6989586621679563973 :: TyFun (f a) (f a) -> Type) (arg6989586621679563974 :: f a) = arg6989586621679563973 <\|> arg6989586621679563974