[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
      Resolution:                    |                Keywords:
Operating System:  Unknown/Multiple  |            Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |               Test Case:
      Blocked By:                    |                Blocking:
 Related Tickets:                    |  Differential Revisions:
-------------------------------------+-------------------------------------
Description changed by simonpj:

Old description:

> 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.

New description:

 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
 [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 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.

--

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