QuantifiedConstraints can prove anything with an infinite loop.
a ~ b => a ~ b
Initial foothold: The following is with GHC 8.8.1
.
Issue #15316 (closed) 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.