#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