Bogus no_fixed_dependencies test in pickQuantifiablePreds

Consider this module:

{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-}
module Foo where

class C a b c | b -> c where
  op :: a -> b -> c

bar1 :: C a Int Char => a -> Char
bar1 x = op x (3 :: Int) :: Char

bar2 x = op x (3 :: Int) :: Char

bar1 is accepted by GHC 9.6, but bar2 is rejected:

Foo.hs:11:10: error: [GHC-39999]
    • No instance for ‘C a Int Char’ arising from a use of ‘op’
    • In the expression: op x (3 :: Int) :: Char
      In an equation for ‘bar2’: bar2 x = op x (3 :: Int) :: Char

Why?

Look in GHC.Tc.Solver, Note [Do not quantify over constraints that determine a variable]. The acual test is

    no_fixed_dependencies cls tys
      = and [ qtvs `intersectsVarSet` tyCoVarsOfTypes fd_lhs_tys
            | fd <- cls_fds
            , let (fd_lhs_tys, _) = instFD fd cls_tvs tys ]
      where
        (cls_tvs, cls_fds) = classTvsFds cls

So when inferring bar2's type we have the constraint [W] C alpha Int Char, where we are planning to quantify over alpha. That should be absolutely fine. But bizarrely the no_fixed_dependencies test decides not to quantify over this constraint on the grounds that there is a fundep b -> c whose LHS (here just Int) does not mention a quantified variable.

Utterly wrong. And in fact this is why we mysteriously do not quantify over the Add (T m) m2 Int) constraint in #22194 (closed), see this comment.