[GHC] #9627: Type error with functional dependencies

[GHC]

#9627: Type error with functional dependencies
-------------------------------------+-------------------------------------
        Reporter:  augustss          |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  7.8.3
  checker)                           |
      Resolution:                    |             Keywords:
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):

 (This ticket is the main motivation for
 [https://people.cs.kuleuven.be/~tom.schrijvers/Research/papers/haskell2017a.pdf
 this paper].)

 Replying to [comment:1 simonpj]:
 > Indeed.  Here is a more direct example: ...
 > From which we get ...

 What's frustrating in the example is that if we put an equation for `f`
 that gets the code to compile:

 {{{
 f _ = undefined
 }}}

 GHC (8.0 and Hugs way back in 2006) infer `f :: Bool -> Bool`.


 > Remember that GHC elaborates the program into System FC, generating
 evidence.
 >  * For functional dependencies I have no clue what evidence might look
 like.

 The short answer would be: whatever GHC is doing to improve to that
 signature, just make it evidence.

 Perhaps GHC is being cautious about selecting an instance for `C`: the
 wanted is `C Int b`; if it weren't for the FunDep, there could be other
 instances that match that; GHC is undependable in picking instances in
 presence of a dependency #15632. I tried with an instance more like the
 `FDs via CHRs` theory

 {{{
 instance (b ~ Bool) => C Int b
 }}}

 That instance head is exactly the wanted, but GHC gives the same
 behaviour.

 > If someone can explain how to elaborate functional dependencies into
 well-typed evidence in System FC, that would be good.  My inability to do
 so was one of the reasons we developed type families and System FC in the
 first place.
 >

 Aha! Does that "inability" date to before the `FDs via CHRs` 2006 paper?
 (The work on Assoc data types started 2005, that lead on to Type
 Families.)

 * One piece of evidence would be the improvement of the FunDep target
 arising from the constraint `(b ~ Bool)` on my recast instance.
 * One piece would be that that instance head exactly matches the wanted.
 * One piece would be that `~` constraint arises from the FunDep.

 A couple of complications:

 1. There might be multiple FunDeps, say

 {{{
 class C2 a b  | a -> b, b -> a
 }}}

    Then looking for evidence would have to treat instances as if:

 {{{
 instance C2 Int Bool

 instance   (b ~ Bool) => C2 Int b
          | (a ~ Int) => C2 a Bool
          | C2 Int Bool
 }}}

    (That's ''not'' any sort of proposal for syntax. I'm trying to express
 there are pseudo-instances arising from the FunDeps.)

    Those pseudo-instances overlap, but they're consistent with the
 FunDeps, according to the `FDs via CHRs` rules.

 2. Overlapping instances combined with FunDeps are already problematic.
 Again treating the target as a bare typevar with an `~` constraint,
 ''then'' considering overlaps in resulting substitution ordering seems to
 work ticket:15632#comment:2

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