newtype coercion wrapping status

[Richard Eisenberg]

According to the original post and the comments on #5498 (http://ghc.haskell.org/trac/ghc/ticket/5498), breaking through abstraction is another reason for keeping GND outside of Safe Haskell. I'm worried that the same concern would affect newtype coercions given the current proposal.

Richard

On Sep 9, 2013, at 10:51 AM, Simon Peyton-Jones wrote:

> The reason it's not safe in Safe Haskell is precisely #1496, the newtpye deriving bug.  Now that's fixed, Safe Haskell can remove the safety check.  Probably.  
> 
> This is another question that could usefully be articulated on the design page, Joachim.
> 
> Simon
> 
> | -----Original Message-----
> | From: Richard Eisenberg [mailto:eir at cis.upenn.edu]
> | Sent: 07 September 2013 18:46
> | To: Simon Peyton-Jones
> | Cc: Joachim Breitner; ghc-devs at haskell.org
> | Subject: Re: newtype coercion wrapping status
> | 
> | OK -- thanks for clarifying. This all sits better with me.
> | 
> | But, I'm still a little concerned about the "Safe Haskell" implications.
> | My understanding is that allowing coercions when the constructor is not
> | exported will not be considered "Safe". Here's a way forward:
> | 
> | Currently: a type is considered abstract when its constructors are not
> | exported.
> | 
> | Future proposal: a type is considered abstract when its constructors are
> | not exported AND its type parameters are all at role Nominal.
> | 
> | Under this new definition of "abstract", a library writer that remembers
> | not to export a constructor but neglects to use a role annotation should
> | consider a type *not* to be abstract. Is this what we want?
> | 
> | Richard
> | 
> | On Sep 7, 2013, at 1:16 PM, Simon Peyton-Jones <simonpj at microsoft.com>
> | wrote:
> | 
> | >
> | > | In the current code, the
> | > |         instance Coercible a b => Coercible (T a) (T b)
> | > | is available for both data and newtypes, if T's type argument has
> | > | Representational role, but independent of any constructor presence.
> | See
> | > | the note at
> | > | https://github.com/nomeata/ghc/compare/ntclass-clean#L9R1902
> | > | for a concise and complete list of the conditions for a Coercible
> | > | instance.
> | >
> | > Right! I explained that badly the first time; thanks for clarifying
> | Joachim.
> | >
> | > So newtype and data behave alike, except that newtype has the
> | *additional* property that if its constructor is available you can coerce
> | to the representation type.
> | >
> | > | If I understood Simon's last suggestion correctly than exporting a
> | type
> | > | constructor with a non-Nominal role means "I am fine if you cast this
> | > | argument". If this is not desired (e.g. maybe Ptr a is an example
> | here),
> | > | then the library author has to annotate the type argument as Nominal.
> | >
> | > Yes, that's right.  In theory someone could want the coercible instance
> | *plus* the nominal role, or vice versa, but I think we can jump that
> | bridge if we come to it.
> | >
> | > Simon
> | >
> 
>