#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.p... this paper].) Replying to [comment:1 simonpj]:

Indeed. Here is a more direct example: ... From which we get ...

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

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

#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): Replying to [comment:4 simonpj]:

I think that

[https://people.cs.kuleuven.be/~tom.schrijvers/portfolio/haskell2017a.html Elaboration on functional dependencies] (Karachalias and Schrijvers, 2017) does he job nicely. Respectfully (to both the authors of the paper and to Simon): I disagree. The paper doesn't consider overlapping instances. (Neither did the `FDs via CHRs` paper.)

Indeed they use the above example in their motivation section. It describes how to translate fundeps into type families -- so the intermediate language is exactly System FC, as today.

I never implemented this, but if someone did then fundeps would acquire

(Yes I linked to the paper in comment:3.) Then how does System FC handle overlaps? Does it cope only with Closed Type Families? Then using System FC won't work for separate compilation of overlapping instances or instances that have the potential for overlap but are non-confluent (ref the Users Guide). Let me be careful to say that GHC's current implementation of these 'features' is more by accident than design. They can be used very powerfully; they can also very easily lead to incoherence and confusion. That's why I ref'd #15632. the same expressive power as type families. Hmm. There's different interpretations of "expressive power" in play here. Thanks to overlaps, I say FunDeps are ''more'' expressive than TFs: then I don't want FunDeps to be hobbled. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9627#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler