* 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

#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]: 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