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.