Fcf.Utils

Type-level error.

TypeError as a fcf.

Conjunction of a list of constraints.

Type equality.

Details

The base library also defines a similar (Type.Equality.==); it differs from TyEq in the following ways:

• TyEq is heterogeneous: its arguments may have different kinds;

• TyEq is reflexive: TyEq a a always reduces to True even if a is a variable.

A stuck type that can be used like a type-level undefined.

(Limited) equivalent of \case { .. } syntax. Supports matching of exact values (-->) and final matches for any value (Any) or for passing value to subcomputation (Else). Examples:

type BoolToNat = Case
  [ 'True  --> 0
  , 'False --> 1
  ]

type NatToBool = Case
  [ 0 --> 'False
  , Any   'True
  ]

type ZeroOneOrSucc = Case
  [ 0  --> 0
  , 1  --> 1
  , Else   ((+) 1)
  ]

Match concrete type in Case.

Match on predicate being successful with type in Case.

Match any type in Case. Should be used as a final branch.

Note: this identifier conflicts with Any (from Fcf.Class.Foldable) Any (from Data.Monoid), and Any (from GHC.Exts).

We recommend importing this one qualified.

Pass type being matched in Case to subcomputation. Should be used as a final branch.

Type-level If. If True a b ==> a; If False a b ==> b

A compile-time assert.

Raises the provided TypeError, whenever the condition evaluates to False.

Usage example: type ExampleAssertionFailure = Eval ( Pure '["foo", "bar"] >>= Length >>= Assert ('Text Assertion) (TyEq Int Void) )

Compile-time assert, with condition negated.

Raises the provided TypeError, whenever the condition evaluates to True.

Also see Assert.

A description of a custom type error.

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-existent 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.")