I initially put this ticket into my internal notes as "Difficulty: Rocket Science", but I've changed my mind. I think this is actually straightforward to implement.
GHC already has implication constraints, except that they're effectively all Wanteds. So, all we would need are to be able to make Given implication constraints. But, these should be rather straightforward, because we can view top-level instances as Given implication constraints. We can just adapt the current look-in-Givens algorithm to do some matching, just like the instance-selection algorithm does. When we find an implication-constraint Given that matches a Wanted, we use it to solve the Wanted and then emit new Wanteds for the antecedents of the Given implication.
I was initially concerned about overlap here -- what if an implication Given's RHS overlaps with a global instance? -- but this was a red herring. Givens have always potentially overlapped with global instances, and very few people are bothered. For example:
{{{ min :: Ord a => a -> a -> a }}}
If we call `min` at type `Int`, the `Ord` constraint is potentially ambiguous: do we mean the dictionary supplied or the global `Ord Int` dictionary? Of course, we mean the local one, and we don't require `-XIncoherentInstances` to do so. So, worrying about overlap in the context of implication Givens is a red herring. We have a clear rule: local constraints always shadow global ones. That's nice, simple, and unsurprising.
This also doesn't change the "GHC never backtracks" principle. If a local implication-constraint's RHS matches, it is used, just like if GHC finds a global implication constraint (read, global constrained instance).
To implement this, GHC would also need to be able to produce the witness for an implication constraint, but this is just like inferring the lambdas for a higher-rank type. I don't see any challenge here.
Of course, a niggling feeling tells me that this ''has'' to be harder
#2256: Incompleteness of type inference: must quantify over implication constraints -------------------------------------+------------------------------------- Reporter: simonpj | Owner: simonpj Type: bug | Status: new Priority: lowest | Milestone: Component: Compiler (Type | Version: 6.8.2 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by nfrisby): Your `min` discussion was helpful to me, but I think it's mostly unrelated, in retrospect; the `Ord a` dictionary -- again ignoring overlapping/incoherent instances -- could only ever "overlap" with a parametric instance of `Ord`, since `a` is skolem. #9701, on the other hand, seems to demonstrate exactly what you were getting at (#12791 too?). Replying to [comment:14 goldfire]: than I'm seeing it. But, really, all I see standing in the way is a bit of plumbing.
Thoughts?
-- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/2256#comment:27 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler