GHC does not check the functional dependency consistency condition correctly
Consider
{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies,
FlexibleInstances, UndecidableInstances,
ScopedTypeVariables #-}
class C x a b | a -> b where
op :: x -> a -> b
instance C Bool [x] [x]
instance C Char x y => C Char [x] [Maybe y]
f x = op True [x]
Should these two instance declarations be accepted? The two instances don't contradict each other, but neither do they agree as all published work on FDs says they should! They are inconsistent in the sense of Definition 6 of the FDs through CHRs paper.
Sadly GHC does not currently reject these as inconsistent. As a result it'll use both instance for improvement. In the definition of f
for example we get
C Bool [alpha] beta
where x:alpha
and the result type of f
is beta
. By using both instances for improvement we get
C Bool [Maybe gamma] [Maybe gamma]
That can be solved, so we get
f :: Maybe x -> [Maybe x]
But where did that Maybe
come from? It's really nothing to do with it.
Examples in the testsuite that exploit this loophole are
ghci/scripts ghci047
polykinds T9106
typecheck/should_compile FD4
typecheck/should_compile T7875
I'm not sure what the right thing here is.