type-spec- Type Level Specification by Example

Safe HaskellNone




A result type used in constraints inside TypeSpec to chain computations that may fail with a TypeError.


Results that with TypeErrors

type Result = Either ErrorMessage Source #

When a type level expectation is tested, it might be that compound expectations fail. In order to have a small, precise error message, the type level assertion results are made to have kind Result.

type FAILED = Left Source #

A nice alias for Right

type OK = Right Source #

A nice alias for Left

type family Try (e :: Result k) :: k where ... Source #

Return the result or fail with a TypeError


Try (OK (d :: k)) = d 
Try (FAILED m) = TypeError m 

type family DontTry (e :: Result r) :: Constraint where ... Source #

A constraint that is satisfied if the parameter is Left. Fails with a TypeError otherwise.


DontTry (FAILED e) = () 
DontTry (OK okIsNotOk) = TypeError ((Text "You specified this wasn't okay: " :$$: (Text " " :<>: ShowType okIsNotOk)) :$$: Text "... turns out it actually is!") 

Extending Error Messages

type family PrependToError (message :: ErrorMessage) (result :: Result a) :: Result a where ... Source #

In case of Left ErrorMessage prepend a message to the message, if the parameter was Right x just return Right x.


PrependToError message (OK x) = OK x 
PrependToError message (FAILED otherMessage) = FAILED (message :<>: otherMessage)