## QuantifiedConstraints can prove anything with an infinite loop.

##
`a ~ b => a ~ b`

Initial foothold: The following is with GHC `8.8.1`

.

Issue #15316 considers a case of loopy `k => k`

implications. The solution there was to reject functions like `f : (k => k) => (k => r) -> r`

on the grounds of `k => k`

not looking like a decidable instance. GHC does now complain about those, but the problem remains.

Consider this example:

```
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE TypeFamilies #-} -- for equational constraints
unsafeCoerce :: a -> b
unsafeCoerce = oops where
oops :: (a ~ b => a ~ b) => a -> b
oops a = a
main :: IO ()
main = unsafeCoerce "Hello!"
```

The checks to avoid loopiness aren't firing, and it compiles.
The example above at runtime outputs `Oops: <<loop>>`

. However, I can modify it so that the compiler erases the infinite loop, to get a true `unsafeCoerce`

:

```
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
class a ~ b => Thing a b
instance a ~ b => Thing a b
unsafeCoerce :: forall a b. a -> b
unsafeCoerce a = oops a where
oops :: (a ~ b => Thing a b) => (Thing a b => r) -> r
oops r = r
main :: IO ()
main = unsafeCoerce "Hello!"
```

Compiling with `-O0`

gives:

```
[1 of 1] Compiling Main ( Oops.hs, Oops.o ) [Optimisation flags changed]
ghc: panic! (the 'impossible' happened)
(GHC version 8.8.1 for x86_64-apple-darwin):
primRepCmmType:VoidRep
```

...and with `-O2`

the program crashes at runtime:

```
[1 of 1] Compiling Main ( Oops.hs, Oops.o )
Linking Oops ...
Oops: internal error: stg_ap_v_ret
(GHC version 8.8.1 for x86_64_apple_darwin)
Please report this as a GHC bug: https://www.haskell.org/ghc/reportabug
fish: './Oops' terminated by signal SIGABRT (Abort)
```

##
`<<loop>>`

More generally: sidestepping the decidability checker, inhabiting any constraint with Here's a simple example for getting a `Show (IO ())`

"instance", which will just be a loop.

```
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
class Show a => Thing a b
instance Show a => Thing a b
pseudoShow :: (Show a => Thing a ()) => a -> String
pseudoShow = show
main :: IO ()
main = putStrLn $ pseudoShow main
```

## My take on what's going on

If you just try to use `Show a => Show a`

or `Show a => Thing a`

, GHC will complain and demand `UndecidableInstances`

. But this is easy to sidestep, if one just has `Show a => Thing a b`

, because `Thing a b`

is a bigger instance head...

Even if you only ever add smaller and smaller instance heads to your wanteds, the problem is that you started off by saying "I need `Show a`

, and fortunately that's a superclass of `Thing a ()`

- so all I need is to provide a `Show a`

instance". And rapidly you have a loop.