GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2019-12-23T14:23:41Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/17267QuantifiedConstraints can prove anything with an infinite loop.2019-12-23T14:23:41ZJames PayorQuantifiedConstraints can prove anything with an infinite loop.## Initial foothold: `a ~ b => a ~ b`
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:
```haskell
{-# 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`:
```haskell
{-# 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)
```
## More generally: sidestepping the decidability checker, inhabiting any constraint with `<<loop>>`
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.## Initial foothold: `a ~ b => a ~ b`
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:
```haskell
{-# 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`:
```haskell
{-# 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)
```
## More generally: sidestepping the decidability checker, inhabiting any constraint with `<<loop>>`
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.8.10.1