singletons-2.6: A framework for generating singleton types

Copyright | (C) 2013-2014 Richard Eisenberg Jan Stolarek
License | BSD-style (see LICENSE)
Maintainer | Ryan Scott
Stability | experimental
Portability | non-portable
Safe Haskell | None
Language | Haskell2010

Data.Singletons.Prelude.Maybe

Contents

- Singletons from `Data.Maybe`
- Defunctionalization symbols

Description

Defines functions and datatypes relating to the singleton for `Maybe`, including a singletons version of all the definitions in `Data.Maybe`.

Because many of these definitions are produced by Template Haskell, it is not possible to create proper Haddock documentation. Please look up the corresponding operation in `Data.Maybe`. Also, please excuse the apparent repeated variable names. This is due to an interaction between Template Haskell and Haddock.

Synopsis

- type family Sing :: k -> Type
- data SMaybe :: forall a. Maybe a -> Type where
  - SNothing :: SMaybe 'Nothing
  - SJust :: forall a (n :: a). (Sing (n :: a)) -> SMaybe ('Just n)
- maybe_ :: b -> (a -> b) -> Maybe a -> b
- type family Maybe_ (a :: b) (a :: (~>) a b) (a :: Maybe a) :: b where ...
- sMaybe_ :: forall b a (t :: b) (t :: (~>) a b) (t :: Maybe a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply Maybe_Sym0 t) t) t :: b)
- type family IsJust (a :: Maybe a) :: Bool where ...
- sIsJust :: forall a (t :: Maybe a). Sing t -> Sing (Apply IsJustSym0 t :: Bool)
- type family IsNothing (a :: Maybe a) :: Bool where ...
- sIsNothing :: forall a (t :: Maybe a). Sing t -> Sing (Apply IsNothingSym0 t :: Bool)
- type family FromJust (a :: Maybe a) :: a where ...
- sFromJust :: forall a (t :: Maybe a). Sing t -> Sing (Apply FromJustSym0 t :: a)
- type family FromMaybe (a :: a) (a :: Maybe a) :: a where ...
- sFromMaybe :: forall a (t :: a) (t :: Maybe a). Sing t -> Sing t -> Sing (Apply (Apply FromMaybeSym0 t) t :: a)
- type family ListToMaybe (a :: [a]) :: Maybe a where ...
- sListToMaybe :: forall a (t :: [a]). Sing t -> Sing (Apply ListToMaybeSym0 t :: Maybe a)
- type family MaybeToList (a :: Maybe a) :: [a] where ...
- sMaybeToList :: forall a (t :: Maybe a). Sing t -> Sing (Apply MaybeToListSym0 t :: [a])
- type family CatMaybes (a :: [Maybe a]) :: [a] where ...
- sCatMaybes :: forall a (t :: [Maybe a]). Sing t -> Sing (Apply CatMaybesSym0 t :: [a])
- type family MapMaybe (a :: (~>) a (Maybe b)) (a :: [a]) :: [b] where ...
- sMapMaybe :: forall a b (t :: (~>) a (Maybe b)) (t :: [a]). Sing t -> Sing t -> Sing (Apply (Apply MapMaybeSym0 t) t :: [b])
- type NothingSym0 = 'Nothing
- data JustSym0 :: forall (a3530822107858468865 :: Type). (~>) a3530822107858468865 (Maybe (a3530822107858468865 :: Type))
- type JustSym1 (t6989586621679310904 :: a3530822107858468865) = 'Just t6989586621679310904
- data Maybe_Sym0 :: forall b6989586621679510991 a6989586621679510992. (~>) b6989586621679510991 ((~>) ((~>) a6989586621679510992 b6989586621679510991) ((~>) (Maybe a6989586621679510992) b6989586621679510991))
- data Maybe_Sym1 (a6989586621679511009 :: b6989586621679510991) :: forall a6989586621679510992. (~>) ((~>) a6989586621679510992 b6989586621679510991) ((~>) (Maybe a6989586621679510992) b6989586621679510991)
- data Maybe_Sym2 (a6989586621679511009 :: b6989586621679510991) (a6989586621679511010 :: (~>) a6989586621679510992 b6989586621679510991) :: (~>) (Maybe a6989586621679510992) b6989586621679510991
- type Maybe_Sym3 (a6989586621679511009 :: b6989586621679510991) (a6989586621679511010 :: (~>) a6989586621679510992 b6989586621679510991) (a6989586621679511011 :: Maybe a6989586621679510992) = Maybe_ a6989586621679511009 a6989586621679511010 a6989586621679511011
- data IsJustSym0 :: forall a6989586621679512421. (~>) (Maybe a6989586621679512421) Bool
- type IsJustSym1 (a6989586621679512619 :: Maybe a6989586621679512421) = IsJust a6989586621679512619
- data IsNothingSym0 :: forall a6989586621679512420. (~>) (Maybe a6989586621679512420) Bool
- type IsNothingSym1 (a6989586621679512617 :: Maybe a6989586621679512420) = IsNothing a6989586621679512617
- data FromJustSym0 :: forall a6989586621679512419. (~>) (Maybe a6989586621679512419) a6989586621679512419
- type FromJustSym1 (a6989586621679512614 :: Maybe a6989586621679512419) = FromJust a6989586621679512614
- data FromMaybeSym0 :: forall a6989586621679512418. (~>) a6989586621679512418 ((~>) (Maybe a6989586621679512418) a6989586621679512418)
- data FromMaybeSym1 (a6989586621679512604 :: a6989586621679512418) :: (~>) (Maybe a6989586621679512418) a6989586621679512418
- type FromMaybeSym2 (a6989586621679512604 :: a6989586621679512418) (a6989586621679512605 :: Maybe a6989586621679512418) = FromMaybe a6989586621679512604 a6989586621679512605
- data ListToMaybeSym0 :: forall a6989586621679512416. (~>) [a6989586621679512416] (Maybe a6989586621679512416)
- type ListToMaybeSym1 (a6989586621679512598 :: [a6989586621679512416]) = ListToMaybe a6989586621679512598
- data MaybeToListSym0 :: forall a6989586621679512417. (~>) (Maybe a6989586621679512417) [a6989586621679512417]
- type MaybeToListSym1 (a6989586621679512601 :: Maybe a6989586621679512417) = MaybeToList a6989586621679512601
- data CatMaybesSym0 :: forall a6989586621679512415. (~>) [Maybe a6989586621679512415] [a6989586621679512415]
- type CatMaybesSym1 (a6989586621679512593 :: [Maybe a6989586621679512415]) = CatMaybes a6989586621679512593
- data MapMaybeSym0 :: forall a6989586621679512413 b6989586621679512414. (~>) ((~>) a6989586621679512413 (Maybe b6989586621679512414)) ((~>) [a6989586621679512413] [b6989586621679512414])
- data MapMaybeSym1 (a6989586621679512574 :: (~>) a6989586621679512413 (Maybe b6989586621679512414)) :: (~>) [a6989586621679512413] [b6989586621679512414]
- type MapMaybeSym2 (a6989586621679512574 :: (~>) a6989586621679512413 (Maybe b6989586621679512414)) (a6989586621679512575 :: [a6989586621679512413]) = MapMaybe a6989586621679512574 a6989586621679512575

# Documentation

type family Sing :: k -> Type Source #

The singleton kind-indexed type family.

#### Instances

Instances details

type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = SBool
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = SOrdering
type Sing Source # |
Instance details Defined in Data.Singletons.TypeLits.Internal type Sing = SNat
type Sing Source # |
Instance details Defined in Data.Singletons.TypeLits.Internal type Sing = SSymbol
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = STuple0
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = SVoid
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SAll
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SAny
type Sing Source # |
Instance details Defined in Data.Singletons.TypeError type Sing = SErrorMessage
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = SList :: [a] -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = SMaybe :: Maybe a -> Type

type Sing Source #

A choice of singleton for the kind ``TYPE` rep` (for some `RuntimeRep` `rep`), an instantiation of which is the famous kind `Type`.

Conceivably, one could generalize this instance to `Sing @k` for any kind `k`, and remove all other `Sing` instances. We don't adopt this design, however, since it is far more convenient in practice to work with explicit singleton values than `TypeRep`s (for instance, `TypeRep`s are more difficult to pattern match on, and require extra runtime checks).

We cannot produce explicit singleton values for everything in ``TYPE` rep`, however, since it is an open kind, so we reach for `TypeRep` in this one particular case.

Instance details Defined in Data.Singletons.TypeRepTYPE type Sing = TypeRep :: TYPE rep -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = SNonEmpty :: NonEmpty a -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Ord type Sing = SDown :: Down a -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = SIdentity :: Identity a -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SFirst :: First a -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SLast :: Last a -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SMax :: Max a -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SMin :: Min a -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SOption :: Option a -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SWrappedMonoid :: WrappedMonoid m -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SDual :: Dual a -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SProduct :: Product a -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SSum :: Sum a -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Monoid type Sing = SFirst :: First a -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Monoid type Sing = SLast :: Last a -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = SEither :: Either a b -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = STuple2 :: (a, b) -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Internal type Sing = SLambda :: (k1 ~> k2) -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Internal type Sing = SWrappedSing :: WrappedSing a -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup type Sing = SArg :: Arg a b -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Sigma type Sing = SSigma :: Sigma s t -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = STuple3 :: (a, b, c) -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Const type Sing = SConst :: Const a b -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = STuple4 :: (a, b, c, d) -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = STuple5 :: (a, b, c, d, e) -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = STuple6 :: (a, b, c, d, e, f) -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = STuple7 :: (a, b, c, d, e, f, g) -> Type

