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.