[GHC] #14822: -XQuantifiedConstraints: Turn term-level entailments (:-) into constraints (=>)

[GHC]

#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