Test.TypeSpec.Internal.Result

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

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

A nice alias for Right

type OK = Right

A nice alias for Left

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

Return the result or fail with a TypeError

Equations

Try (OK (d :: k)) = d

Try (FAILED m) = TypeError m

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

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

Equations

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 ...

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

Equations

PrependToError message (OK x) = OK x

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