[GHC] #8516: Add (->) representation and the Invariant class to GHC.Generics

[GHC]

#8516: Add (->) representation and the Invariant class to GHC.Generics
-------------------------------------+-------------------------------------
        Reporter:  nfrisby           |                Owner:
            Type:  feature request   |               Status:  new
        Priority:  low               |            Milestone:
       Component:  Compiler (Type    |              Version:  7.7
  checker)                           |
      Resolution:                    |             Keywords:  Generics
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: goldfire (added)


Comment:

 I've been thinking about this recently, and I suspect there might be a way
 to accomplish this without needing anything like `Functor` or `Invariant`.

 The //only// reason we currently use `Functor` constraints in derived
 `Generic1` instances is to give us the ability to "tunnel into" data
 structures that are polymorphically recursive at least two levels deep
 (e.g., `newtype Compose f g a = Compose (f (g a))`). Consider a `Generic1`
 instance for `Foo`:

 {{{#!hs
 instance Functor f => Generic1 (Compose f g) where
   type Rep1 (Compose f g) =
     D1 ('MetaData "Compose" "Ghci3" "interactive" 'True)
       (C1 ('MetaCons "Compose" 'PrefixI 'False)
         (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness
 'DecidedLazy)
           (f :.: Rec1 g)))
   from1 (Compose x) = M1 (M1 (M1 (Comp1 (fmap Rec1 x))))
   to1 (M1 (M1 (M1 x))) = Compose (fmap unRec1 (unComp1 x))
 }}}

 This works, but requires that ugly `Functor` constraint. Is there an
 alternative? If we replace the `fmap` calls with holes:

 {{{#!hs
 instance Generic1 (Compose f g) where
   type Rep1 (Compose f g) =
     D1 ('MetaData "Compose" "Ghci3" "interactive" 'True)
       (C1 ('MetaCons "Compose" 'PrefixI 'False)
         (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness
 'DecidedLazy)
           (f :.: Rec1 g)))
   from1 (Compose x) = M1 (M1 (M1 (Comp1 (_1 x))))
   to1 (M1 (M1 (M1 x))) = Compose (_2 (unComp1 x))
 }}}

 Then it becomes clear what functions we need:

 {{{#!hs
 _1 :: f (g a) -> f (Rec1 g a)
 _2 :: f (Rec1 g a) -> f (g a)
 }}}

 All that `_1` and `_2` are doing is wrapping and unwrapping a `newtype`
 underneath an `f`! This would be a perfect job for `Data.Coerce.coerce`.
 If we could write something like this:

 {{{#!hs
 instance (Coercible (f (g a)) (f (Rec1 g a)), Coercible (f (Rec1 g a)) (f
 (g a))
     => Generic1 (Compose f g) where
   type Rep1 (Compose f g) =
     D1 ('MetaData "Compose" "Ghci3" "interactive" 'True)
       (C1 ('MetaCons "Compose" 'PrefixI 'False)
         (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness
 'DecidedLazy)
           (f :.: Rec1 g)))
   from1 (Compose x) = M1 (M1 (M1 (Comp1 (coerce x))))
   to1 (M1 (M1 (M1 x))) = Compose (coerce (unComp1 x))
 }}}

 It would work! But we can't write this since `a` isn't in scope in the
 instance's context. I can't even figure out how to hack it using something
 like [http://hackage.haskell.org/package/constraints-0.8/docs/Data-
 Constraint-Forall.html Data.Constraint.Forall] from the `constraints`
 library.

 Of course, there's the issue that we don't know //a priori// what role the
 type argument to `f` has, so there would still be some types for which
 this `Generic1` instance wouldn't typecheck. But I claim that any type for
 which `f` is forced to be nominal (i.e., for which you couldn't `coerce`
 underneath `f`) couldn't have a `Functor` instance anyway, so this
 approach should be no less expressive than the current one.

 goldfire, would #9123 (higher-kinded roles) give us the ability to express
 this? If so, I think we could sidestep the issue of including `Invariant`
 in `base` entirely, since it would become unnecessary.

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