Unsatisfiable

Unsatisfiable type class and plugin to empower it.

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 {}

plugin :: Plugin

To use this plugin add

{-# OPTIONS_GHC -fplugin=Unsatisfiable #-}

to your source file.

This plugin does two things:

Firstly, when there is wanted Unsatisfiable constraint, we pretty-pring its message. Unfortunately the actual No instance for (Unsatisfiable msg) error is also printed, as we don't solve it, except when -fdefer-type-errors is enabled. In that case unsatisfiable will throw an error with the rendered message.

Secondly, when Unsatisfiable constraint is given, all other constraints are solved automatically using unsatisfiable as the evidence. This is useful

class C a => D a
instance Unsatisfiable Msg => D Int  -- Note absence of C Int in the context

The motivation here is that if we use Unsatisfiable to ban an instance with a nice error message, we don't want to get extra error messages arising from failure to solve the superclass constraints, which we get if we are obliged to use

instance (Unsatisfiable Msg, C Int) => D Int

When GHC looks for valid type hole fits this plugin might print some errors. You may disable them with -fno-show-valid-hole-fits ghc option.