restrictions on Coercible

[Simon Peyton-Jones]

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