[GHC] #2256: Incompleteness of type inference: must quantify over implication constraints

[GHC]

#2256: Incompleteness of type inference: must quantify over implication
constraints
-------------------------------------+-------------------------------------
              Reporter:  simonpj     |            Owner:  simonpj
                  Type:  bug         |           Status:  new
              Priority:  lowest      |        Milestone:  7.10.1
             Component:  Compiler    |          Version:  6.8.2
  (Type checker)                     |         Keywords:
            Resolution:              |     Architecture:  Unknown/Multiple
      Operating System:              |       Difficulty:  Unknown
  Unknown/Multiple                   |       Blocked By:
       Type of failure:  GHC         |  Related Tickets:
  rejects valid program              |
             Test Case:              |
              Blocking:              |
Differential Revisions:              |
-------------------------------------+-------------------------------------

Comment (by goldfire):

 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 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:14>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler