Runtime Loop from QuantifiedConstraints and UndecidableInstances
Summary
This might be an already known bug (I realise there are quite a few other GHC issues mentioning loops related to superclasses) but I am not getting any -Wloopy-superclass-solve
warnings GHC 9.6.2, which makes me think this is distinct from the cases in #20666 (closed).
Steps to reproduce
Run the following program (Haskell Playground: https://play.haskell.org/saved/Bt2c9wRx). Note there is no explicit recursion anywhere in the code.
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE UndecidableInstances #-}
import Data.Kind (Constraint)
class Bottom where
giveMeAString :: String
main :: IO ()
main = putStrLn (case veryBad of MkDict -> giveMeAString)
data Set = Empty | Russel
-- Note the perhaps more natural superclass constraints
-- `b ~ Empty => Bottom` or `forall t. In t Empty => Bottom`
-- do lead to loops at compile time
type In :: Set -> Set -> Constraint
class (In Russel Empty => Bottom) => In a b
instance (In t Russel, In t t) => In t Empty
instance (In t t => In t Empty) => In t Russel
data Dict a where
MkDict :: c => Dict c
bad :: Dict (In Russel Empty)
bad = MkDict
veryBad :: Dict Bottom
veryBad = case bad of MkDict -> MkDict
Expected behavior
Either loop at compile time or give a specific error message. Indeed GHC 9.4.7 outputs:
Main.hs:21:10: error:
• Could not deduce Bottom
arising from the superclasses of an instance declaration
from the context: In t t => In t 'Void
bound by the instance declaration at Main.hs:21:10-45
or from: In 'Russel 'Void
bound by a quantified context at Main.hs:21:10-45
Possible fix: add Bottom to the context of the instance declaration
• In the instance declaration for ‘In t 'Russel’
|
21 | instance (In t t => In t Void) => In t Russel
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Environment
- GHC versions used: 9.6.2 and 9.8.1-alpha