singletons-2.1: A framework for generating singleton types

Data.Promotion.Prelude.Maybe

Description

Defines promoted functions and datatypes relating to `Maybe`, including a promoted 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

# Promoted functions from `Data.Maybe`

maybe_ :: forall b a. b -> (a -> b) -> Maybe a -> b Source

type family Maybe_ a a a :: b Source

Equations

 Maybe_ n _z_1627800793 Nothing = n Maybe_ _z_1627800796 f (Just x) = Apply f x

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

type family IsJust a :: Bool Source

Equations

 IsJust Nothing = FalseSym0 IsJust (Just _z_1627802224) = TrueSym0

type family IsNothing a :: Bool Source

Equations

 IsNothing Nothing = TrueSym0 IsNothing (Just _z_1627802217) = FalseSym0

type family FromJust a :: a Source

Equations

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

type family FromMaybe a a :: a Source

Equations

 FromMaybe d x = Case_1627802204 d x x

type family MaybeToList a :: [a] Source

Equations

 MaybeToList Nothing = `[]` MaybeToList (Just x) = Apply (Apply (:\$) x) `[]`

type family ListToMaybe a :: Maybe a Source

Equations

 ListToMaybe `[]` = NothingSym0 ListToMaybe ((:) a _z_1627802185) = Apply JustSym0 a

type family CatMaybes a :: [a] Source

Equations

 CatMaybes `[]` = `[]` CatMaybes ((:) (Just x) xs) = Apply (Apply (:\$) x) (Apply CatMaybesSym0 xs) CatMaybes ((:) Nothing xs) = Apply CatMaybesSym0 xs

type family MapMaybe a a :: [b] Source

Equations

 MapMaybe _z_1627802137 `[]` = `[]` MapMaybe f ((:) x xs) = Case_1627802169 f x xs (Let1627802156Scrutinee_1627802126Sym3 f x xs)

# Defunctionalization symbols

data JustSym0 l Source

Instances

 SuppressUnusedWarnings (TyFun k (Maybe k) -> *) (JustSym0 k) Source type Apply (Maybe k) k (JustSym0 k) l0 = JustSym1 k l0 Source

type JustSym1 t = Just t Source

data Maybe_Sym0 l Source

Instances

 SuppressUnusedWarnings (TyFun k (TyFun (TyFun k k -> *) (TyFun (Maybe k) k -> *) -> *) -> *) (Maybe_Sym0 k k) Source type Apply (TyFun (TyFun k1 k -> *) (TyFun (Maybe k1) k -> *) -> *) k (Maybe_Sym0 k k1) l0 = Maybe_Sym1 k k1 l0 Source

data Maybe_Sym1 l l Source

Instances

 SuppressUnusedWarnings (k -> TyFun (TyFun k k -> *) (TyFun (Maybe k) k -> *) -> *) (Maybe_Sym1 k k) Source type Apply (TyFun (Maybe k) k1 -> *) (TyFun k k1 -> *) (Maybe_Sym1 k1 k l1) l0 = Maybe_Sym2 k1 k l1 l0 Source

data Maybe_Sym2 l l l Source

Instances

 SuppressUnusedWarnings (k -> (TyFun k k -> *) -> TyFun (Maybe k) k -> *) (Maybe_Sym2 k k) Source type Apply k (Maybe k1) (Maybe_Sym2 k k1 l1 l2) l0 = Maybe_Sym3 k k1 l1 l2 l0 Source

type Maybe_Sym3 t t t = Maybe_ t t t Source

data IsJustSym0 l Source

Instances

 SuppressUnusedWarnings (TyFun (Maybe k) Bool -> *) (IsJustSym0 k) Source type Apply Bool (Maybe k) (IsJustSym0 k) l0 = IsJustSym1 k l0 Source

data IsNothingSym0 l Source

Instances

 SuppressUnusedWarnings (TyFun (Maybe k) Bool -> *) (IsNothingSym0 k) Source type Apply Bool (Maybe k) (IsNothingSym0 k) l0 = IsNothingSym1 k l0 Source

data FromJustSym0 l Source

Instances

 SuppressUnusedWarnings (TyFun (Maybe k) k -> *) (FromJustSym0 k) Source type Apply k (Maybe k) (FromJustSym0 k) l0 = FromJustSym1 k l0 Source

data FromMaybeSym0 l Source

Instances

 SuppressUnusedWarnings (TyFun k (TyFun (Maybe k) k -> *) -> *) (FromMaybeSym0 k) Source type Apply (TyFun (Maybe k) k -> *) k (FromMaybeSym0 k) l0 = FromMaybeSym1 k l0 Source

data FromMaybeSym1 l l Source

Instances

 SuppressUnusedWarnings (k -> TyFun (Maybe k) k -> *) (FromMaybeSym1 k) Source type Apply k (Maybe k) (FromMaybeSym1 k l1) l0 = FromMaybeSym2 k l1 l0 Source

Instances

 SuppressUnusedWarnings (TyFun (Maybe k) [k] -> *) (MaybeToListSym0 k) Source type Apply [k] (Maybe k) (MaybeToListSym0 k) l0 = MaybeToListSym1 k l0 Source

Instances

 SuppressUnusedWarnings (TyFun [k] (Maybe k) -> *) (ListToMaybeSym0 k) Source type Apply (Maybe k) [k] (ListToMaybeSym0 k) l0 = ListToMaybeSym1 k l0 Source

data CatMaybesSym0 l Source

Instances

 SuppressUnusedWarnings (TyFun [Maybe k] [k] -> *) (CatMaybesSym0 k) Source type Apply [k] [Maybe k] (CatMaybesSym0 k) l0 = CatMaybesSym1 k l0 Source

data MapMaybeSym0 l Source

Instances

 SuppressUnusedWarnings (TyFun (TyFun k (Maybe k) -> *) (TyFun [k] [k] -> *) -> *) (MapMaybeSym0 k k) Source type Apply (TyFun [k] [k1] -> *) (TyFun k (Maybe k1) -> *) (MapMaybeSym0 k k1) l0 = MapMaybeSym1 k k1 l0 Source

data MapMaybeSym1 l l Source

Instances

 SuppressUnusedWarnings ((TyFun k (Maybe k) -> *) -> TyFun [k] [k] -> *) (MapMaybeSym1 k k) Source type Apply [k1] [k] (MapMaybeSym1 k k1 l1) l0 = MapMaybeSym2 k k1 l1 l0 Source