[GHC] #15359: Quantified constraints do not work with equality constraints

[GHC]

#15359: Quantified constraints do not work with equality constraints
-------------------------------------+-------------------------------------
        Reporter:  goldfire          |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:  8.6.1
       Component:  Compiler          |              Version:  8.5
      Resolution:                    |             Keywords:
                                     |  QuantifiedConstraints
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 AntC):

 Replying to [comment:6 simonpj]:
 >
 > Well, can you show me a quantified constraint with an equality in the
 head that is not useless?

 Remembering that this extension includes implication constraints, not only
 quantified, I can think of plenty. Here's one close to David's heart, per
 [https://mail.haskell.org/pipermail/ghc-devs/2017-November/015073.html
 this message]. "Reasoning backwards with type families". Suppose a class
 (rather than Type Family) for `And` over type-level Booleans: if we know
 the result is `True`, that gives an implication for the arguments:

 {{{
 class (c ~ 'True => a ~ 'True, c ~ 'True => b ~ 'True)
       => And (a :: Bool) (b :: Bool) (c :: Bool)
 }}}

 (And further implications would apply, per David's message. So this is a
 general technique for injectivity or partial/quasi-injectivity. Doesn't
 Richard's "fundamentally incomplete" apply here: there is not complete
 injectivity from result to arguments. So the implication `=>` says: ''if''
 the lhs constraint/equality holds, ''then'' you can use the rhs
 constraint/equality; otherwise (i.e. the lhs doesn't hold) the `=>` holds
 anyway.)

 Richard says
 >> any equality implication constraint is guaranteed to be redundant,
 because GHC can already deduce all equalities from whatever assumptions
 are at hand.

 For `And` that would need taking the instances as assumptions, **plus**
 making an assumption those are the only instances.

 Whereas my reading of the papers (seems I'm wrong) is that when
 `QuantifiedConstraints` sees those superclass constraints, it will assume
 them for type improvement, and verify they hold for each instance decl.

 >
 > Can you think of one that is?  I can't.

 If you want an example with quantification:

 {{{
 class (forall b'. C a b' => b' ~ b)
       => C a b  where ...
 }}}

 Which is more-or-less verbatim from the textbooks as a FOPL definition of
 ... a Functional Dependency -- that is, in relational database textbooks.
 And appears more-or-less verbatim in Mark P Jones papers on FunDeps and in
 the 'FDs through CHRs' paper.

 I'm talking about FOPL because the hs2017 paper (opening sentence) says

 "Quantified class constraints have been proposed many years ago to raise
 the expressive power of type classes from Horn clauses to first-order
 logic."

 That "proposed many years ago" cites your 2000 paper (with Ralf).

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15359#comment:7>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler