On 10 April 2015 at 01:48, Simon Peyton Jones wrote:

| prefer, such as only exporting the Coerce instance if all the | constructors are exported, it seems that the ship sailed on these

Coercible is relatively recent; I don't think we should regard it as cast in stone.

But yes, the Coerbible instance of a newtype is only available when the data constructor for the newtype is lexically in scope.

Yes, so as you point out in the paper, this is done to preserve abstractions, but the same rule isn't applied to data types since some types like IORef don't even have constructors that can be in scope. Ideally I'd like to find a way forward that works for everyone and isn't just a Safe Haskell mode setting. I think the first question is, are there situations where you'd want to use `coerce` internally to a module but disallow it externally? The role mechanism is a little awkward as it doesn't allow this (although it does for newtype's). If yes, then I think we should start there. If it seems we don't need external vs internal control, then we could simply change the default to be that GHC sets referential type parameters to nominal and allows them to be weakened to referential through role annotations. We could use hackage to test how much breakage this would cause. The third option is something Safe Haskell specific, so probably applying the newtype constructor rule to data types.

Simon

| -----Original Message----- | From: davidterei@gmail.com [mailto:davidterei@gmail.com] On Behalf Of | David Terei | Sent: 10 April 2015 09:38 | To: Simon Peyton Jones | Cc: Omari Norman; haskell Cafe; ghc-devs@haskell.org | Subject: Re: Generalized Newtype Deriving not allowed in Safe Haskell | | I'll prepare a patch for the userguide soon. | | As for something better, yes I think we can and should. It's on my todo | list :) Basically, the new-GND design has all the mechanisms to be | safe, but sadly the defaults are rather worrying. Without explicit | annotations from the user, module abstractions are broken. This is why | we left GND out of Safe Haskell for the moment as it is a subtle and | easy mistake to make. | | If the module contained explicit role annotations then it could be | allowed. The discussion in | https://ghc.haskell.org/trac/ghc/ticket/8827 has other solutions that I | prefer, such as only exporting the Coerce instance if all the | constructors are exported, it seems that the ship sailed on these | bigger changes sadly. | | Cheers, | David | | On 9 April 2015 at 00:56, Simon Peyton Jones | wrote: | > There is a long discussion on | > https://ghc.haskell.org/trac/ghc/ticket/8827 | > about whether the new Coercible story makes GND ok for Safe Haskell. | > At a type-soundness level, definitely yes. But there are other | > less-clear-cut issues like “breaking abstractions” to consider. The | > decision on the ticket | > (comment:36) seems to be: GND stays out of Safe Haskell for now, but | > there is room for a better proposal. | > | > | > | > I don’t have an opinion myself. David Terei and David Mazieres are in | > the driving seat, but I’m sure they’ll be responsive to user input. | > | > | > | > However, I think the user manual may not have kept up with #8827. | The | > sentence “GeneralizedNewtypeDeriving — It can be used to violate | > constructor access control, by allowing untrusted code to manipulate | > protected data types in ways the data type author did not intend, | > breaking invariants they have established.” vanished from the 7.8 | > user manual (links below). Maybe it should be restored. | > | > | > | > Safe Haskell aficionados, would you like to offer a patch for the | manual? | > And maybe also a less drastic remedy than omitting GND altogether? | > | > | > | > Simon | > | > | > | > From: Omari Norman [mailto:omari@smileystation.com] | > Sent: 09 April 2015 02:44 | > To: haskell Cafe | > Subject: Generalized Newtype Deriving not allowed in Safe Haskell | > | > | > | > When compiling code with Generalized Newtype Deriving and the | > -fwarn-unsafe flag, I get | > | > | > | > -XGeneralizedNewtypeDeriving is not allowed in Safe Haskell | > | > | > | > This happens both in GHC 7.8 and GHC 7.10. | > | > | > | > I thought I remembered reading somewhere that GNTD is now part of the | > safe language? The GHC manual used to state that GNTD is not allowed | > in Safe | > Haskell: | > | > | > | > https://downloads.haskell.org/~ghc/7.6.3/docs/html/users_guide/safe- | ha | > skell.html#safe-language | > | > | > | > But this language on GNTD not being part of the safe language was | > removed in the 7.8 manual: | > | > | > | > https://downloads.haskell.org/~ghc/7.8.2/docs/html/users_guide/safe- | ha | > skell.html#safe-language | > | > | > | > The GHC release notes don't say anything about this one way or the | other. | > Thoughts? | > | > | > _______________________________________________ | > ghc-devs mailing list | > ghc-devs@haskell.org | > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs | > _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

