[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):

 Does the following claim hold water and/or illuminate anything?

 The implication constraint on `implic` can either be simplified (eg `C a`
 immediately refines `a` and/or has `D a` as a superclass) or it is only
 satisfiable by a parametric instance of `D`. Suppose that overlapping and
 incoherent instances are not allowed. Then any non-parametric instance of
 `D` (eg your `D Int`) would immediately render that implication constraint
 unsatisfiable.

 So the concern is just yet another due solely to overlapping/incoherent
 instances?

 Replying to [comment:16 goldfire]:
 > * Inference: We don't. Just like we don't infer higher-rank types
 (which, of course, are the same as implication constraints). If a user
 wants this feature, they have to ask for it.
 >
 > * Completeness: This is thornier. Here is how I see a problem arising:
 >
 > {{{
 > class C a
 > class D a
 > instance D Int
 >
 > needsD :: D a => a -> ()
 > implic :: (forall a. C a => D a) -> ()
 > implic = needsD (5 :: Int)
 > }}}
 >
 >     When typechecking `implic`, the local universal dictionary for `D a`
 will be used to provide a dictionary to `needsD`. This will then generate
 an unsatisfiable wanted `C Int`. But, of course, we could have just used
 the global instance `D Int` instead.
 >
 >     An issue such as this one can't arise today (even with local
 dictionaries shadowing global ones) because local dictionaries never give
 rise to new wanteds. If you have a local dictionary, it's good to use.
 >
 >     Given/Given interactions would be the same. If one implication-Given
 can be used in an interaction, it would be, giving rise to its antecedent
 Wanted constraints.
 >
 >     This does get me a little worried about nondeterminism. But, I
 conjecture that if this interaction can give rise to nondeterminism, then
 it would be possible to exhibit the nondeterminism today, using
 overlapping instances.
 >
 >     So, it all comes down to specifying completeness against what spec,
 and I'm saying that we could be complete against a spec where every local
 constraint shadows every overlapped global one. That is, when `(forall a.
 C a => D a)` is in scope, `instance D Int` is not. Will this be easy
 enough to use to make it practicable? There will be some surprises around
 it, but I think it's all quite easy to digest with a little guidance.
 (Certainly easier to understand than closed type families!)
 >
 > * Impredicativity: This, to me, is just like the story in kind `*`. `c`
 should be forbidden from unifying with an implication constraint.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/2256#comment:26>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler