Hello cafe,
Is it possible in Haskell to check a lack of a certain constraint?
For example,
``` foo :: C => a foo = undefined
```
Here `foo` can only be compiled if called with C satisfied. How do I write the opposite, so that `foo` is only possible to use when C is not satisfied?
With best regards.
Indeed I found myself wanting this, too. Such a feature might reduce the amount of overlapping instances, but of course it bears the danger that others pointed out. For example, suppose you have a type T :: (* -> *) and the library author of T already defined an instance instance C a => C (T a). Now suppose you have a concrete type A which you know can never have a (lawful) C A instance, but you can define an instance C (T A). The latter would be formally overlapping with the former, even if you know that the former will never be implemented. Thus, instead of local non-satisfiability, a token for the proof that an instance can not exist might be more useful (and more safe). This would correspond to case 2 in Sylvain Henry's GHC proposal. I have no idea, however, how such a proof can be presented [*] in a way that can not be circumvented by a third author and lead to unsoundness. As a concrete example, I defined an instance MonadParsec (StateT String Maybe) which makes a wonderfully fast parser that you can swap in for a Megaparsec parser, but it is overlapping because of MonadParsec Maybe => MonadParsec (StateT s Maybe) although it is absurd to try to make Maybe an instance of MonadParsec. Another example: Think about why the mtl library has an instance MonadFoo m => MonadFoo (BarT m) for every pair (Foo,Bar) of transformers. (And there are quadratically many of these!) It is precisely because a catch-all instance like (MonadTrans t, MonadFoo m) => MonadFoo (t m) will be overlapping as long as we can't rule out MonadFoo (t m) by other means. Olaf [*] The logically natural way would be to have a Void constraint, so that we can say: MonadParsec Maybe => Void