Negative reasoning for type classes to make better errors

Rust has skirted the edge with various aspects of type classes. In particular, per https://github.com/Ixrec/rust-orphan-rules/issues/1 there have been various explorations of "negative reasoning" and revises orphan rules. (Rust doesn't allow orphans, and uses its orphans to ensure there are no overlaps (except for "specialization" but let's ignore that for now).

One big idea here is that while regular contexts depending on "anti-constraints" is pretty bogus (except for perhaps not equal constraints), there is no reason while top level assertions, that are completely erased, cannot be negative. Indeed, orphan and overlap rules can be phrased in terms somewhat like that (if condition....something is *not* allowed).

Why do I bring this up? I am thinking it may be useful to make errors better without baking in ad-hoc logic into GHC or removing expressive power.

For example, inspired by the recent https://www.thecodedmessage.com/posts/haskell-gripe/, take
```haskell
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE OverloadedLists #-}
1 + [1]
```
this program is deeply unconstrained, and could perhaps be well typed in all sorts of stupid ways.
But if we could write a declaration like
```haskell
assert !(Num a, IsList a)
````
to assert no type has both number and list literals, we can in fact rule out the program, with a nice error, e.g something like
```
No type 'a' satisfying
1 :: a
[1] :: a
(+) :: a -> a -> a
in expression
1 + [1]
no types are both list-like and number-like
```

Besides trying to keep brittle ad-hoc logic out of GHC, I think it quite a subjective matter whether one should provide assertions like this---I would *not* put such assertions in `base`. Instead, I would advocate they be just in custom preludes, especially for teaching. This would be a small step towards "teaching languages".

Note that since `assert !(Num a, IsList a)` is erased / has no computation interpretation, there is no risk of programs "relying" on this in any ways. It simply makes more programs ill-typed. Instances are always exported, but assertions like this can safely not be. Teaching prelude modules would of course export them for downstream student use, but any user is free to write their own that just effects the local module and nothing else.