[Haskell-cafe] GHC.Generics: how to derive a Generic instance for an existential type?

[Andreas Abel]

Dear Pedro,

thanks for the answer and your pointers to the literature.  As usual, 
people want things to work *now*, and I am no exception. ;-)

It seems like generics are broken in ghc 7.6.3 which we support for 
Agda, so I have to give up on generics for next years (until we drop 
support for ghc < 7.8).

   https://code.google.com/p/agda/issues/detail?id=1558

Cheers,
Andreas

On 07.06.2015 09:34, José Pedro Magalhães wrote:
> Hi Andreas,
>
> No, GHC.Generics doesn't support existentials.
>
> If your existentials are used as arguments to constructors (like in the
> example you've provided), the only approach I'm aware of that might help
> you is this:
>
>     Alexey Rodriguez Yakushev and Johan Jeuring.
>     Enumerating Well-Typed Terms Generically.
>     <http://www.cs.uu.nl/research/techreps/UU-CS-2009-017.html>
>     In Proceedings workshop on Approaches and Applications of Inductive
>     Programming 2009.
>     (This reference seems to be missing its references. You could also
>     look at Chapter 5 of Alexey's thesis
>     <file:///C:/Users/Dreixel/Desktop/rodriguez.pdf>.)
>
>
> If your existentials are used only as indices, then you could look at this:
>
>     José Pedro Magalhães and Johan Jeuring.
>     Generic Programming for Indexed Datatypes.
>     <http://dreixel.net/research/pdf/gpid.pdf>
>     In Proceedings of the 7th ACM SIGPLAN Workshop on Generic
>     Programming (WGP'11), pp. 37–46, ACM, 2011.
>     (Chapter 10 of my thesis
>     <http://dreixel.net/index.php?content=thesis> has a more up-to-date
>     version.)
>
>
>
> Cheers,
> Pedro
>
> On Sat, Jun 6, 2015 at 2:41 PM, Andreas Abel <andreas.abel at ifi.lmu.de
> <mailto:andreas.abel at ifi.lmu.de>> wrote:
>
>     I wonder whether GHC.Generics supports existential types yet...
>
>     {-# LANGUAGE DeriveGeneric #-}
>     {-# LANGUAGE ExistentialQuantification #-}
>     {-# LANGUAGE StandaloneDeriving #-}
>
>     import GHC.Generics
>
>     data U = forall a. (Generic a) => U a
>        -- deriving (Generic)
>          -- Can't make a derived instance of ‘Generic U’:
>          --   Constructor ‘U’ has existentials or constraints in its type
>          --   Possible fix: use a standalone deriving declaration instead
>
>     -- deriving instance Generic U
>          -- Can't make a derived instance of ‘Generic U’:
>          --   U must be a vanilla data constructor
>          -- In the stand-alone deriving instance for ‘Generic U’
>
>     data D1Ser
>     data C1_0Ser
>
>     instance Generic U where
>        type Rep U = D D1Ser (C1 C1_0Ser (S1 NoSelector (Rep a)))
>          -- Not in scope: type variable ‘a’
>
>     -- How to bring the existential type `a' into scope?
>
>     --
>     Andreas Abel  <><      Du bist der geliebte Mensch.
>
>     Department of Computer Science and Engineering
>     Chalmers and Gothenburg University, Sweden
>
>     andreas.abel at gu.se <mailto:andreas.abel at gu.se>
>     http://www2.tcs.ifi.lmu.de/~abel/
>     _______________________________________________
>     Haskell-Cafe mailing list
>     Haskell-Cafe at haskell.org <mailto:Haskell-Cafe at haskell.org>
>     http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
>
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/