On 12 April 2015 at 13:01, Richard Eisenberg wrote:

On Apr 12, 2015, at 9:51 AM, David Terei wrote:

...

Ideally I'd like to find a way forward that works for everyone and isn't just a Safe Haskell mode setting.

Agreed. I'm not convinced this can be done, but it's certainly worth trying.

...

I think the first question is, are there situations where you'd want to use `coerce` internally to a module but disallow it externally? The role mechanism is a little awkward as it doesn't allow this (although it does for newtype's). If yes, then I think we should start there.

Yes, the ability to use `coerce` within one module but not elsewhere would be nice. This can currently be simulated (without too much difficulty) with newtypes. A datatype D can have a more permissive role signature than an equivalent newtype N (where `newtype N = MkN D`). The package then exports N (without its constructor). This effectively allows local uses of `coerce`, even for datatypes. A more direct mechanism would be better, but I don't think we should bend over backwards for it.

...

If it seems we don't need external vs internal control, then we could simply change the default to be that GHC sets referential type parameters to nominal and allows them to be weakened to referential through role annotations. We could use hackage to test how much breakage this would cause.

I worry that the breakage would be significant. But, now that authors have had a chance to put in role annotations, maybe it wouldn't be so bad. The change to GHC to make this happen is trivial: just change default_role in TcTyDecls.initialRoleEnv1. I don't have the infrastructure around to make an all-of-Hackage test, but I'm happy to support someone else who does.

A way to temper this as discussed in the ticket is to have the default be determined by the export list. A data type with all it's constructors exported can default to representational roles when possible, while nominal roles would be the default when a subset of constructors are exported. This is more complex for users to understand, but does map to the semantics expected under Haskell2010. It may be best to drive this decision with data. Luckily we've also got infrastructure for testing against Hackage: http://hackage.haskell.org/package/hackager

Richard _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Good advice. I'll set that up soon. On 13 April 2015 at 00:10, Simon Peyton Jones wrote:

David

If you would like to lead a debate, and drive it to a conclusion, that would be most helpful.

Usually it's constructive to write a wiki page that sets out the design choices, with examples to illustrate their consequences, to set the terms of the debate. Otherwise you risk misunderstandings, with red herrings being discussed repeatedly.

Thanks

Simon

| -----Original Message----- | From: davidterei@gmail.com [mailto:davidterei@gmail.com] On Behalf Of | David Terei | Sent: 12 April 2015 09:52 | To: Simon Peyton Jones | Cc: Omari Norman; ghc-devs@haskell.org; haskell Cafe | Subject: Re: Generalized Newtype Deriving not allowed in Safe Haskell | | On 10 April 2015 at 01:48, Simon Peyton Jones | wrote: | > | prefer, such as only exporting the Coerce instance if all the | > | constructors are exported, it seems that the ship sailed on these | > | > Coercible is relatively recent; I don't think we should regard it as | cast in stone. | > | > But yes, the Coerbible instance of a newtype is only available when | the data constructor for the newtype is lexically in scope. | | Yes, so as you point out in the paper, this is done to preserve | abstractions, but the same rule isn't applied to data types since some | types like IORef don't even have constructors that can be in scope. | | Ideally I'd like to find a way forward that works for everyone and | isn't just a Safe Haskell mode setting. | | I think the first question is, are there situations where you'd want to | use `coerce` internally to a module but disallow it externally? The | role mechanism is a little awkward as it doesn't allow this (although | it does for newtype's). If yes, then I think we should start there. | | If it seems we don't need external vs internal control, then we could | simply change the default to be that GHC sets referential type | parameters to nominal and allows them to be weakened to referential | through role annotations. We could use hackage to test how much | breakage this would cause. | | The third option is something Safe Haskell specific, so probably | applying the newtype constructor rule to data types. | | > | > Simon | > | > | -----Original Message----- | > | From: davidterei@gmail.com [mailto:davidterei@gmail.com] On Behalf | > | Of David Terei | > | Sent: 10 April 2015 09:38 | > | To: Simon Peyton Jones | > | Cc: Omari Norman; haskell Cafe; ghc-devs@haskell.org | > | Subject: Re: Generalized Newtype Deriving not allowed in Safe | > | Haskell | > | | > | I'll prepare a patch for the userguide soon. | > | | > | As for something better, yes I think we can and should. It's on my | > | todo list :) Basically, the new-GND design has all the mechanisms | > | to be safe, but sadly the defaults are rather worrying. Without | > | explicit annotations from the user, module abstractions are | broken. | > | This is why we left GND out of Safe Haskell for the moment as it | is | > | a subtle and easy mistake to make. | > | | > | If the module contained explicit role annotations then it could be | > | allowed. The discussion in | > | https://ghc.haskell.org/trac/ghc/ticket/8827 has other solutions | > | that I prefer, such as only exporting the Coerce instance if all | > | the constructors are exported, it seems that the ship sailed on | > | these bigger changes sadly. | > | | > | Cheers, | > | David | > | | > | On 9 April 2015 at 00:56, Simon Peyton Jones | > | | > | wrote: | > | > There is a long discussion on | > | > https://ghc.haskell.org/trac/ghc/ticket/8827 | > | > about whether the new Coercible story makes GND ok for Safe | Haskell. | > | > At a type-soundness level, definitely yes. But there are other | > | > less-clear-cut issues like “breaking abstractions” to consider. | > | The > decision on the ticket > (comment:36) seems to be: GND | stays | > | out of Safe Haskell for now, but > there is room for a better | > | proposal. | > | > | > | > | > | > | > | > I don’t have an opinion myself. David Terei and David Mazieres | > | are in > the driving seat, but I’m sure they’ll be responsive to | user input. | > | > | > | > | > | > | > | > However, I think the user manual may not have kept up with | #8827. | > | The | > | > sentence “GeneralizedNewtypeDeriving — It can be used to violate | > | > constructor access control, by allowing untrusted code to | > | manipulate > protected data types in ways the data type author did | > | not intend, > breaking invariants they have established.” | vanished | > | from the 7.8 > user manual (links below). Maybe it should be | restored. | > | > | > | > | > | > | > | > Safe Haskell aficionados, would you like to offer a patch for | the | > | manual? | > | > And maybe also a less drastic remedy than omitting GND | altogether? | > | > | > | > | > | > | > | > Simon | > | > | > | > | > | > | > | > From: Omari Norman [mailto:omari@smileystation.com] > Sent: 09 | > | April 2015 02:44 > To: haskell Cafe > Subject: Generalized | Newtype | > | Deriving not allowed in Safe Haskell > > > > When compiling | code | > | with Generalized Newtype Deriving and the > -fwarn-unsafe flag, I | > | get > > > > -XGeneralizedNewtypeDeriving is not allowed in Safe | > | Haskell > > > > This happens both in GHC 7.8 and GHC 7.10. | > | > | > | > | > | > | > | > I thought I remembered reading somewhere that GNTD is now part | of | > | the > safe language? The GHC manual used to state that GNTD is | not | > | allowed > in Safe > Haskell: | > | > | > | > | > | > | > | > | > | | https://downloads.haskell.org/~ghc/7.6.3/docs/html/users_guide/safe- | > | ha | > | > skell.html#safe-language | > | > | > | > | > | > | > | > But this language on GNTD not being part of the safe language | was | > | > removed in the 7.8 manual: | > | > | > | > | > | > | > | > | > | | https://downloads.haskell.org/~ghc/7.8.2/docs/html/users_guide/safe- | > | ha | > | > skell.html#safe-language | > | > | > | > | > | > | > | > The GHC release notes don't say anything about this one way or | > | the other. | > | > Thoughts? | > | > | > | > | > | > _______________________________________________ | > | > ghc-devs mailing list | > | > ghc-devs@haskell.org | > | > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs | > | > | > _______________________________________________ | > ghc-devs mailing list | > ghc-devs@haskell.org | > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Here's an idea: For a module to be Safe, then for each exported datatype, one of the following must hold: 1) The datatype comes with a role annotation. 2) The module exports all of the datatype's constructors. 3) If the datatype is defined in a place other than the current module, the current module exports no fewer data constructors than are exported in the datatype's defining module. Why? 1) The role annotation, even if it has no effect, shows that the programmer has considered roles. Any mistake here is clearly the programmer's fault. 2) This datatype is clearly meant not to be abstract. `Coercible` then gives clients no more power than they already have. 3) This is subtler. It is a common idiom to export a datatype's constructors from a package-internal module, but then never to export the constructors beyond the package. If such a datatype has a role annotation (in its defining module, of course), then we're fine, even if it is exported abstractly later. However, suppose we are abstractly re-exporting a datatype that exports its constructors from its defining module. If there is no role annotation on the datatype, we're in trouble and should fail. BUT, if the datatype were exported abstractly in its defining module, then we don't need to fail on re-export, because nothing has changed. Actually, we could simplify the conditions. Change (2) to: 2') The module exports all of the datatype's visible constructors. I think explaining in terms of separate rules (2) and (3) is a little clearer, because the re-export case is slightly subtle, and this subtlety can be lost in (2'). This proposal would require tracking (in interface files, too) whether or not a datatype comes with a role annotation. This isn't hard, though. It might even help in pretty-printing. An alternative would be to have a way of setting roles differently on export than internally. I don't think this breaks the type system, but it's yet another thing to specify and support. And we'd have to consider the possibility that some module will import a datatype from multiple re-exporting modules, each with different ascribed role annotations. Is this an error? Does GHC take some sort of least upper bound? I prefer not to go here, but there's nothing terribly wrong with this approach. Richard On Apr 10, 2015, at 9:37 AM, David Terei wrote:

I'll prepare a patch for the userguide soon.

As for something better, yes I think we can and should. It's on my todo list :) Basically, the new-GND design has all the mechanisms to be safe, but sadly the defaults are rather worrying. Without explicit annotations from the user, module abstractions are broken. This is why we left GND out of Safe Haskell for the moment as it is a subtle and easy mistake to make.

If the module contained explicit role annotations then it could be allowed. The discussion in https://ghc.haskell.org/trac/ghc/ticket/8827 has other solutions that I prefer, such as only exporting the Coerce instance if all the constructors are exported, it seems that the ship sailed on these bigger changes sadly.

Cheers, David

On 9 April 2015 at 00:56, Simon Peyton Jones wrote:

...

There is a long discussion on https://ghc.haskell.org/trac/ghc/ticket/8827 about whether the new Coercible story makes GND ok for Safe Haskell. At a type-soundness level, definitely yes. But there are other less-clear-cut issues like “breaking abstractions” to consider. The decision on the ticket (comment:36) seems to be: GND stays out of Safe Haskell for now, but there is room for a better proposal.

I don’t have an opinion myself. David Terei and David Mazieres are in the driving seat, but I’m sure they’ll be responsive to user input.

However, I think the user manual may not have kept up with #8827. The sentence “GeneralizedNewtypeDeriving — It can be used to violate constructor access control, by allowing untrusted code to manipulate protected data types in ways the data type author did not intend, breaking invariants they have established.” vanished from the 7.8 user manual (links below). Maybe it should be restored.

Safe Haskell aficionados, would you like to offer a patch for the manual? And maybe also a less drastic remedy than omitting GND altogether?

Simon

From: Omari Norman [mailto:omari@smileystation.com] Sent: 09 April 2015 02:44 To: haskell Cafe Subject: Generalized Newtype Deriving not allowed in Safe Haskell

When compiling code with Generalized Newtype Deriving and the -fwarn-unsafe flag, I get

-XGeneralizedNewtypeDeriving is not allowed in Safe Haskell

This happens both in GHC 7.8 and GHC 7.10.

I thought I remembered reading somewhere that GNTD is now part of the safe language? The GHC manual used to state that GNTD is not allowed in Safe Haskell:

https://downloads.haskell.org/~ghc/7.6.3/docs/html/users_guide/safe-haskell....

But this language on GNTD not being part of the safe language was removed in the 7.8 manual:

https://downloads.haskell.org/~ghc/7.8.2/docs/html/users_guide/safe-haskell....

The GHC release notes don't say anything about this one way or the other. Thoughts?

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs