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