[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:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  7.10.1
      Resolution:                    |             Keywords:  FunDeps
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by AntC):

 Thanks Iavor,

 * Yes the `C Char ...` instance is vacuous. I think GHC must accept it,
 because for all it knows there is some other instance decl for `C` that
 will provide a base case. That tells us we should be cautious if an
 instance (or set of instances) is accepted: the instances alone are weak
 evidence until/unless we can prove they can be inhabited.

 * I think what Simon's worried about is that the two instance decls have
 got entangled. And yet they don't overlap. So I'd be suspicious we'd see
 different behaviour under separate compilation.

 * Your instances for `F` break the FunDep coverage condition, so
 presumably you needed UndecidableInstances. What's reasonable to expect
 after that? I did get some types to inhabit those instances; and yes they
 were inconsistent with the Fundeps on `F`.

 * I guess GHC with UndecidableInstances sees there's a constraint on the
 instance (`G`, `H`), and that constraint carries a FunDep, so delegates
 the FunDep to it. We know GHC doesn't/can't chase round all the
 constraints, because it can't see all the instances. It delays that check
 to the use site -- but then that only considers the instances selected at
 that site.

 * Constraints like you've put are useful -- the type-level Type Equality
 test example. Arguably any such Type Equality test breaks '''Definition
 6''' Consistency condition.

 * Does your example actually do any harm anywhere? Could some distant
 module end up treating an Int as a Char/segfaulting?

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