Way to scrutinize on unsatisfiable constraint

This is motivated by -fdefer-type-errors use, which is broken otherwise. But also to avoid using error, when GHC knows something is unreachable.

The prologue is not big:

{-# LANGUAGE GADTs, DataKinds, UndecidableInstances #-}
{-# OPTIONS -fdefer-type-errors #-}

import GHC.TypeLits

The non-sense Int ~ Char cases are also an example of unsatisfiable constraints, but the TypeError variant is actually something you run into in practice:

class Bar a where
    bar :: a

instance TypeError ('Text "No.") => Bar Int where
    bar = 42

One use case of above is to forbid some instance from existing. E.g. instance TypeError ('Text "ZipList cannot be made into Monad") => Monad ZipList where ....

Yet, with a small indirection:

*Main> let y = bar :: Int

<interactive>:10:9: warning: [-Wdeferred-type-errors]
    • No.
    • In the expression: bar :: Int
      In an equation for ‘y’: y = bar :: Int
*Main> y
42

We do get a warning, but code still runs.

For that we need to somehow explicitly(?) scrutinize on impossible context, or alternatively TypeErrord instances should not require any explicit implementations and implicit one created by GHC would throw the (deferred) TypeError, not No instance nor default method for class operation bar.

It would be nicer to have some special expression constuct (in a spirit of EmptyCase), to scrutinize dictionaries of impossible constraints. I don't know what that syntax could look like.

So what I want is to be able to write

instance TypeError ('Text "No.") => Bar Int where

which

1. won't give me a warning about unimplemented methods
2. with -fdefer-type-errors given methods will throw TypeError.

and a stretch goal is to have explicit syntax for these "default" implementations too.

While I can replace implementations with error "this shouldn't happen", and then that error will be forced, we are not able to recover an actual type-error in exception. That would be very useful for testing TypeError machinery. Real use case: https://github.com/well-typed/optics/issues/322