#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:11 goldfire]:
... I neither know a good pithy way of explaining that
I can't see even a convoluted explanation: it seems an arbitrary restriction. (Perhaps Simon is just being conservative with a new feature?) 1. Why is `~` banned, but not `Coercible` (or a user-written coercion class)? 2. In the 'FDs through CHRs' paper all of the improvement rules are in the form of a constraint implying an equality. 3. Richard's suggestion of a Closed Type Family (in a `~` superclass constraint -- which is a standard idiom) just is exactly what seems to be banned: {{{ class (F a b ~ c) -- there's the Eq constraint => D a b c where ... type family F a b where F blah1 blah2 = blah3 -- take '=' from left to right, so it's an implication F a (T a b') = (... b' ...) -- repeated tyvars on lhs is an '~' test -- local-scoped tyvar b' is quantified }}} "just is"? Well, no: I've had to chop up the logic and find a name for it and spread it round the program text.
Previously, Simon was worried that the equality constraints would always be redundant.
Hmm. Maybe redundant in the sense if you draw all the bits back together, the type equalities are entailed. But in the general case (such as my `And` example) that needs closed-world reasoning: closed Kinds; closed sets of instances. Which I don't expect GHC to even try.
I think that's still true in your examples, but with a key twist: the equality constraints can be used for improvement during type checking. That may indeed be correct.
As a practical matter though, I can't imagine how to implement them. And, given the fact that we have many ways of expressing these ideas already, without quantified equality constraints, (for example, your `ElimElem` could be implemented as a closed type family), I'm not yet motivated to start thinking about how to write a solver than can deal with
There's a risk of non-termination. But GHC entertains that already with `UndecidableInstances` and/or `UndecidableSuperClasses`. I think we could work up [https://github.com/ghc-proposals/ghc-proposals/pull/114 a proposal for that]. In the language of the 'FDs through CHRs' paper, we must make sure all quantification is 'range restricted'. these. Isn't "many ways" actually a problem here? Too many similar-but-subtly- different ways. And specifically Type Families are out of favour [https://github.com/ghc-proposals/ghc- proposals/pull/114#issuecomment-372124549 for certain purposes] (see re 'lens example' -- chop up the program logic, repeat it around the program, find a name for it; I think that also swayed the decision on records/`HasField` class to use FunDeps rather than TFs). Simon's (quite rightly) always looking for underpinning rationalisations that "allows us to simplify the language by (say) deprecating or removing features". Haskell has had a problem since at least 1997; didn't get fixed in H98; didn't get fixed in H2010; unlikely to get resolved for H2020: that we'd like to 'bless' MPTCs; but then we'd need to bless FunDeps and/or Type Families; but then we'd have to deal with overlaps/Closed TFs. All of them have an underlying type improvement logic, which is a 'local' implication constraint with equalities. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15359#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler