Unsatisfiable.Class

Unsatisfiable type-class.

Documentation

class Unsatisfiable (msg :: ErrorMessage)

Unsatisfiable type-class.

This a common idiom, to have a type-class with a non-exported member. This class cannot be ever instantiated, and we can use it to "forbid" some instances from existence, by defining an instance with unsatisfiable constraint.

The unsatisfiable acts as better undefined, using this type-class constraint.

The behaviour of this class would be rather better defined than instantiating the polymorphic TypeError to kind Constraint, because it is clear when to report the custom error: instead of an unsolved constraint error, when the constraint solver fails to solve a wanted Unsatisfiable msg.

The custom error reporting is done using plugin type-checker plugin.

See discussion in GHC#18310.

There are some examples of using this class and plugin at https://github.com/phadej/unsatisfiable/tree/master/unsatisfiable-examples/examples

Minimal complete definition

unsatisfiable_

unsatisfiable :: forall msg a. Unsatisfiable msg => a

See Unsatisfiable.

If you need some other TYPE, you can use case trick by instantiating unsatisfiable to Void and using EmptyCase.

case unsatisfiable @msg @Void of {}