Documentation

Equality constraint in form of a typeclass.

A type family to compute Boolean equality.

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

Append for type-level lists. We use this synonym instead of using the one from Data.Vinyl.TypeLevel directly because the latter is missing a fixity declaration. See the vinyl pull request.

Remove all occurences of the given element.

Difference between two lists.

Constrain two types to be equal, and produce an error message if they are found not to be.

>>> :k! FailUnlessEqual Int Int ('Text "This should not result in a failure")
FailUnlessEqual Int Int ('Text "This should not result in a failure") :: Constraint
= (() :: Constraint, Int ~ Int)

>>> :k! FailUnlessEqual Bool Int ('Text "This should result in a failure")
FailUnlessEqual Bool Int ('Text "This should result in a failure") :: Constraint
= ((TypeError ...), Bool ~ Int)

Constrain two types to be equal. If they are found not to be, produce an error message. If they are shown to be equal, impose an additional given constraint.

>>> :k! FailUnlessEqualElse Int Int ('Text "This should not result in a failure") ()
FailUnlessEqualElse Int Int ('Text "This should not result in a failure") () :: Constraint
= (() :: Constraint, Int ~ Int)

>>> :k! FailUnlessEqualElse Bool Int ('Text "This should result in a failure") ()
FailUnlessEqualElse Bool Int ('Text "This should result in a failure") () :: Constraint
= ((TypeError ...), Bool ~ Int)

the ~ constraint might seem redundant, but, without it, GHC would reject

>>> :{
foo :: FailUnlessEqualElse a b ('Text "MyError") () => a -> b
foo = id
:}

GHC needs to "see" the type equality ~ in order to actually "learn" something from a type family's result.

We use DefaultEq here, rather than ==, so this will work with type variables known to be equal, even if nothing is known about them concretely. For example, the following will compile:

>>> :{
foo :: FailUnlessEqualElse a b ('Text "MyError") () => a -> b
foo x = x
--
bar :: a -> a
bar = foo
:}

If we used (==), then bar would be rejected.

(==) has its place (see the comments below it in Data.Type.Equality) but I don't think it has anything to offer us here. In particular, the equality constraint we bundle up seems to win us all the reasoning power that (==) would provide and more. The following adaptation of the example in the Data.Type.Equality comments compiles:

>>> :{
foo :: FailUnlessEqualElse (Maybe a) (Maybe b) ('Text "yo") ()
       :- FailUnlessEqualElse a b ('Text "heya") ()
foo = Sub Dict
:}

In this example, the entire consequent follows from the equality constraint in the antecedent; the FailUnlessElsePoly part of it is irrelevant, so we don't need to be able to reason from it. If we were reasoning solely using (==), foo would be rejected because the error messages are different.

Fail with given error if the condition holds.

A version of FailWhenElsePoly that imposes an equality constraint on its Bool argument.

Fail with given error if the condition does not hold. Otherwise, return the third argument.

Fail with given error if the condition does not hold.

A version of FailUnlessElsePoly that imposes an equality constraint on its Bool argument.

Fail with given error if the condition does not hold. Otherwise, return the third argument.

Bring type-level list at term-level using given function to demote its individual elements.

Make sure given type is evaluated. This type family fits only for types of Type kind.

Similar to SingI [], but does not require individual elements to be also instance of SingI.

Data.List.Singletons.SList analogue for KnownList.

Split a record into two pieces.

A value of type parametrized with some type parameter.

Utility function to help transform the first argument of a binfunctor.

Given a type-level list that is SingI, construct evidence that it is also a KnownList. Note that KnownList is weaker, hence this construction is always possible.