[Haskell] problem building syb-generics

[Simon Peyton-Jones]

OK I think you are now falling across one of the compromises we made when adding impredictative polymorphism to GHC (described in the paper "Boxy types" on my home page). Put briefly, eta reduction can change the typing properties of a program.  Undesirable, but we could not see how to avoid it.

That means that you may need to eta-expand some definitions. So instead of
	dataCast _ = gcast1
try
	dataCast _ f = gcast1 f

(Or something like that... just add the missing arguments.)

I'm disconnected from the network at the moment, so I can't test this.

Simon

| -----Original Message-----
| From: Matthew Pocock [mailto:matthew.pocock at ncl.ac.uk]
| Sent: 11 July 2006 10:54
| To: Simon Peyton-Jones
| Cc: GHC users
| Subject: Re: [Haskell] problem building syb-generics
| 
| On Tuesday 04 July 2006 13:20, Simon Peyton-Jones wrote:
| 
| > Lexically-scoped type variables are undergoing a slight upheaval in GHC 6.6
| > that has not quite settled, and that is what you are running into.
| 
| Thanks for the help. After a lot of trial & error, and reading and stuff I've
| got past the problems introduced by lexicals. Now I'm hitting another
| problem. I think there's a missmatch between Maybe (c a) returned by
| dataCast1 and Maybe (c (t' a)) returned by gcast1. Is this dues to something
| stupid I have done, or bit-rot between the two libraries?
| 
| Thanks
| 
| Matthew
| 
| Data/Generics2/Instances.hs:290:17:
|     Couldn't match expected type `forall a1. (Data ctx a1) => c (t a1)'
|            against inferred type `c1 (t1 a1)'
|       Expected type: (forall a2. (Data ctx a2) => c (t a2))
|                      -> Maybe (c [a])
|       Inferred type: c1 (t1 a1) -> Maybe (c1 (t' a1))
|     In the expression: gcast1
|     In the definition of `dataCast1': dataCast1 _ = gcast1
| 
| The type of gcast is:
| Data.Typeable.  gcast1  :: (Typeable1 t, Typeable1 t') => c (t a) -> Maybe (c
| (t' a))
| 
| And the dataCast1 signature (in Data.Generics2.Basics) is:
| 
| class (Typeable a, Sat (ctx a)) => Data ctx a
|    where
|      -- | Mediate types and unary type constructors
|      dataCast1 :: Typeable1 t
|                => ctx ()
|                -> (forall a. Data ctx a => c (t a))
|                -> Maybe (c a)
|   ...
| 
| The implementation (in Data.Generics2.Instances) is:
| 
| instance (Sat (ctx [a]), Data ctx a) =>
|          Data ctx [a] where
|   dataCast1 _  = gcast1
|   ...