[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: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.
 >

 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'.

 > 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
 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