Re: [GHC] #5927: A type-level "implies" constraint on Constraints

15 Aug 2016

      #5927: A type-level "implies" constraint on Constraints
-------------------------------------+-------------------------------------
        Reporter:  illissius         |                Owner:
            Type:  feature request   |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  7.4.1
  checker)                           |
      Resolution:                    |             Keywords:
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 RyanGlScott):

 * cc: RyanGlScott (added)

Comment:

 I //do// have a pratical use-case for this feature: I think it would help
 solve part of the story for being able to derive `Generic` instances for
 GADTs (see Trac issues #8560 and #10514). In particular, I think
 `ImplicationConstraints` would allow be to be polymorphic over any
 existentially quanitified constraint in a GADT. In particular, there are
 GADTs like this:

 {{{#!hs
 class GShow a where
   gshow :: a -> String

 data T a where
   MkT :: GShow a => a -> T a
 }}}

 GHC generics currently lacks a facility for expressing the existential
 `GShow` constraint. I think we could add something like this:

 {{{#!hs
 data EC c f a where
   MkEC :: c => f a -> EC c f a
 }}}

 Then we could derive a `Generic` instance for `T` like so:

 {{{#!hs
 instance Generic (T a) where
   type Rep (T a) =
     D1 ('MetaData "T" "Ghci2" "interactive" 'False)
       (C1 ('MetaCons "MkT" 'PrefixI 'False)
         (EC (GShow a)
           (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness
 'DecidedLazy)
             (Rec0 a))))
   from (MkT x) = M1 (M1 (MkEC (M1 (K1 x))))
   to (M1 (M1 (MkEC (M1 (K1 x))))) = MkT x
 }}}

 So far, so good. Now I want to be able to define a generic `GShow`
 instance for `T` (where `GShow` comes from the
 [http://hackage.haskell.org/package/generic-deriving-1.10.7/docs/Generics-
 Deriving-Show.html generic-deriving] library). We already have cases for
 all generic datatypes except `EC`. This is what I want to be able to
 write:

 {{{#!hs
 class GShow' f where
   gshow' :: f a -> String

 instance (c => GShow' f) => GShow' (EC c f) where
   gshow' (MkEC x) = gshow' x
 }}}

 But for that, I need `ImplicationConstraints`. If I want to generalize
 this to `Generic1` instances, I'd probably need `QuantifiedConstraints`
 too.

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/5927#comment:17
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler