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

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