#14822: -XQuantifiedConstraints: Turn term-level entailments (:-) into constraints (=>) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: | QuantifiedConstraints, wipT2893 Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by kcsongor): What would the conditions of generating such an implication constraint be? To me it seems like this would make use of the fact that the kind `Bool` is closed, and in theory, a constraint `forall (b :: Bool). C b` could be discharged by having an instance for `C 'True` and `C 'False`. Or in terms of implication constraints, that `forall (b :: Bool). C b => D b` could be built from the individual constituents. If my understanding is correct as written above, then I don't think it would make sense. When I see a quantified implication constraint, like `forall a. C a => D a`, I expect it to be parametric in `a`, which means that the solution of that constraint should be a function that uses the dictionary for `C a` to build the dictionary for `D a`, regardless of what `a` is instantiated to. (This expectation is grounded in the open world assumption.) For what it's worth, I think the question can be reformulated as whether the constraint `(forall a b. Funny a b)` should be solved based on your provided instances (to which I would answer no). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14822#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler