restrictions on Coercible

[Richard Eisenberg]

I've moved this conversation to the comments on #8503, which is where I should have started it in the first place. Please see there for my response.

Richard

On Nov 13, 2013, at 6:27 PM, Simon Peyton-Jones <simonpj at microsoft.com> wrote:

> Ah, life is never as simple as you hope.
> 
> The whole treatment of recursive types is a bit flaky in GHC.  For newtypes here is the motivation
> 	newtype R = MkR R
> Now if we have an instance
> 	instance Coercible a R => Coercible a R
> we aren't going to make much progress.  Mutual recursion is similar.
> 
> This is very much a corner case.  I think that if the recursion is under a type constructor eg
> 	newtype R1 = MkR [R1]
> then we are fine.  But the current test is conservative.  I worry about
> 	newtype R2 a = MkR (F a)
> because perhaps
> 	type instance F Int = R2 Int
> and now R2 Int is just like R.  But GHC won't spot this today.
> 
> In any case, I suppose that, provided it was documented, GND could simply ignore the recursion problem, behave as advertised, and if that gives a loop it's the programmer's fault.
> 
> Things in hs-boot files are treated (again conservatively) as if they might be recursive.
> 
> A related thing is unpacking data types.  Consider
> 	data T = MkT {-# UNPACK #-} !S
> 	data S = MkS {-# UNPAXCK #-} !Int {-# UNPAXCK #-} !Int
> A S-value is represented as a pair of Int# values.  And similarly T.  But what about
> 	data S2 = MkS2 {-# UNPACK #-} !Int {-# UNPACK #-} !S2
> We don’t want to unpack infinitely.  Strictness analysis also risks infinitely unpacking a strict argument.
> 
> I think the rules for newtypes could be different (and perhaps more generous) than for data types.
> 
> Simon
> 
> 
> | -----Original Message-----
> | From: Richard Eisenberg [mailto:eir at cis.upenn.edu]
> | Sent: 13 November 2013 20:16
> | To: Simon Peyton-Jones; Joachim Breitner
> | Cc: ghc-devs at haskell.org Devs
> | Subject: restrictions on Coercible
> | 
> | Hi Simon, Joachim, and others,
> | 
> | I'm in the midst of reimplementing GeneralizedNewtypeDeriving in terms
> | of coerce. See #8503 for why I'm doing this. But, I've run up against a
> | limitation of Coercible I'd like to know more about. Currently, the
> | stage2 compiler fails to build because of the problem.
> | 
> | In Module.lhs, there is this line:
> | 
> | > newtype PackageId = PId FastString deriving( Eq, Typeable )
> | 
> | The deriving mechanism sensibly prefers to use the GND mechanism when
> | it can, and it can (seemingly) for Eq here. But, I get this error:
> | 
> | > compiler/basicTypes/Module.lhs:297:46:
> | >     No instance for (ghc-prim:GHC.Types.Coercible FastString
> | PackageId)
> | >       because ‛PackageId’ is a recursive type constuctor
> | 
> | This is curious, because PackageId is manifestly *not* recursive. A
> | little poking around tells me that any datatype mentioned in a .hs-boot
> | file is considered recursive. There is sense to this, but the error
> | message sure is confusing. In any case, this opens up a broader issue:
> | we want GND to work with recursive newtypes. For example:
> | 
> | > class C a where
> | >   meth :: a
> | >
> | > instance C (Either a String) where
> | >   meth = Right ""
> | >
> | > newtype RecNT = MkRecNT (Either RecNT String)
> | >   deriving C
> | 
> | The above code works just fine in 7.6.3. But, if Coercible isn't
> | allowed over recursive newtypes, then this wouldn't work if GND is
> | implemented in terms of coerce.
> | 
> | So, my question is: why have this restriction? And, if there is a good
> | reason for it, it should probably be documented somewhere. I couldn't
> | find mention of it in the user's guide or in the haddock docs. If we do
> | keep this restriction, what to do about GND? Seems like this may kill
> | the idea of implementing GND in terms of coerce, but that makes me sad.
> | 
> | Thanks,
> | Richard
>