#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