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