[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 simonpj):

 I think we are all agreed that type inference must be sound.  But, as
 mentioned above, "sound" for GHC means that
  * If the program passes the type checker, the elaborated Core program
 satisfies Core Lint.
  * If a program satisfies Core Lint, it enjoys preservation and progress
 (of the Core program); it cannot seg-fault.

 In operational terms I think the change proposed is well specified: look
 at comment:14, especially the user manual section and the three bullets at
 the end of the comment.  The question at issue is not soundness, but
 rather
  * Precisely which programs satisfy the type inference engine?
  * Is type inference complete? I.e. does it find a type for every program
 specified by the first bullet?
  * Is type inference robust?  I.e. can a small change in the program (e.g.
 swapping the order of arguments to a function) make the difference between
 type inference succeeding and failing?
  * Is the elaborated program coherent?  I.e. is it well specified what the
 result of running that program will be?

 The effect of `-XDysFunctionalDependencies` on these aspects of type
 inference is not well understood.  But it seems a much more benign form of
 allowing the programmer saying "trust me please" than `unsafeCoerce`, for
 example, because the soundness guarantee is not threatened.  The
 `-XUndecideableInstances` flag is somewhat similar, in that it continues
 to guarantee soundness, but allows type inference to diverge.

 This could perfectly well be a per-instance pragma, rather than a module-
 wide language extensions. Something like
 {{{
 instance {-# DYSFUNCTIONAL#-} Monad m => CTest X (m Int) where ...
 }}}
 That might be better, actually; it's more precisely targeted.

 Simon

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