#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 simonpj): I agree that much of this is not hard. And it's certainly useful. Indeed it is explicitly discussed in our Haskell Workshop 2000 paper [http://research.microsoft.com/en-us/um/people/simonpj/papers/derive.htm Derivable Type Classes]. The issues I see are: * Inference. If users can write such instances, they will probably expect them to be inferred. But that may wrongly defer a type error from a function to its call sites, by inferring an implication which is actually unsatisfiable. * Completeness. "Given" constraints interact with each other. How do "given" implications interact with simple "givens"? * Impredicativity. Can a constraint variable `c` be instantiated with one of these implications? Perhaps it's just a question of ruling that out. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/2256#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler