Add (->) representation and the Invariant class to GHC.Generics

[nfrisby]

We currently disallow any use of the parameter in the domain of (->).

newtype F a = F ((a -> Int) -> Int) deriving Generic1

<interactive>:4:38:
    Can't make a derived instance of `Generic1 (F g)':
      Constructor `F' must use the last type parameter only as the last argument of a data type, newtype, or (->)
    In the data declaration for `F'

DeriveFunctor succeeds for this F.

I'd like to add this representation type to GHC.Generics and DeriveGeneric.

newtype (f :->: g) a = FArrow1 (f a -> g a)

We could then represent the first example above. We could also derive the more interesting Generic1 (F g).

newtype F g a = F (g a -> Int) deriving Generic1

type instance Rep1 (F g) = Rec1 g :->: Rec0 Int

instance Generic1 (F g) where
  to x = F $ unRec0 . unArrow1 x . Rec1
  from (F x) = FArrow1 $ Rec0 . x . unRec1

Admittedly, there's not many generic definitions impeded by not having (:->:). Contra- and in-variant types are uncommon.

I'm suggesting this feature without strong motivating examples because I think this would streamline the implementation of -XDeriveGenerics in some ways while also making it more general — assuming that we added the Invariant class to base or ghc-prim.

class Invariant t where
  invmap :: (a -> b) -> (b -> a) -> t a -> t b

invmap_covariant :: Functor t => (a -> b) -> (b -> a) -> t a -> t b
invmap_covariant f _ = fmap f

instance (Invariant f,Invariant g) => Invariant (FArrow f g) where
  invmap co contra (FArrow h) = FArrow $ invmap co contra . h . invmap contra co

(Of course, Invariant should be a super class of Functor. :/ )

Now we can handle quite involved examples:

newtype F g h a = F (g (h a)) deriving Generic1

instance Invariant g => Generic1 (F g h) where
  to x = invmap unRec1 Rec1 $ unComp1 x
  from (F x) = Comp1 $ invmap Rec1 unRec1

All of that said, I'm mostly opening this ticket so I can get feedback on difficulties I might not be anticipating and have a place to reference from the compiler source code comments.

[RyanGlScott]

I really like the idea of adding (:->:) to GHC.Generics. One of my biggest gripes with deriving Generic1 is that it doesn't work with many data types that have function arguments (e.g., Endo). I think adding (:->:) would allow GHC generics to at least be as expressive as DeriveFunctor/Foldable/Traversable.

I'm a bit hesitant about adding Invariant to base, however, primarily because I find it unlikely that it would ever be made a superclass of Functor, given the sheer amount of breakage that would cause. Moreover, I don't think we need Invariant to be able to derive Generic1 for data types with (:->:). I believe at most a generated Generic1 instance would need some Functor constraints, but that's no different than the current story.

(I haven't worked out the additional rules you'd need to add to the algorithms in Figures 1-4 of ​http://dreixel.net/research/pdf/gdmh.pdf, but the examples I've worked out by hand so far have only needed Functor constraints.)

[RyanGlScott]

Well, I had previously thought one could get away with not considering Invariant, but after thinking about it some more, having Invariant is crucial for this new feature to be compositional.

We'd add two new data types:

infixr 4 :->:, :->-:
newtype (f :->: r)  p = ContraArrow1 { unContraArrow1 :: f p -> r   }
newtype (f :->-: g) p = InvArrow1    { unInvArrow1    :: f p -> g p }

And, if we ​change Rec1 f to f :.: Par1, then we can also define the following for symmetry:

infixr 4 :>-:
type (r :>-: f) = ((->) r) :.: f

(I've adopted a pretty arbitrary naming scheme where hyphens (-) denote occurrences of the type parameter. Feel free to suggest other names.)

Then we can generate instances for data types no matter which side of an arrow a type parameter might occur. Here is an example:

newtype Endo a = Endo (a -> a) deriving Generic1

instance Invariant Endo where
  invmap f g (Endo x) = Endo (f . x . g)

==>

instance Generic1 Endo where
  type Rep1 Endo = D1 ... (C1 ... (S1 ... (Par1 :->-: Par1)))
  to1 (M1 (M1 (M1 c))) = Endo ((.) (invCompose unPar1 Par1) unInvArrow1 c)
  from1 (Endo c) = M1 (M1 (M1 ((.) InvArrow1 (invCompose Par1 unPar1) c)))

invCompose :: (c -> d) -> (a -> b) -> (b -> c) -> a -> d
invCompose = \f g h x -> f (h (g x))

So far, so good. But if we define something like this:

newtype Endo2 a = Endo2 (Endo a) deriving Generic1

Then things become awkward. GHC would attempt to generate an instance like this:

instance Generic1 Endo2 where
  type Rep1 Endo2 = D1 ... (C1 ... (S1 ... (Endo :.: Par1)))
  to1 (M1 (M1 (M1 c))) = Endo2 ((.) (fmap unPar1) unComp1 c)
  from1 (Endo2 c) = M1 (M1 (M1 ((.) Comp1 (fmap Par1) c)))

But this will never work, because it assumes Endo is a Functor instance, which can't happen. This is quite a problem: we can make one datatype a Generic1 instance, but we can't make a simple newtype wrapper around it a Generic1 instance!

However, if we changed the way GHC generated code for the :.: case to assume that the outermost datatype is an Invariant instance, not a Functor instance, then it would work:

instance Generic1 Endo where
  type Rep1 Endo = D1 ... (C1 ... (S1 ... (Par1 :->-: Par1)))
  to1 (M1 (M1 (M1 c))) = Endo ((.) (invCompose unPar1 Par1) unInvArrow1 c)
  from1 (Endo c) = M1 (M1 (M1 ((.) InvArrow1 (invCompose Par1 unPar1) c)))

Of course, this would mean bringing in Invariant to base, and it makes an assumption that most datatypes you'd find in the wild are Invariant instances already. As I mentioned above, trying to make Invariant a superclass of Functor is a hard sell.

Futhermore, I'm not sure if we'd really gain anything after all this breakage besides being able to derive Functor and Invariant instances generically. I'm not convinced the benefits outweigh the potential heartburn in this case.

[RyanGlScott]

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:

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:

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:

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

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 ​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.

[nfrisby]

Ryan, this looks very promising! I think this snippet presents the idea clearly, if I understand correctly. Please confirm.

-- | We suspect higher-order kinds (#9123) would supplant this typeclass.
class RoleIsRep f where
  mapCoerce :: Coercible a b => f a -> f b

data T f a = T (f [a])

instance RoleIsRep f => Generic1 (T f) where
  type Rep1 (T f) =
    D1 ('MetaData "T" "module" "package" 'True)
      (C1 ('MetaCons "T" 'PrefixI 'False)
        (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
          (f :.: Rec1 [])))
  from1 (T x) = M1 (M1 (M1 (Comp1 (mapCoerce x))))
  to1 (M1 (M1 (M1 x))) = T (mapCoerce (unComp1 x))

Note that this is a performance improvement in some cases to boot!

And your observation is that if we can define a lawful Functor f then we can define RoleRep f, right?

Can we anticipate a time where a user would want these three things simultaneously: 1) a lawful Functor f, 2) a nominal role for f's argument, and 3) an automatically derived Generic1 instance? That's the only case where this would be "worse" for the user, I think.

[RyanGlScott]

nfrisby, that sounds about right. What you call RoleIsRep is what Edward Kmett calls ​Representational, which has the definition:

class Representational f where
  rep :: Coercible a b => Coercion (f a) (f b)

goldfire raised the idea of making Representational a superclass of Functor ​here. Indeed, every Functor instance should also admit a Representational instance. I can't prove this directly, since you aren't allowed to implement Coercible instances directly, but you can at least write both halves of the isomorphism a Coercion induces:

functorRep1 :: (Coercible a b, Functor f) => f a -> f b
functorRep1 = fmap coerce

functorRep2 :: (Coercible a b, Functor f) => f b -> f a
functorRep2 = fmap coerce

And since the Functor laws dictate that fmap id = id, and coerce is morally the same thing as id, we can reason that fmap coerce = coerce for all law-abiding Functors.

With that above machinery, our new Generic1 instance looks like:

data T f a = T (f [a])

instance Representational f => Generic1 (T f) where
  type Rep1 (T f) =
    D1 ('MetaData "T" "module" "package" 'True)
      (C1 ('MetaCons "T" 'PrefixI 'False)
        (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
          (f :.: Rec1 [])))
  from1 (T x) = M1 (M1 (M1 (Comp1 (coerceWith rep x))))
  to1 (M1 (M1 (M1 x))) = T (coerceWith rep (unComp1 x))

Replying to nfrisby:

Can we anticipate a time where a user would want these three things simultaneously: 1) a lawful Functor f, 2) a nominal role for f's argument, and 3) an automatically derived Generic1 instance? That's the only case where this would be "worse" for the user, I think.

My hope is that (1) and (2) won't happen simultaneously, but now that I think about it more closely, there is a case where this does happen: type families. Consider this code:

type family Id a where
  Id a = a

newtype I a = I (Id a)

instance Functor I where
  fmap f (I a) = I (f a)

newtype T a = T (I [a]) deriving Generic1

However, if we switched over to Representational, this would no longer typecheck, since GHC always infers nominal roles for every argument of a type family. The fact that Id's argument is nominal is a bit annoying, since it feels like it should be representational, but at present we have no way of enforcing that.

[simonpj]

Crumbs... #9123 (about Representational) is a long thread! I'm totally not up to speed with all that.

However, part of the mix seems to be the feasibility (or otherwise) of allowing constraints like (forall a. Eq a => Eq [a] instance contexts; see #2893, #2456, and #5927, etc. For example:

instance (Binary a, forall b. Binary b => Binary (f b))
       => Binary (GRowe f a) where ...

I've always said "I don't know how to implement that", but this morning it feels different. Suppose that we only allowed those quantified constraints in the context of a top-level instance declaration.

• Solving "Wanted" constraints of this form is easy: it's just an implication constraint.
• Allowing them as "Given" constraints would be a little awkward, because it'd need a new field in the "inert set" of the constraint solver. But for instances it's all top-level-ish, so we could perhaps just extend the "local instance environment".

But even in the more general form it would be quite do-able I think. So, if allowing quantified constraints will help, perhaps it's time we bit that bullet.

Simon

Then it would only show up as a "Given" constraint when solving instance declarations, not in some arbitrary

[RyanGlScott]

Thanks, Simon! ImplicationConstraints/QuantifiedConstraints is something I've been wanting for a while, and it would definitely help me express more things in GHC generics than I've been wanting to express (see ​this comment in #5927 for more).

nfrisby, I thought of one more scenario in which conditions (1) and (2) could hold, but it's a bit of a silly one:

type role Wat nominal
newtype Wat a = Wat a deriving (Functor, Generic1)

A scheming user could use RoleAnnotations to explicitly mark a role as nominal that would otherwise be inferred as representational (or phantom). But this feels extremely silly to me, since having a Functor instance seems to defeat the whole point of having a nominal role, since you can just use fmap to change the internal representation yourself. Indeed, the only examples I can think of where users mark roles as nominal are:

1. Set (from the ​containers package)
2. HashSet (from the ​unordered-containers package)
3. Key (from the ​vault package)

And none of those can have Functor instances anyway. So I don't think this "counterexample" is much of a concern at all.

[RyanGlScott]

And as it turns out, goldfire has a separate ticket (#8177) for the proposed idea of being able to give explicit role signatures to type families, which might make the potential regression in ​this comment not an actual regression. See my comment ​here.

[goldfire]

Replying to simonpj:

But even in the more general form it would be quite do-able I think. So, if allowing quantified constraints will help, perhaps it's time we bit that bullet.

I think this is do-able. (I'm not currently volunteering to do it, though. Perhaps in the future, as doing this looks fun.) See our conversation starting at comment:14:ticket:2256.

[songzh]

Replying to nfrisby:

We currently disallow any use of the parameter in the domain of (->).

newtype F a = F ((a -> Int) -> Int) deriving Generic1

<interactive>:4:38:
    Can't make a derived instance of `Generic1 (F g)':
      Constructor `F' must use the last type parameter only as the last argument of a data type, newtype, or (->)
    In the data declaration for `F'

DeriveFunctor succeeds for this F.

I'd like to add this representation type to GHC.Generics and DeriveGeneric.

newtype (f :->: g) a = FArrow1 (f a -> g a)

We could then represent the first example above. We could also derive the more interesting Generic1 (F g).

newtype F g a = F (g a -> Int) deriving Generic1

type instance Rep1 (F g) = Rec1 g :->: Rec0 Int

instance Generic1 (F g) where
  to x = F $ unRec0 . unArrow1 x . Rec1
  from (F x) = FArrow1 $ Rec0 . x . unRec1

Admittedly, there's not many generic definitions impeded by not having (:->:). Contra- and in-variant types are uncommon.

I'm suggesting this feature without strong motivating examples because I think this would streamline the implementation of -XDeriveGenerics in some ways while also making it more general — assuming that we added the Invariant class to base or ghc-prim.

class Invariant t where
  invmap :: (a -> b) -> (b -> a) -> t a -> t b

invmap_covariant :: Functor t => (a -> b) -> (b -> a) -> t a -> t b
invmap_covariant f _ = fmap f

instance (Invariant f,Invariant g) => Invariant (FArrow f g) where
  invmap co contra (FArrow h) = FArrow $ invmap co contra . h . invmap contra co

(Of course, Invariant should be a super class of Functor. :/ )

Now we can handle quite involved examples:

newtype F g h a = F (g (h a)) deriving Generic1

instance Invariant g => Generic1 (F g h) where
  to x = invmap unRec1 Rec1 $ unComp1 x
  from (F x) = Comp1 $ invmap Rec1 unRec1

All of that said, I'm mostly opening this ticket so I can get feedback on difficulties I might not be anticipating and have a place to reference from the compiler source code comments.

[Ben Gamari <ben@…>]

In 7df5896/ghc:

Implement QuantifiedConstraints

We have wanted quantified constraints for ages and, as I hoped,
they proved remarkably simple to implement.   All the machinery was
already in place.

The main ticket is Trac #2893, but also relevant are
  #5927
  #8516
  #9123 (especially!  higher kinded roles)
  #14070
  #14317

The wiki page is
  https://ghc.haskell.org/trac/ghc/wiki/QuantifiedConstraints
which in turn contains a link to the GHC Proposal where the change
is specified.

Here is the relevant Note:

Note [Quantified constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The -XQuantifiedConstraints extension allows type-class contexts like
this:

  data Rose f x = Rose x (f (Rose f x))

  instance (Eq a, forall b. Eq b => Eq (f b))
        => Eq (Rose f a)  where
    (Rose x1 rs1) == (Rose x2 rs2) = x1==x2 && rs1 >= rs2

Note the (forall b. Eq b => Eq (f b)) in the instance contexts.
This quantified constraint is needed to solve the
 [W] (Eq (f (Rose f x)))
constraint which arises form the (==) definition.

Here are the moving parts
  * Language extension {-# LANGUAGE QuantifiedConstraints #-}
    and add it to ghc-boot-th:GHC.LanguageExtensions.Type.Extension

  * A new form of evidence, EvDFun, that is used to discharge
    such wanted constraints

  * checkValidType gets some changes to accept forall-constraints
    only in the right places.

  * Type.PredTree gets a new constructor ForAllPred, and
    and classifyPredType analyses a PredType to decompose
    the new forall-constraints

  * Define a type TcRnTypes.QCInst, which holds a given
    quantified constraint in the inert set

  * TcSMonad.InertCans gets an extra field, inert_insts :: [QCInst],
    which holds all the Given forall-constraints.  In effect,
    such Given constraints are like local instance decls.

  * When trying to solve a class constraint, via
    TcInteract.matchInstEnv, use the InstEnv from inert_insts
    so that we include the local Given forall-constraints
    in the lookup.  (See TcSMonad.getInstEnvs.)

  * topReactionsStage calls doTopReactOther for CIrredCan and
    CTyEqCan, so they can try to react with any given
    quantified constraints (TcInteract.matchLocalInst)

  * TcCanonical.canForAll deals with solving a
    forall-constraint.  See
       Note [Solving a Wanted forall-constraint]
       Note [Solving a Wanted forall-constraint]

  * We augment the kick-out code to kick out an inert
    forall constraint if it can be rewritten by a new
    type equality; see TcSMonad.kick_out_rewritable

Some other related refactoring
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

* Move SCC on evidence bindings to post-desugaring, which fixed
  #14735, and is generally nicer anyway because we can use
  existing CoreSyn free-var functions.  (Quantified constraints
  made the free-vars of an ev-term a bit more complicated.)

* In LookupInstResult, replace GenInst with OneInst and NotSure,
  using the latter for multiple matches and/or one or more
  unifiers