[GHC] #8634: Relax functional dependency coherence check ("liberal coverage condition")

[GHC]

#8634: Relax functional dependency coherence check ("liberal coverage condition")
-------------------------------------+-------------------------------------
              Reporter:  danilo2     |             Owner:
                  Type:  feature     |            Status:  new
  request                            |         Milestone:  7.10.1
              Priority:  high        |           Version:  7.7
             Component:  Compiler    |          Keywords:
            Resolution:              |  Operating System:  Unknown/Multiple
Differential Revisions:  Phab:D69    |   Type of failure:  None/Unknown
          Architecture:              |         Test Case:
  Unknown/Multiple                   |          Blocking:
            Difficulty:  Unknown     |
            Blocked By:              |
       Related Tickets:  #1241,      |
  #2247, #8356, #9103, #9227         |
-------------------------------------+-------------------------------------

Comment (by diatchki):

 comment:14 specifies what GHC is NOT going to do, but it does not specify
 what it will do!  As a programmer, when I see a class-declaration:
 {{{
 class C a b | a -> b
 }}}
 I think:  ''Aha, there is a functional relation between the parameters of
 this class.  This means that whenever the first parameters of instances
 are the same, so will be the second ones''. I don't know what this
 declaration means in the context of `Dysfunctional Dependencies`.

 I am also unclear about why `DysfunctionalDependencies` removes some of
 the consistency checks but not ``all``?   I believe that due to the
 current GHC implementation, "nothing will go wrong" even if we allowed
 instances such as `C Int Char` and `C Int Bool`, or am I missing
 something?

 All of this will change, however, if we were to complete the
 implementation of FDs and added support for using the FDs on given
 constraints: then type-safety actually depends on the consistency of the
 instances, and we better not have any `Dysfunctoinal Dependencies` around.





 Replying to [comment:25 simonpj]:
 > Martin, thanks.  Yes, as comment:14 specifies (fairly precisely I
 thought), `DysFunctionalDependencies` means relaxing the coverage
 condition altogether.
 >
 > Let me stress once more that, apparently contrary to your second bullet,
 dropping coverage does not threaten type soundness.  I'm not quite sure
 what you mean by "type safety".  I did actually go back to our JFP paper
 "Understanding functional dependencies using constraint handling rules" to
 see if I could find a concrete example of the problems that might arise,
 but all I could find I was the unsupported claim that "all is lost" if we
 don't have confluence.
 >
 > I ''believe'' (but I have no example that demonstrates) that dropping
 the Coverage Condition might mean that a small change in the program makes
 a large difference in whether the type inference algorithm succeeds.  But
 it would be good to have some concrete cases.  One way to gather some
 might be to allow it, and see whether our users start complaining about
 unpredicatable inference.
 >
 > Simon

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