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 mailto:andreas.abel@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@gu.se mailto:andreas.abel@gu.se http://www2.tcs.ifi.lmu.de/~abel/ _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org mailto:Haskell-Cafe@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@gu.se http://www2.tcs.ifi.lmu.de/~abel/