Type.Errors

A description of a custom type error.

Pretty print a list.

>>> :show_error PrettyPrintList '[Bool]...... 'Bool'...

>>> :show_error PrettyPrintList '[1, 2]...... '1', and '2'...

>>> :show_error PrettyPrintList '["hello", "world", "cool"]...... "hello", "world", and "cool"...

Like ShowType, but quotes the type if necessary.

>>> :show_error ShowTypeQuoted Int...... 'Int'...

>>> :show_error ShowTypeQuoted "symbols aren't quoted"...... "symbols aren't quoted"...

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

Error messages produced via TypeError are often too strict, and will be emitted sooner than you'd like. The solution is to use DelayError, which will switch the error messages to being consumed lazily.

>>> :{foo :: TypeError ('Text "Too eager; prevents compilation") => ()foo = ():}...... Too eager; prevents compilation...

>>> :{foo :: DelayError ('Text "Lazy; emitted on use") => ()foo = ():}

>>> foo...... Lazy; emitted on use...

Like DelayError, but implemented as a first-class family. DelayErrorFcf is useful when used as the last argument to IfStuck and UnlessStuck.

A helper definition that doesn't emit a type error. This is occassionally useful to leave as the residual constraint in IfStuck when you only want to observe if an expression isn't stuck.

Like NoError, but implemented as a first-class family. NoErrorFcf is useful when used as the last argument to IfStuck and UnlessStuck.

IfStuck expr b c leaves b in the residual constraints whenever expr is stuck, otherwise it Evaluates c.

Often you want to leave a DelayError in b in order to report an error when expr is stuck.

The c parameter is a first-class family, which allows you to perform arbitrarily-complicated type-level computations whenever expr isn't stuck. For example, you might want to produce a typeclass Constraint here. Alternatively, you can nest calls to IfStuck in order to do subsequent processing.

This is a generalization of kcsongor's Break machinery described in detecting the undetectable.

Like IfStuck, but specialized to the case when you don't want to do anything if expr isn't stuck.

>>> :{observe_no_rep    :: WhenStuck         (Rep t)         (DelayError ('Text "No Rep instance for " ':<>: ShowTypeQuoted t))    => t    -> ()observe_no_rep _ = ():}

>>> observe_no_rep HasNoRep...... No Rep instance for 'HasNoRep'...

>>> observe_no_rep True()

Like IfStuck, but leaves no residual constraint when expr is stuck. This can be used to ensure an expression isn't stuck before analyzing it further.

See the example under UnlessPhantom for an example of this use-case.

This library provides tools for performing lexical substitutions over types. For example, the function UnlessPhantom asks you to mark phantom variables via PHANTOM.

Unfortunately, this substitution cannot reliably be performed via type families, since it will too often get stuck. Instead we provide te, which is capable of reasoning about types symbolically.

Any type which comes with the warning "This type family is always stuck." must be used in the context of te and the magic [t| quasiquoter. To illustrate, the following is stuck:

>>> :{foo :: SubstVar VAR Boolfoo = True:}...... Couldn't match expected type ...SubstVar VAR Bool...... with actual type ...Bool......

But running it via te makes everything work:

>>> :{foo :: $(te[t| SubstVar VAR Bool |])foo = True:}

If you don't want to think about when to use te, it's a no-op when used with everyday types:

>>> :{bar :: $(te[t| Bool |])bar = True:}

This type family is always stuck. It must be used in the context of te.

A meta-variable for marking which argument should be a phantom when working with UnlessPhantom.

PHANTOM is polykinded and can be used in several settings.

See UnlessPhantom for examples.

This type family is always stuck. It must be used in the context of te.

UnlessPhantom expr err determines if the type described by expr is phantom in the variables marked via PHANTOM. If it's not, it produces the error message err.

For example, consider the definition:

>>> :{data Qux a b = Qux b:}

which is phantom in a:

>>> :eval_error $(te[t| UnlessPhantom (Qux PHANTOM Int) ('Text "Ok") |])()

but not in b:

>>> :eval_error $(te[t| UnlessPhantom (Qux Int PHANTOM) ('Text "Bad!") |])...... Bad!...

Unfortunately there is no known way to emit an error message if the variable is a phantom.

Often you'll want to guard UnlessPhantom against IfStuck, to ensure you don't get errors when things are merely ambiguous. You can do this by writing your own fcf whose implementation is UnlessPhantom:

>>> :{data NotPhantomErrorFcf :: k -> Exp Constrainttype instance Eval (NotPhantomErrorFcf f) =  $(te[t| UnlessPhantom (f PHANTOM)                        ( ShowTypeQuoted f                   ':<>: 'Text " is not phantom in its argument!")        |]):}

>>> :{observe_phantom    :: UnlessStuck         f         (NotPhantomErrorFcf f)    => f p    -> ()observe_phantom _ = ():}

We then notice that using observe_phantom against Proxy doesn't produce any errors, but against Maybe does:

>>> observe_phantom Proxy()

>>> observe_phantom (Just 5)...... 'Maybe' is not phantom in its argument!...

Finally, we leave observe_phantom unsaturated, and therefore f isn't yet known. Without guarding the UnlessPhantom behind UnlessStuck, this would incorrectly produce the message "f is not phantom in its argument!"

>>> observe_phantom...

This type family is always stuck. It must be used in the context of te.

Subst expr a b substitutes all instances of a for b in expr.

>>> :kind! $(te[t| Subst (Either Int Int) Int Bool |])...= Either Bool Bool

>>> :kind! $(te[t| Subst (Either Int Bool) Int [Char] |])...= Either [Char] Bool

>>> :kind! $(te[t| Subst (Either Int Bool) Either (,) |])...= (Int, Bool)

This type family is always stuck. It must be used in the context of te.

VAR is a meta-varaible which marks a substitution in SubstVar. The result of SubstVar expr val is expr[val/VAR].

VAR is polykinded and can be used in several settings.

See SubstVar for examples.

This type family is always stuck. It must be used in the context of te.

Like Subst, but uses the explicit meta-variable VAR to mark substitution points.

>>> :kind! $(te[t| SubstVar (Either VAR VAR) Bool |])...= Either Bool Bool

>>> :kind! $(te[t| SubstVar (Either VAR Bool) [Char] |])...= Either [Char] Bool

>>> :kind! $(te[t| SubstVar (VAR Int Bool) (,) |])...= (Int, Bool)

Kind of type-level expressions indexed by their result type.

Expression evaluator.