[Haskell-cafe] Check a lack of a constraint?

[Olaf Klinke]

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