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

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
14 messages Options
Reply | Threaded
Open this post in threaded view
|

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

GHC - devs mailing list
#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
           Keywords:                 |  Operating System:  Unknown/Multiple
  QuantifiedConstraints              |
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 Feeling abusive toward GHC this morning, I tried this:

 {{{#!hs
 class C a b

 data Dict c where
   Dict :: c => Dict c

 foo :: (forall a b. C a b => a ~ b) => Dict (C a b) -> a -> b
 foo Dict x = x
 }}}

 I thought it wouldn't work, and I was right:

 {{{
     • Class ‘~’ does not support user-specified instances
     • In the quantified constraint ‘forall (a :: k) (b :: k).
                                     C a b =>
                                     a ~ b’
       In the type signature:
         foo :: (forall a b. C a b => a ~ b) => Dict (C a b) -> a -> b
 }}}

 Good. But then I tried something more devious:

 {{{#!hs
 class C a b
 class a ~ b => D a b

 data Dict c where
   Dict :: c => Dict c

 foo :: (forall a b. C a b => D a b) => Dict (C a b) -> a -> b
 foo Dict x = x
 }}}

 This also fails, with ` Couldn't match expected type ‘b’ with actual type
 ‘a’`.

 I'm fine with the second case failing (because I think anything else would
 be very challenging), but the error message is unfortunate. According to
 the semantics of class constraints and quantified constraints, this case
 should be accepted. So if we reject it, we should have a good reason --
 like we offer in the first case. Essentially, we need to explain that any
 logical entailment of an equality constraint simply doesn't hold in the
 presence of a quantified constraint. I neither know a good pithy way of
 explaining that to users nor how to detect when to do so.

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

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

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

GHC - devs mailing list
#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 RyanGlScott):

 It's very strange to me that we allow quantified `Coercible` constraints
 but not quantified `(~)` constraints. What is the rationale behind this
 decision choice?

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

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

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

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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 goldfire):

 Oh dear. I see trouble a-brewing.

 I agree that `Coercible` and `~` should either both be allowed or both be
 rejected. But the implications in my OP are unimplementable, I think. So
 I'm lost as to how to specify this.

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

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

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

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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:1 RyanGlScott]:
 > It's very strange to me that we allow quantified `Coercible` constraints
 but not quantified `(~)` constraints. What is the rationale behind this
 decision choice?

 Yes, I'm gravely disappointed to learn that: I've been posting lots of
 suggestions using `~` inside quantified (implication) constraints.
 {{{
     • Class ‘~’ does not support user-specified instances
 }}}

 Before there was `~`, there were plenty of ways for a user to specify a
 unifiability constraint -- see for example `TypeCast` in the HList paper.
 (Using bi-directional FunDeps.) And other examples of Quantified
 Constraints are using FunDeps for type improvement. So just do that
 instead of `~`?

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

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

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

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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 goldfire):

 Simon and I discussed this today. The lack of symmetry between `Coercible`
 and `~` here is by design. Essentially, any equality implication
 constraint is guaranteed to be redundant, because GHC can already deduce
 all equalities from whatever assumptions are at hand. On the other hand,
 `Coercible` implication constraints are quite useful, because coercibility
 is fundamentally incomplete.

 So the trouble I saw isn't so bad. But I still think we should document
 the restriction and report a better error message here.

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

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

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

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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:                    |
-------------------------------------+-------------------------------------
Changes (by dfeuer):

 * cc: dfeuer (added)


