Generic.Data.Rep.Assert

Structural assertions on generic data representation.

Documentation

type family StripD1 a where ...

Equations

StripD1 (D1 _ a) = a

type GAssertNotVoid a = Assert (IsNotVoid (StripD1 (Rep a))) (GAssertErrorVoid a)

Type is not void i.e. has at least one constructor.

type family IsNotVoid a where ...

Equations

IsNotVoid V1 = False

IsNotVoid _ = True

type GAssertNotSum a = Assert (IsNotSum (StripD1 (Rep a))) (GAssertErrorSum a)

Type is not a sum type i.e. has at most one constructor.

Permits void types.

type family IsNotSum a where ...

Equations

IsNotSum (_ :+: _) = False

IsNotSum _ = True

type GAssertSum a = Assert (IsSum (StripD1 (Rep a))) (GAssertErrorNotSum a)

Type is a sum type i.e. has >=2 constructors.

Permits void types.

type family IsSum a where ...

Equations

IsSum (C1 _ _) = False

IsSum _ = True

type GAssertEnum a = Assert (IsEnum (StripD1 (Rep a))) (GAssertErrorNotEnum a)

Type has only empty constructors.

Permits void types.

type family IsEnum a where ...

Equations

IsEnum V1 = True

IsEnum (C1 _ a) = ConsIsEmpty a

IsEnum (l :+: r) = IsEnum l `And` IsEnum r

type family ConsIsEmpty a where ...

Equations

ConsIsEmpty U1 = True

ConsIsEmpty _ = False

type family And l r where ...

Type level boolean AND.

Equations

And True True = True

And _ _ = False