Documentation

There are three type classes that are relevant for the API in Logic.Ltl:

1. InterpretLtl mod m op

2. InterpretLtlHigherOrder mod m op

3. InterpretEffectStateful (Const [Ltl mod]) m op

For each of these classes, if you have an instance, there is a standard way to define instance(s) for the class(es) further down on the list. That is, in principle we could define

instance InterpretLtl mod m op => InterpretLtlHigherOrder mod m op

and

instance InterpretLtlHigherOrder mod m op => InterpretEffectStateful (Const [Ltl mod]) m op

However, we chose not do do this, and provide this macro instead, which defines the "missing" instances on a case-by-case basis. This is because sometimes you want to implement one of the classes further down the list, and do so generally, so that GHC won't be able to pick a most specific instance.

The macro relies on unification of instance heads: It will only generate instances which are strictly more specific than any pre-existing instance in current scope.