Comment:

 Redundant in what sense?

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

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

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

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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 simonpj):

 > Redundant in what sense?

 Well, can you show me a quantified constraint with an equality in the head
 that is not useless?

 For example what about this (by analogy with `Coercible`)
 {{{
 f :: forall m.
      (forall a b. a ~ b => m a ~ m b)
    => blah
 }}}
 No, that redundant. If we have `[W] t1 a ~ t2 b` there is a built-in rule
 to decompose it to `[W] t1 ~ t2` and `[W] a ~ b`.  (There is no such rule
 in general for `Coercible` which is why we need to allow it.)   So that
 quantified constraint wasn't useful.

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

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

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

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

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

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

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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 goldfire):

 All the examples in comment:7 involve superclass constraints, mostly on
 classes without any methods. This is interesting for type-level
 programming, but it's not clear where (even in type-level programming) the
 rubber is hitting the road here.

 Can you give a concrete example of a function that usefully uses an
 equality constraint in the head of an implication? This should be a
 function that I can call (that is, the constraints are satisfiable).

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

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

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

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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:8 goldfire]:         [replying in two instalments]
 > All the examples in comment:7 involve superclass constraints,

 ... because your ticket:15351#comment:5 tells me I don't even need
 instances declared.

 > mostly on classes without any methods. This is interesting for type-
 level programming,

 Yes the `And` example is for type-level programming. You haven't said
 those superclass constraints are redundant. Those implications/equalities
 can be derived from examining the instances; but a) needs reasoning from
 `Bool` being a closed type, b) needs reasoning from a closed set of
 instances.

 > but it's not clear where (even in type-level programming) the rubber is
 hitting the road here.
 >
 I don't expect GHC to be a general-purpose logic engine, so if we want
 type improvement per David's ghc-devs message "Reasoning backwards" --
 which seem eminently sensible, and improvements not achievable by
 injective Type Families (yet), why ''can't'' I use `QuantifiedConstraints`
 superclass? I could use similar for "Reasoning backwards" in type-level
 arithmetic over `Nat`: if a sum is `Z`, both arguments must be `Z`.

 As I said in comment:3, if it can't use `~`, there's plenty of ways to
 user-define an equivalent.

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

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

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

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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:8 goldfire]:          [2 of 2]

 Considering using quantified implications to emulate FunDeps -- because
 FunDeps are quantified implications.

 >  it's not clear where ... the rubber is hitting the road here.
 >

 Seeing the analogy between type improvement/multi-param type classes and
 relational theory was a great insight. But FunDeps is a clumsy mechanism.
 FunDeps and `OverlappingInstances` do not live happily together -- as all
 the theory says (and often need `UndecidableInstances`). FunDeps and
 superclass constraints calling Closed Type Families needs clunky machinery
 to concoct a CTF, give equations disconnected from the class, and still
 you're liable to need instances that look to GHC like they're overlapping.

 Then taking the hs2017 paper's "raise expressive power ... to first-order
 logic":

 * Superclass constraints with implications express more precisely the
 logic of the class.
 * Without an explicit FunDep, we avoid the 'FunDep consistency check',
 which is onerous and imprecise; and
 * anyway GHC's implementation is bogus -- as it needs to be, because
 FunDeps are imprecise.
 * Sometimes we can avoid `UndecidableInstances` or at least write
 instances that are less cluttered.

  > Can you give a concrete example of a function that usefully uses an
 equality constraint in the head of an implication? This should be a
 function that I can call (that is, the constraints are satisfiable).

 The class `C` above is emulating a regular FunDep; no reason it couldn't
 have methods. Here's something more ambitious (a classic litmus test of
 expressivity):

 {{{
 data HNil = HNil;    data HCons e l = HCons e l

 -- method to eliminate element 'e' from a heterogeneous list 'l'

 class ElimElem e l l'''  | e l -> l'''  where   -- here's the classic
 definition, with FunDep and overlaps
   elimElem :: e -> l -> l'''                    -- because overlaps, I
 can't use an Associated Type in the class

 instance ElimElem e HNil HNil  where
   elimElem _ HNil = HNil
 instance {-# OVERLAPPING #-} (ElimElem e l' l''')
          => ElimElem e (HCons e l') l''' where
   elimElem _x (HCons _ l') = elimElem _x l'

 -- instance (ElimElem e l' l''') => ElimElem e (HCons e' l') (HCons e'
 l''') where
                                                 -- wrong! instance head
 not strictly more general

 instance (ElimElem e l' l'', l''' ~ HCons e' ''')
          => ElimElem e (HCons e' l') l''' where
   elimElem _x (HCons y l') = HCons y (elimElem _x l')
 }}}

 I'd like to write that without FunDeps -- then can I use implications?

 {{{
 class (l ~ HNil => l''' ~ HNil,
        ( forall l'. l ~ HCons e l' => (ElimElem e l' l'''),
        ( forall e' l'. (l ~ HCons e' l', e /~ e') => (ElimElem e l' l'',
 l''' ~ HCons e' l'') )
       => ElimElem e l' l'''  where               -- no FunDep
         elimElem :: e -> l -> l'''

 -- HNil and HCons matching instances as above, but no OVERLAPPING

 instance (ElimElem e l' l'')
          => ElimElem e (HCons e' l') (HCons e' l'')  where
   elimElem _x (HCons y l') = HCons y (elimElem _x l')

 }}}

 Yes the two `HCons` instances might theoretically overlap (looking only at
 the instance heads) -- so again I can't use an Associated TF; but we never
 call elimElem at the intersection type, thanks to the type improvement
 applied from the superclass constraints. (I'd still prefer to make that
 explicit with an Apartness Guard ...)

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

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

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

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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 goldfire):

 As you point out, the last two instance always overlap looking only at the
 instance heads. So I think you'd still need `{-# OVERLAPPING #-}`.

 Previously, Simon was worried that the equality constraints would always
 be redundant. 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 these.

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

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

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

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

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

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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]:
 >  the last two instance always overlap looking only at the instance
 heads. So I think you'd still need `{-# OVERLAPPING #-}`.
 >

 Yeah kinda; but no. GHC's overlap is a marvel of engineering compromise.
 So you're not squinting at the right angle.

 * The two instances are in no substitution order, so
 `OVERLAPPING`/`OVERLAPPABLE` would be rejected.
 * "It is fine for there to be a ''potential'' of overlap ...; an error is
 only reported if a particular constraint matches more than one." [Users
 guide]
   So I'm relying on type improvement to apply before instance selection:
 then GHC should never be looking for a Wanted that matches more than one
 instance.

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

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets