Skip to content

GitLab

Closed
Opened by James Payor@jamespayor

QuantifiedConstraints can prove anything with an infinite loop.

Initial foothold: a ~ b => a ~ b

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)

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.

Edited by James Payor