Internal.Data.Basic.TypeLevel

Documentation

type family AllSatisfy (c :: k -> Constraint) (l :: [k]) :: Constraint where ...

Equations

AllSatisfy c '[] = ()

AllSatisfy c (x ': xs) = (c x, AllSatisfy c xs)

class MappableList l where

Minimal complete definition

mapTypeList

Methods

mapTypeList :: AllSatisfy c l => proxy1 c -> (forall proxy2 x. c x => proxy2 x -> a) -> proxy3 l -> [a]

Instances

MappableList k ([] k)

Methods

mapTypeList :: AllSatisfy [k] c l => proxy1 c -> (forall proxy2 x. c x => proxy2 x -> a) -> proxy3 l -> [a]

MappableList k ks => MappableList k ((:) k k1 ks)

Methods

mapTypeList :: AllSatisfy ((k ': k1) ks) c l => proxy1 c -> (forall proxy2 x. c x => proxy2 x -> a) -> proxy3 l -> [a]

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

Equations

Elem x '[] = False

Elem x (x ': xs) = True

Elem x (y ': xs) = Elem x xs

type family EqualOrError (a :: k) (b :: k) (err :: ErrorMessage) :: Constraint where ...

Equations

EqualOrError a a err = ()

EqualOrError a b err = TypeError err

type CheckWithError b err = EqualOrError b True err

type family Not (b :: Bool) where ...

Equations

Not True = False

Not False = True

type ErrorText = Text

type family xs ++ ys where ...

Equations

'[] ++ ys = ys

(x ': xs) ++ ys = x ': (xs ++ ys)

type family Without (xs :: [k]) (ys :: [k]) :: [k] where ...

Equations

Without xs '[] = xs

Without '[] ys = '[]

Without (x ': xs) ys = If (x `Elem` ys) (Without xs ys) (x ': Without xs ys)

type family IsSubset xs ys :: Constraint where ...

Equations

IsSubset '[] ys = ()

IsSubset (x ': xs) ys = (IsTrue (Elem x ys), IsSubset xs ys)

class c x => TypeSatisfies c x field

Instances

c x => TypeSatisfies c x field

type family OnMaybe (a :: k) (f :: b -> k) (m :: Maybe b) :: k where ...

Equations

OnMaybe a f (Just b) = f b

OnMaybe a f Nothing = a

class CheckWithError (NotMaybe a) (FieldNullErr field) => NotNull a field

Instances

CheckWithError (NotMaybe a) (FieldNullErr Symbol field) => NotNull a field

type family ListToTuple (f :: k -> *) (l :: [k]) where ...

Equations

ListToTuple f '[] = ()

ListToTuple f '[a] = f a

ListToTuple f '[a, b] = (f a, f b)

ListToTuple f '[a, b, c] = (f a, f b, f c)

ListToTuple f '[a, b, c, d] = (f a, f b, f c, f d)

ListToTuple f '[a, b, c, d, e] = (f a, f b, f c, f d, f e)

data ErrorMessage :: * where

A description of a custom type error.

Constructors

ShowType :: ErrorMessage

Pretty print the type. ShowType :: k -> ErrorMessage

(:<>:) :: ErrorMessage infixl 6

Put two pieces of error message next to each other.

(:$$:) :: ErrorMessage infixl 5

Stack two pieces of error message on top of each other.

type family TypeError b (a :: ErrorMessage) :: b where ...

The type-level equivalent of error.

The polymorphic kind of this type allows it to be used in several settings. For instance, it can be used as a constraint, e.g. to provide a better error message for a non-existant instance,

-- in a context
instance TypeError (Text "Cannot Show functions." :$$:
                    Text "Perhaps there is a missing argument?")
      => Show (a -> b) where
    showsPrec = error "unreachable"

It can also be placed on the right-hand side of a type-level function to provide an error for an invalid case,

type family ByteSize x where
   ByteSize Word16   = 2
   ByteSize Word8    = 1
   ByteSize a        = TypeError (Text "The type " :<>: ShowType a :<>:
                                  Text " is not exportable.")

Since: 4.9.0.0