data SMaybe :: forall a. Maybe a -> Type where Source #

Constructors

SNothing :: SMaybe 'Nothing |
SJust :: forall a (n :: a). (Sing (n :: a)) -> SMaybe ('Just n) |

#### Instances

Instances details

SDecide a => TestCoercion (SMaybe :: Maybe a -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Instances Methods testCoercion :: forall (a0 :: k) (b :: k). SMaybe a0 -> SMaybe b -> Maybe (Coercion a0 b)
SDecide a => TestEquality (SMaybe :: Maybe a -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Instances Methods testEquality :: forall (a0 :: k) (b :: k). SMaybe a0 -> SMaybe b -> Maybe (a0 :~: b)
ShowSing a => Show (SMaybe z) |
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> SMaybe z -> ShowS show :: SMaybe z -> String showList :: [SMaybe z] -> ShowS

# Singletons from `Data.Maybe`

maybe_ :: b -> (a -> b) -> Maybe a -> b Source #

type family Maybe_ (a :: b) (a :: (~>) a b) (a :: Maybe a) :: b where ... Source #

Equations

Maybe_ n _ 'Nothing = n |
Maybe_ _ f ('Just x) = Apply f x |

sMaybe_ :: forall b a (t :: b) (t :: (~>) a b) (t :: Maybe a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply Maybe_Sym0 t) t) t :: b) Source #

The preceding two definitions are derived from the function `maybe` in `Data.Maybe`. The extra underscore is to avoid name clashes with the type `Maybe`.

type family IsJust (a :: Maybe a) :: Bool where ... Source #

Equations

IsJust 'Nothing = FalseSym0 |
IsJust ('Just _) = TrueSym0 |

sIsJust :: forall a (t :: Maybe a). Sing t -> Sing (Apply IsJustSym0 t :: Bool) Source #

type family IsNothing (a :: Maybe a) :: Bool where ... Source #

Equations

IsNothing 'Nothing = TrueSym0 |
IsNothing ('Just _) = FalseSym0 |

sIsNothing :: forall a (t :: Maybe a). Sing t -> Sing (Apply IsNothingSym0 t :: Bool) Source #

type family FromJust (a :: Maybe a) :: a where ... Source #

Equations

FromJust 'Nothing = Apply ErrorSym0 "Maybe.fromJust: Nothing" |
FromJust ('Just x) = x |

sFromJust :: forall a (t :: Maybe a). Sing t -> Sing (Apply FromJustSym0 t :: a) Source #

type family FromMaybe (a :: a) (a :: Maybe a) :: a where ... Source #

Equations

FromMaybe d x = Case_6989586621679512610 d x x |

sFromMaybe :: forall a (t :: a) (t :: Maybe a). Sing t -> Sing t -> Sing (Apply (Apply FromMaybeSym0 t) t :: a) Source #

type family ListToMaybe (a :: [a]) :: Maybe a where ... Source #

Equations

ListToMaybe '[] = NothingSym0 |
ListToMaybe ('(:) a _) = Apply JustSym0 a |

sListToMaybe :: forall a (t :: [a]). Sing t -> Sing (Apply ListToMaybeSym0 t :: Maybe a) Source #

type family MaybeToList (a :: Maybe a) :: [a] where ... Source #

Equations

MaybeToList 'Nothing = '[] |
MaybeToList ('Just x) = Apply (Apply (:@#@$) x) '[] |

sMaybeToList :: forall a (t :: Maybe a). Sing t -> Sing (Apply MaybeToListSym0 t :: [a]) Source #

type family CatMaybes (a :: [Maybe a]) :: [a] where ... Source #

Equations

CatMaybes '[] = '[] |
CatMaybes ('(:) ('Just x) xs) = Apply (Apply (:@#@$) x) (Apply CatMaybesSym0 xs) |
CatMaybes ('(:) 'Nothing xs) = Apply CatMaybesSym0 xs |

sCatMaybes :: forall a (t :: [Maybe a]). Sing t -> Sing (Apply CatMaybesSym0 t :: [a]) Source #

type family MapMaybe (a :: (~>) a (Maybe b)) (a :: [a]) :: [b] where ... Source #

Equations

MapMaybe _ '[] = '[] |
MapMaybe f ('(:) x xs) = Case_6989586621679512589 f x xs (Let6989586621679512585Scrutinee_6989586621679512448Sym3 f x xs) |

sMapMaybe :: forall a b (t :: (~>) a (Maybe b)) (t :: [a]). Sing t -> Sing t -> Sing (Apply (Apply MapMaybeSym0 t) t :: [b]) Source #

# Defunctionalization symbols

type NothingSym0 = 'Nothing Source #

data JustSym0 :: forall (a3530822107858468865 :: Type). (~>) a3530822107858468865 (Maybe (a3530822107858468865 :: Type)) Source #

#### Instances

Instances details

SingI (JustSym0 :: TyFun a (Maybe a) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing JustSym0 Source #
SuppressUnusedWarnings (JustSym0 :: TyFun a3530822107858468865 (Maybe a3530822107858468865) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Instances Methods suppressUnusedWarnings :: () Source #
type Apply (JustSym0 :: TyFun a (Maybe a) -> Type) (t6989586621679310904 :: a) Source # |
Instance details Defined in Data.Singletons.Prelude.Instances type Apply (JustSym0 :: TyFun a (Maybe a) -> Type) (t6989586621679310904 :: a) = 'Just t6989586621679310904

type JustSym1 (t6989586621679310904 :: a3530822107858468865) = 'Just t6989586621679310904 Source #

data Maybe_Sym0 :: forall b6989586621679510991 a6989586621679510992. (~>) b6989586621679510991 ((~>) ((~>) a6989586621679510992 b6989586621679510991) ((~>) (Maybe a6989586621679510992) b6989586621679510991)) Source #

#### Instances

Instances details

SingI (Maybe_Sym0 :: TyFun b ((a ~> b) ~> (Maybe a ~> b)) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Maybe Methods sing :: Sing Maybe_Sym0 Source #
SuppressUnusedWarnings (Maybe_Sym0 :: TyFun b6989586621679510991 ((a6989586621679510992 ~> b6989586621679510991) ~> (Maybe a6989586621679510992 ~> b6989586621679510991)) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Maybe Methods suppressUnusedWarnings :: () Source #
type Apply (Maybe_Sym0 :: TyFun b6989586621679510991 ((a6989586621679510992 ~> b6989586621679510991) ~> (Maybe a6989586621679510992 ~> b6989586621679510991)) -> Type) (a6989586621679511009 :: b6989586621679510991) Source # |

Instance details

Defined in Data.Singletons.Prelude.Maybe

type Apply (Maybe_Sym0 :: TyFun b6989586621679510991 ((a6989586621679510992 ~> b6989586621679510991) ~> (Maybe a6989586621679510992 ~> b6989586621679510991)) -> Type) (a6989586621679511009 :: b6989586621679510991) = Maybe_Sym1 a6989586621679511009 a6989586621679510992 :: TyFun (a6989586621679510992 ~> b6989586621679510991) (Maybe a6989586621679510992 ~> b6989586621679510991) -> Type

data Maybe_Sym1 (a6989586621679511009 :: b6989586621679510991) :: forall a6989586621679510992. (~>) ((~>) a6989586621679510992 b6989586621679510991) ((~>) (Maybe a6989586621679510992) b6989586621679510991) Source #

#### Instances

Instances details

SingI d => SingI (Maybe_Sym1 d a :: TyFun (a ~> b) (Maybe a ~> b) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Maybe Methods sing :: Sing (Maybe_Sym1 d a) Source #
SuppressUnusedWarnings (Maybe_Sym1 a6989586621679511009 a6989586621679510992 :: TyFun (a6989586621679510992 ~> b6989586621679510991) (Maybe a6989586621679510992 ~> b6989586621679510991) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Maybe Methods suppressUnusedWarnings :: () Source #
type Apply (Maybe_Sym1 a6989586621679511009 a6989586621679510992 :: TyFun (a6989586621679510992 ~> b6989586621679510991) (Maybe a6989586621679510992 ~> b6989586621679510991) -> Type) (a6989586621679511010 :: a6989586621679510992 ~> b6989586621679510991) Source # |
Instance details Defined in Data.Singletons.Prelude.Maybe type Apply (Maybe_Sym1 a6989586621679511009 a6989586621679510992 :: TyFun (a6989586621679510992 ~> b6989586621679510991) (Maybe a6989586621679510992 ~> b6989586621679510991) -> Type) (a6989586621679511010 :: a6989586621679510992 ~> b6989586621679510991) = Maybe_Sym2 a6989586621679511009 a6989586621679511010

data Maybe_Sym2 (a6989586621679511009 :: b6989586621679510991) (a6989586621679511010 :: (~>) a6989586621679510992 b6989586621679510991) :: (~>) (Maybe a6989586621679510992) b6989586621679510991 Source #

#### Instances

Instances details

(SingI d1, SingI d2) => SingI (Maybe_Sym2 d1 d2 :: TyFun (Maybe a) b -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Maybe Methods sing :: Sing (Maybe_Sym2 d1 d2) Source #
SuppressUnusedWarnings (Maybe_Sym2 a6989586621679511010 a6989586621679511009 :: TyFun (Maybe a6989586621679510992) b6989586621679510991 -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Maybe Methods suppressUnusedWarnings :: () Source #
type Apply (Maybe_Sym2 a6989586621679511010 a6989586621679511009 :: TyFun (Maybe a) b -> Type) (a6989586621679511011 :: Maybe a) Source # |
Instance details Defined in Data.Singletons.Prelude.Maybe type Apply (Maybe_Sym2 a6989586621679511010 a6989586621679511009 :: TyFun (Maybe a) b -> Type) (a6989586621679511011 :: Maybe a) = Maybe_ a6989586621679511010 a6989586621679511009 a6989586621679511011

type Maybe_Sym3 (a6989586621679511009 :: b6989586621679510991) (a6989586621679511010 :: (~>) a6989586621679510992 b6989586621679510991) (a6989586621679511011 :: Maybe a6989586621679510992) = Maybe_ a6989586621679511009 a6989586621679511010 a6989586621679511011 Source #

data IsJustSym0 :: forall a6989586621679512421. (~>) (Maybe a6989586621679512421) Bool Source #

#### Instances

Instances details

SingI (IsJustSym0 :: TyFun (Maybe a) Bool -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Maybe Methods sing :: Sing IsJustSym0 Source #
SuppressUnusedWarnings (IsJustSym0 :: TyFun (Maybe a6989586621679512421) Bool -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Maybe Methods suppressUnusedWarnings :: () Source #
type Apply (IsJustSym0 :: TyFun (Maybe a) Bool -> Type) (a6989586621679512619 :: Maybe a) Source # |
Instance details Defined in Data.Singletons.Prelude.Maybe type Apply (IsJustSym0 :: TyFun (Maybe a) Bool -> Type) (a6989586621679512619 :: Maybe a) = IsJust a6989586621679512619

type IsJustSym1 (a6989586621679512619 :: Maybe a6989586621679512421) = IsJust a6989586621679512619 Source #

data IsNothingSym0 :: forall a6989586621679512420. (~>) (Maybe a6989586621679512420) Bool Source #

#### Instances

Instances details

SingI (IsNothingSym0 :: TyFun (Maybe a) Bool -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Maybe Methods sing :: Sing IsNothingSym0 Source #
SuppressUnusedWarnings (IsNothingSym0 :: TyFun (Maybe a6989586621679512420) Bool -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Maybe Methods suppressUnusedWarnings :: () Source #
type Apply (IsNothingSym0 :: TyFun (Maybe a) Bool -> Type) (a6989586621679512617 :: Maybe a) Source # |
Instance details Defined in Data.Singletons.Prelude.Maybe type Apply (IsNothingSym0 :: TyFun (Maybe a) Bool -> Type) (a6989586621679512617 :: Maybe a) = IsNothing a6989586621679512617

type IsNothingSym1 (a6989586621679512617 :: Maybe a6989586621679512420) = IsNothing a6989586621679512617 Source #

data FromJustSym0 :: forall a6989586621679512419. (~>) (Maybe a6989586621679512419) a6989586621679512419 Source #

#### Instances

Instances details

SingI (FromJustSym0 :: TyFun (Maybe a) a -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Maybe Methods sing :: Sing FromJustSym0 Source #
SuppressUnusedWarnings (FromJustSym0 :: TyFun (Maybe a6989586621679512419) a6989586621679512419 -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Maybe Methods suppressUnusedWarnings :: () Source #
type Apply (FromJustSym0 :: TyFun (Maybe a) a -> Type) (a6989586621679512614 :: Maybe a) Source # |
Instance details Defined in Data.Singletons.Prelude.Maybe type Apply (FromJustSym0 :: TyFun (Maybe a) a -> Type) (a6989586621679512614 :: Maybe a) = FromJust a6989586621679512614

type FromJustSym1 (a6989586621679512614 :: Maybe a6989586621679512419) = FromJust a6989586621679512614 Source #

data FromMaybeSym0 :: forall a6989586621679512418. (~>) a6989586621679512418 ((~>) (Maybe a6989586621679512418) a6989586621679512418) Source #

#### Instances

Instances details

SingI (FromMaybeSym0 :: TyFun a (Maybe a ~> a) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Maybe Methods sing :: Sing FromMaybeSym0 Source #
SuppressUnusedWarnings (FromMaybeSym0 :: TyFun a6989586621679512418 (Maybe a6989586621679512418 ~> a6989586621679512418) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Maybe Methods suppressUnusedWarnings :: () Source #
type Apply (FromMaybeSym0 :: TyFun a6989586621679512418 (Maybe a6989586621679512418 ~> a6989586621679512418) -> Type) (a6989586621679512604 :: a6989586621679512418) Source # |
Instance details Defined in Data.Singletons.Prelude.Maybe type Apply (FromMaybeSym0 :: TyFun a6989586621679512418 (Maybe a6989586621679512418 ~> a6989586621679512418) -> Type) (a6989586621679512604 :: a6989586621679512418) = FromMaybeSym1 a6989586621679512604

data FromMaybeSym1 (a6989586621679512604 :: a6989586621679512418) :: (~>) (Maybe a6989586621679512418) a6989586621679512418 Source #

#### Instances

Instances details

SingI d => SingI (FromMaybeSym1 d :: TyFun (Maybe a) a -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Maybe Methods sing :: Sing (FromMaybeSym1 d) Source #
SuppressUnusedWarnings (FromMaybeSym1 a6989586621679512604 :: TyFun (Maybe a6989586621679512418) a6989586621679512418 -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Maybe Methods suppressUnusedWarnings :: () Source #
type Apply (FromMaybeSym1 a6989586621679512604 :: TyFun (Maybe a) a -> Type) (a6989586621679512605 :: Maybe a) Source # |
Instance details Defined in Data.Singletons.Prelude.Maybe type Apply (FromMaybeSym1 a6989586621679512604 :: TyFun (Maybe a) a -> Type) (a6989586621679512605 :: Maybe a) = FromMaybe a6989586621679512604 a6989586621679512605

type FromMaybeSym2 (a6989586621679512604 :: a6989586621679512418) (a6989586621679512605 :: Maybe a6989586621679512418) = FromMaybe a6989586621679512604 a6989586621679512605 Source #

data ListToMaybeSym0 :: forall a6989586621679512416. (~>) [a6989586621679512416] (Maybe a6989586621679512416) Source #

#### Instances

Instances details

SingI (ListToMaybeSym0 :: TyFun [a] (Maybe a) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Maybe Methods sing :: Sing ListToMaybeSym0 Source #
SuppressUnusedWarnings (ListToMaybeSym0 :: TyFun [a6989586621679512416] (Maybe a6989586621679512416) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Maybe Methods suppressUnusedWarnings :: () Source #
type Apply (ListToMaybeSym0 :: TyFun [a] (Maybe a) -> Type) (a6989586621679512598 :: [a]) Source # |
Instance details Defined in Data.Singletons.Prelude.Maybe type Apply (ListToMaybeSym0 :: TyFun [a] (Maybe a) -> Type) (a6989586621679512598 :: [a]) = ListToMaybe a6989586621679512598

type ListToMaybeSym1 (a6989586621679512598 :: [a6989586621679512416]) = ListToMaybe a6989586621679512598 Source #

data MaybeToListSym0 :: forall a6989586621679512417. (~>) (Maybe a6989586621679512417) [a6989586621679512417] Source #

#### Instances

Instances details

SingI (MaybeToListSym0 :: TyFun (Maybe a) [a] -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Maybe Methods sing :: Sing MaybeToListSym0 Source #
SuppressUnusedWarnings (MaybeToListSym0 :: TyFun (Maybe a6989586621679512417) [a6989586621679512417] -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Maybe Methods suppressUnusedWarnings :: () Source #
type Apply (MaybeToListSym0 :: TyFun (Maybe a) [a] -> Type) (a6989586621679512601 :: Maybe a) Source # |
Instance details Defined in Data.Singletons.Prelude.Maybe type Apply (MaybeToListSym0 :: TyFun (Maybe a) [a] -> Type) (a6989586621679512601 :: Maybe a) = MaybeToList a6989586621679512601

type MaybeToListSym1 (a6989586621679512601 :: Maybe a6989586621679512417) = MaybeToList a6989586621679512601 Source #

data CatMaybesSym0 :: forall a6989586621679512415. (~>) [Maybe a6989586621679512415] [a6989586621679512415] Source #

#### Instances

Instances details

SingI (CatMaybesSym0 :: TyFun [Maybe a] [a] -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Maybe Methods sing :: Sing CatMaybesSym0 Source #
SuppressUnusedWarnings (CatMaybesSym0 :: TyFun [Maybe a6989586621679512415] [a6989586621679512415] -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Maybe Methods suppressUnusedWarnings :: () Source #
type Apply (CatMaybesSym0 :: TyFun [Maybe a] [a] -> Type) (a6989586621679512593 :: [Maybe a]) Source # |
Instance details Defined in Data.Singletons.Prelude.Maybe type Apply (CatMaybesSym0 :: TyFun [Maybe a] [a] -> Type) (a6989586621679512593 :: [Maybe a]) = CatMaybes a6989586621679512593

type CatMaybesSym1 (a6989586621679512593 :: [Maybe a6989586621679512415]) = CatMaybes a6989586621679512593 Source #

data MapMaybeSym0 :: forall a6989586621679512413 b6989586621679512414. (~>) ((~>) a6989586621679512413 (Maybe b6989586621679512414)) ((~>) [a6989586621679512413] [b6989586621679512414]) Source #

#### Instances

Instances details

SingI (MapMaybeSym0 :: TyFun (a ~> Maybe b) ([a] ~> [b]) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Maybe Methods sing :: Sing MapMaybeSym0 Source #
SuppressUnusedWarnings (MapMaybeSym0 :: TyFun (a6989586621679512413 ~> Maybe b6989586621679512414) ([a6989586621679512413] ~> [b6989586621679512414]) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Maybe Methods suppressUnusedWarnings :: () Source #
type Apply (MapMaybeSym0 :: TyFun (a6989586621679512413 ~> Maybe b6989586621679512414) ([a6989586621679512413] ~> [b6989586621679512414]) -> Type) (a6989586621679512574 :: a6989586621679512413 ~> Maybe b6989586621679512414) Source # |
Instance details Defined in Data.Singletons.Prelude.Maybe type Apply (MapMaybeSym0 :: TyFun (a6989586621679512413 ~> Maybe b6989586621679512414) ([a6989586621679512413] ~> [b6989586621679512414]) -> Type) (a6989586621679512574 :: a6989586621679512413 ~> Maybe b6989586621679512414) = MapMaybeSym1 a6989586621679512574

data MapMaybeSym1 (a6989586621679512574 :: (~>) a6989586621679512413 (Maybe b6989586621679512414)) :: (~>) [a6989586621679512413] [b6989586621679512414] Source #

#### Instances

Instances details

SingI d => SingI (MapMaybeSym1 d :: TyFun [a] [b] -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Maybe Methods sing :: Sing (MapMaybeSym1 d) Source #
SuppressUnusedWarnings (MapMaybeSym1 a6989586621679512574 :: TyFun [a6989586621679512413] [b6989586621679512414] -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Maybe Methods suppressUnusedWarnings :: () Source #
type Apply (MapMaybeSym1 a6989586621679512574 :: TyFun [a] [b] -> Type) (a6989586621679512575 :: [a]) Source # |
Instance details Defined in Data.Singletons.Prelude.Maybe type Apply (MapMaybeSym1 a6989586621679512574 :: TyFun [a] [b] -> Type) (a6989586621679512575 :: [a]) = MapMaybe a6989586621679512574 a6989586621679512575

type MapMaybeSym2 (a6989586621679512574 :: (~>) a6989586621679512413 (Maybe b6989586621679512414)) (a6989586621679512575 :: [a6989586621679512413]) = MapMaybe a6989586621679512574 a6989586621679512575 Source #