#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