Skip to content

GitLab

  • Menu
Projects Groups Snippets
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
  • Sign in / Register
  • GHC GHC
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
    • Locked Files
  • Issues 4,842
    • Issues 4,842
    • List
    • Boards
    • Service Desk
    • Milestones
    • Iterations
  • Merge requests 456
    • Merge requests 456
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
    • Test Cases
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • CI/CD
    • Code review
    • Insights
    • Issue
    • Repository
    • Value stream
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Glasgow Haskell Compiler
  • GHCGHC
  • Issues
  • #17267

Closed
Open
Created Sep 27, 2019 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 Sep 28, 2019 by James Payor
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking