[GHC] #2893: Implement "Quantified contexts" proposal

GHC ghc-devs at haskell.org
Sat Aug 20 22:01:14 UTC 2016


#2893: Implement "Quantified contexts" proposal
-------------------------------------+-------------------------------------
        Reporter:  porges            |                Owner:
            Type:  feature request   |               Status:  new
        Priority:  normal            |            Milestone:  ⊥
       Component:  Compiler          |              Version:  6.10.1
      Resolution:                    |             Keywords:  proposal
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):

 Iceland_jack, there are two problems with using typeclasses like these to
 "solve" this problem:

 1. They're based on explicit `Dict` values. As a result, using them
 requires lots of pattern matching and type variable scoping hullabaloo,
 which gets annoying pretty quickly.
 2. What does it mean to automatically generate instances for `(:=>)`? Do
 we only generate instances that correspond to actual instance contexts? If
 so, then the following would typecheck, since there is an `instance () :=>
 Eq ()`:

    {{{#!hs
    ins :: () :- Eq ()
    }}}

    But the following would //not// typecheck!

    {{{#!hs
    ins :: Eq () :- Eq ()
    }}}

    Because there is no `instance Eq () => Eq ()` anywhere (and thus no
 `instance Eq () :=> Eq ()`), only `instance Eq ()`. But the implication
 `Eq () => Eq ()` should obviously hold. Does that mean we should also
 generate an `instance Eq () :=> Eq ()` automatically? But what about `(Eq
 (), Ord ()) => Eq ()`? `(Eq (), Ord (), Show ()) => Eq ()`? There is an
 extremely high number of contexts in which `Eq ()` holds, and generating
 every possible one of them would result in a combinatorial explosion.

    While those classes are neat tricks that can get you some of the
 functionality of `QuantifiedConstraints`/`ImplicationConstraints`, they
 don't go all the way. I really feel that some compiler smarts would make
 these features manageable.

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


More information about the ghc-tickets mailing list