#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