[GHC] #10675: GHC does not check the functional dependency consistency condition correctly

[GHC]

#10675: GHC does not check the functional dependency consistency condition
correctly
-------------------------------------+-------------------------------------
              Reporter:  simonpj     |             Owner:
                  Type:  bug         |            Status:  new
              Priority:  normal      |         Milestone:
             Component:  Compiler    |           Version:  7.10.1
              Keywords:              |  Operating System:  Unknown/Multiple
          Architecture:              |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
             Test Case:              |        Blocked By:
              Blocking:              |   Related Tickets:
Differential Revisions:              |
-------------------------------------+-------------------------------------
 Consider
 {{{
 {-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies,
              FlexibleInstances, UndecidableInstances,
              ScopedTypeVariables #-}

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

 instance                           C [x] [x]
 instance {-# OVERLAPS #-} C x y => C [x] [Maybe y]

 f x = op [x]
 }}}
 Should these two instance declarations be accepted?  They are simply
 ''inconsistent'' in the sense of Definition 6 of the
 [http://research.microsoft.com/en-us/um/people/simonpj/papers/fd-
 chr/jfp06.pdf 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 [alpha] beta
 }}}
 where `x:alpha` and the result type of `f` is `beta`.  By using both
 instances for improvement we get
 {{{
   C [Maybe gamma] [Maybe gamma]
 }}}
 Is that what we want?  The two instances don't ''contradict'' each other,
 but neither do they agree as all published work on FDs says they should!

 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.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/10675>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler