Undecidable quantified superclass constraints aren’t rejected by the decidability checker
Summary
This small (albeit somewhat nonsensical) program using QuantifiedConstraints
causes the constraint solver to diverge:
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE TypeFamilies #-}
module QC where
class (forall c. C (F f c) c) => C f b where
type F f c :: * -> *
f :: (c -> b) -> F f c a -> f a
bar :: C f String => f ()
bar = f show undefined
src/QC.hs:1:1: error:
solveWanteds: too many iterations (limit = 100)
Unsolved: WC {wc_simple =
[WD] $dShow_a2mS {0}:: Show a0 (CDictCan)
[WD] $dIP_a3xb {0}:: ?callStack::GHC.Stack.Types.CallStack (CDictCan)}
Set limit with -fconstraint-solver-iterations=n; n=0 for no limit
|
1 | {-# LANGUAGE FlexibleContexts #-}
| ^
src/QC.hs:13:9: error:
• Could not deduce (Show a0) arising from a use of ‘show’
from the context: C f String
bound by the type signature for:
bar :: forall (f :: * -> *). C f String => f ()
at src/QC.hs:12:1-25
The type variable ‘a0’ is ambiguous
These potential instances exist:
instance Show Ordering -- Defined in ‘GHC.Show’
instance Show Integer -- Defined in ‘GHC.Show’
instance Show a => Show (Maybe a) -- Defined in ‘GHC.Show’
...plus 22 others
...plus 27 instances involving out-of-scope types
(use -fprint-potential-instances to see them all)
• In the first argument of ‘f’, namely ‘show’
In the expression: f show undefined
In an equation for ‘bar’: bar = f show undefined
|
13 | bar = f show undefined
| ^^^^
The above program is silly, and the reported error (that the Show
instance is ambiguous) is ultimately still correct, so who cares, right? But I actually have a slightly larger example that fails with the same error, even though I believe it is actually well-typed:
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE TypeFamilies #-}
module QCFunDep where
class (Applicative f, forall c. C (F f c) c) => C f b | f -> b where
type F f c :: * -> *
f :: (c -> b) -> F f c a -> f a
foo :: C f Integer => f ()
foo = pure ()
bar :: C f String => f ()
bar = f show foo
I think the second program might fail to typecheck because of #15351, so that issue might not be new. Either way, it seems like the solver diverging is something that shouldn’t happen, so this report is really about that.
Environment
- GHC version used: 8.6.5
- Operating System: macOS 10.14.5 (18F132)
- System Architecture: x86_64