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