module A (List, ints) wheredata List a = Nil | Cons a (List a)infixr 4 `Cons`ints :: List Intints = 1 `Cons` 2 `Cons` 3 `Cons` Nil
{-# LANGUAGE GeneralizedNewtypeDeriving #-}module B whereimport Anewtype Age = MkAge Int deriving Cclass C a where cList :: List ainstance C Int where cList = ints
{-# LANGUAGE Safe #-}module C (ages) whereimport Aimport Bages :: List Ageages = cList
Module C compiles without a hiccup. But, it shouldn't: the coercion between ages and ints (performed by !GeneralizedNewtypeDeriving in module B) isn't Safe, as it breaks through List's abstraction. (Note that the constructors of List are not exported from module A!)
If module B includes {-# LANGUAGE Safe #-}, it duly doesn't compile, because of the stringent "constructors-must-be-in-scope" check done by the Coercible mechanism. The problem is that safety can be inferred without this check taking place.
You may also want to read the commentary on #8745 (closed) for related discussion.
Edited
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Child items
0
Show closed items
No child items are currently assigned. Use child items to break down this issue into smaller parts.
From the manual, describing the guarantees of Safe Haskell:
Module boundary control — Haskell code compiled using the safe language is guaranteed to only access symbols that are publicly available to it through other modules export lists. An important part of this is that safe compiled code is not able to examine or create data values using data constructors that it cannot import. If a module M establishes some invariants through careful use of its export list then code compiled using the safe language that imports M is guaranteed to respect those invariants. Because of this, Template Haskell and !GeneralizedNewtypeDeriving are disabled in the safe language as they can be used to violate this property.
Without the check to make sure that all relevant constructors are in scope, the above property would be false.
OK, but what does "access the symbols" mean, exactly? The kind of a type constructor may change if you change its implementation; and similarly its roles. I think it should be fine to coerce T Age to T Int, even if T's constructors are not visible, unless T's author declares T's role to be nominal.
In comment 3 I argue that it's right to infer Safe for B, and hence that B should compile fine with {-# LANGUAGE Safe #-}. That would mean removing the recursive check (which I particularly dislike).
Reopening ticket for now. David Mazieres and I don't think that this is the right solution. It means that a developer now needs to understand beyond Haskell2010 and some subtle details just to get correctly working module export control.
Including email DM sent describing our position:
At any rate, David and I just discussed the new Coerce typeclass.Based on David's understanding of its behavior, it sounds prettydangerous for Safe Haskell. At a minimum, the programmer is going toneed to understand a lot more than Haskell 2010 to write secure code.Based on my possibly limited understanding of the newfeature--automatically generating instances of the Coerce type seemsvery un-Haskell-like. By analogy, we could automatically generateinstance of Read and Show (or add equivalent DebugRead/DebugShowclasses) wherever possible, but this would similarly break abstractionby providing effective access to non-exported constructors.I understand why there is a need for something better thanGeneralizedNewtypeDeriving. However, implementing Coerce as atypeclass has the very serious disadvantage that there is no Haskellmechanism for controlling instance exports. And if we are going toadd a new mechanism (roles) to control such exports, exporting aninstance that is never requested and that undermines modularity andabstraction is an unfortunate default.It may be too late for this, but a cleaner solution more in keepingwith other extensions would be to have a -XDeriveCoerce extension thatallows Coerce to be explicitly derived when safe. This could becombined with leaving the previous behavior ofGeneralizedNewtypeDeriving and just deprecating the language feature.Though controlling instance exports does not have a precedent, anotheroption might be to special-case the Coerce class and only exportinstances of Coerce when all constructors of a type are also exported.This would prevent anyone from using Coerce to do things they couldn'talready do manually.
Though controlling instance exports does not have a precedent, another
option might be to special-case the Coerce class and only export
instances of Coerce when all constructors of a type are also exported.
This would prevent anyone from using Coerce to do things they couldn't
already do manually.
This is what we had originally; the check was removed in 59722295/ghc. It wouldn’t be hard to re-introduce it; but it will mean that a lot of uses of coerce or GND in Safe Haskell will fail, including coerce :: Set Age -> Set Int.
Maybe requiring a deriving (Coercible), or -XDeriveCoerce, or a standalone deriving declaration to get the coerce-under-type constructor behaviour isn’t such a bad idea after all, even outside the context of Safe Haskell? It would turn the current blacklisting (“add role annotatoin if it is not safe”) into whitelisting (“tell us that Coercing is safe, and how”).
For additional convenience we could retain the previous behaviour of „instance available if all constructors are in scope“, so that the author of simple cases like [], Either, Maybe do not have to do something; only those who hide their constructors have to act to allow their users to coerce under their type constructor.
TL;DR: Coercing under a type constructor is allowed if (a) all involved constructors are in scope (“could write it by hand test”) or (b) someone who had access to the constructors (most likely the author) explicitly declared the instance, using some form of deriving. No special behaviour needed for Safe Haskell.
Coercible is not a regular type class, and its "instances" are not subject to the usual rules of "always-exported". So you can 100% ignore the rules for normal instances.
The question is "under what circumstances are the instances of Coercible visible?". Or, to make it sound less type-class-ish, you could ask "what rules are used to solve Coercible constraints?".
Section 3 of the paper discusses this in some detail -- I hope everyone in this conversation has read it carefully. Specifically:
The "newtype-unwrapping" instance is available only if the newtype data constructor is visible. This is uncontroversial, just what Safe Haskell wants, and is clearly not what a "normal instance" is like.
The "lifting" instances are controlled by roles. And here there is room for debate about the proper defaults for those roles. For example, we could say that with Safe Haskell the default roles (ie if you don't give an explicit signature) of any data type declared in that module are nominal rather than representational.
For example, we could say that with Safe Haskell the default roles (ie if you don't give an explicit signature) of any data type declared in that module are nominal rather than representational.
What would that mean for inferring a module as Safe? Is A in the example Safe or nor? Would a module only be safe if it annotates everything as “nominal”?
It seems to me that any special handling of Safe Haskell module is doomed to fail, because we want to be able to infer modules as Safe, i.e. we’ll have code where we do not know whether they are intended to be used as Safe modules or not.
I think it would be helpful first for David & David to say exactly what they don't like about this:
{-# LANGUAGE Safe #-}module Lib( T, ... ) where data T a = Leaf a | Node (Tree a) (Tree a){-# LANGUAGE Safe #-}module Client( main ) import Lib newtype Age = MkAge Int foo :: T Age foo = .... bar :: T Int bar = coerce foo
To me this seems fine. If (inside Lib) the functions over T make use of type-class constraints over T's parameter, then we can declare a nominal role:
{-# LANGUAGE Safe #-}module Lib( T, ... ) where data T a = Leaf a | Node (Tree a) (Tree a) -- Balanced, based on Ord a role T nominal
I can see the following possible choices:
(A) Status quo. Data types without role signatures get representational roles by default. The above is accepted as-is
(B) Data types without role signatures get representational roles by default, except with {-# LANGUAGE SAFE #-} which changes the default to nominal. So Lib will compile without complaint, but Client will fail. Presumably, Lib without a Safe pragma would be inferred as Unsafe, since T would have representational role.
(C) Data types without role signatures always get nominal roles by default. That would mean that many many data types in libraries would have to have a role signature added, if you want to lift coercions over them.
So I need to educate myself better still but based on my current understanding (from the wiki page on roles) and the example Simon, what David and I don't like about this is that you can no longer look at just an export list for your module to verify what a consumer of your module is capable of doing.
I.e., the Safe Haskell specific issue with GND that we cared about when we disabled GND was #5498 (closed). My understanding is that the new roles and coercion infrastructure that forms the base of 7.8's GND deals with all the type safety issues where you could easily segfault a program or inspect a bool as an int. However, by default it doesn't deal with the module boundary issue. In fact, it makes it worse as now phantom roles allow coercion between them.
For example, Ptr requires explicit use of roles to ensure safety. This isn't very satisfactory to DM and I. Now a developer needs to understand GHC specific Haskell and a some subtle details to correctly implement abstractions. We'd prefer if export lists were self-contained and authoritative, not export lists + roles.
Speaking just for myself, I think (C) would be ideal. It coincides most closely with my (and what I believe most programmers) intuitive expectations of data types and abstraction is and gives the strongest safety by default. (B) has the downside of making a lot of code by default not safe and we were very much hoping solving GND would expand the default world that is safe, not reduce it. (A) as explained above isn't great in our opinion.
P.S., I'm traveling right now so may be some delays in replying but I'll try to be prompt.
I don't have a strong opinion; (C) is fine with me if library authors are happy. Maybe they will be; after all, they didn't have lifted coercions before, and (by default) they still won't.
Note that (C) is not related to the visiblity or otherwise of a recursive set of data constructors; it's simply a question of what the default roles for an un-annotated data type are.
Does anyone else care?
It's a tremendous pity that all this is happening just as 7.8 is on the verge of release (indeed, I thought it had already happened). I am reluctant to delay it while we debate this issue further. (I am not optimistic about a rapid consensus.)
Both the (A) and (C) solutions have bad cases. It comes down to picking a poison.
In (C), picking nominal as the default role means the GeneralizedNewtypeDeriving basically goes away with GHC 7.8. You will be unable to use GND for anything unless every author above you in the chain puts role annotations in. Moreover, we'll be stuck writing them forever for every data type. It still closes the GND loopholes, but it does so by nuking the site from orbit.
For (A), picking representational as the default role means that authors have to deal with unexpected encapsulation leaks. This required a half dozen annotations over base, and a couple in containers, maybe a dozen in lens and affects a relative minority of modules.
Both scenarios are bad.
Argument in favor of (A) is that many authors have already refactored to write their instances this way over the course of the last 2 release candidates, because we've been hammering home that they'll have to deal with it and that in the long term it is less work for everyone going forward, but it does mean that the folks who do care about SafeHaskell need to be conscious of the new language feature.
I rather don't like the fact that (A) puts a new burden on people silently, but I really don't like that (C) requires literally everyone to annotate everything forever. We'd never stop paying that tax, and everyone who thought they were ready for 7.8 is back to the drawing board, and needs to start preparing for the release anew.
Turning this around to try to find something productive here, I have two thoughts:
) One option might be to add a warning to any data type that doesn't export its constructors that has representational role. That isn't perfect. Some folks expose constructors in other-modules that they don't leak to to the end user in exposed-modules, but it'd be a start and covers for example, the cases in containers.
) Is there actually a SafeHaskell problem here at all? coerce itself isn't currently exposed in a Safe module, so it can't be used for a SafeHaskell exploit directly without trust. I am currently unaware of any path by which we can abuse GND alone to obtain a coercion.
If (2) holds, then while it is annoying to library authors that there is a new avenue to deal with that can violate their encapsulation, it does come into user-land from the same GHC.Prim module that you get unsafeCoerce# from, which can do everything coerce can do.
One option here is to just retain the status quo that GeneralizedNewtypeDeriving isn't available in Safe Haskell.
Then you'd retain the invariant that GND absolutely can't be used to violate library invariants, and since coerce isn't available in Safe mode without explicit trust, the interaction of these two features goes away completely.
nominal by default when constructors aren't all exported
representational by default when all constructors are exported
I understand the concern with (C) and the burden, I'm just not sure how high it is with some heuristics applied as suggested above. I like this approach (although I may be missing some corner cases) as it matches what I feel is a good high level starting point that GND and surrounding infrastructure (coercion) shouldn't allow you to write code that you couldn't write by hand unless explicitly opted-in by the library author.
I tend to agree with Edward's comments above, except on one perhaps-critical point: since RC 2, there is now a new module Data.Coerce in base that does export coerce Safe-ly. So, Edward's point (2) is incorrect. See #8745 (closed).
Separately, there has been a fair amount of debate between choices (A) and (C). I have advocated for (A), based on decreasing the pain for library authors. Perhaps in a clean-slate implementation of a language with coerce, I would favor (C), but that is not the case we have in front of us. (Yes, under (C), we would require more annotations, but we already require a host of instance declarations for many types, and this would just be yet another thing that Haskellers would know to do.)
The recursive-constructor-check that is described in the beginning of this ticket has lost its luster for me. If Safe inference worked, it would solve most of the problems brought up with the interaction between Safe and coerce. But, it also makes the coerce feature / GND very bowdlerized under Safe Haskell, and many desired uses of GND would no longer be possible. And, it's ugly from a user standpoint, requiring lots of importing of names unmentioned in code.
I see a two feasible ways forward, given the lateness of hour:
Keep the status quo.
Remove GND and coerce from the Safe subset for 7.8. We could look into ways of bringing them into Safe Haskell for 7.10.
In particular, I don't think that Simon's option (C) is viable, unless we want a Release Candidate 3, which I don't. Separately from the choice between (1) and (2), I definitely favor issuing warnings around missing role annotations, but it's unclear to me where the warnings should go. Edward's idea for warning when abstractly exporting a type with representational roles and no role annotation is a good start, and is perhaps the answer.
David's suggestion above (controlling roles in export lists) seems to present strange action-at-a-distance, in that if I don't export constructors from their defining module, the behavior is different from when I don't export the constructors from a different module. I worry that, while perhaps catching common cases, it would be very unexpected behavior in the details.
Just as a note, I was talking with Edward about this for just a moment, and I'm inclined to agree with him and Richard that we should bar GND and Data.Coerce from -XSafe for 7.8 as this discussion goes on. It's a bit 11th hour, but the changes are easy and safe.
I think the least pain would be temporarily marking that module Unsafe, and reverting to the pre 7.8 rule of no GND under Safe and then all we'll have "done no harm" as all code that worked before will continue to work and no new security problems will have been introduced.
I'd also be okay with looking into the 'if you don't export all your constructors you get a nominal role' rule for 7.10, but I am somewhat leery of introducing it in 7.8 after folks have already braced for a rather different impact.
May I throw the suggestion in ticket:8827#comment:80661 again into the ring? Most data types are exported with their constructors, so we want their users to coerce and GND as they wish; with that suggestion, no additional annotations are needed, and coerce can be replaced by hand-written code.
Abstract type constructors would, under this proposal, not be coercible by default, but this can easily be enabled using deriving (even instance deriving anywhere where the corresponding manual code can be written).
This is a variant of David’s suggestion (controlling roles in export lists) in that we correlate coercibility with constructor scope, but does not have the awkwardness of making the defining module’s export list special. In fact, it would quite precisely follow the guidance of “coerce (and GND) work exactly when you could write manual code for it”.
So given the late hour, perhaps (sadly) as others have suggested, we keep the status quo for 7.8 and leave GND and Coercion unsafe. Be nicer if we could have solved for 7.8 but that's on me for not be reachable easily or following the mailing list.
Going forward, my suggestion or a similar proposal such as nomeata's in ticket:8827#comment:80725 sound the nicest to me. We could potentially argue for this with data as well by seeing how prevalent coercion and GND is on abstract types that don't have explicit roles.
If everyone can quickly reach consensus though on the above proposal then I'm very happy with that as well :)
I'll admit to liking the general flavor of ticket:8827#comment:80725, but the details elude me somewhat. What, precisely, would go after the word deriving? What's the interaction between derived instances and role annotations? Could a derived instance be more restrictive than the assigned roles? (It certainly couldn't be less restrictive!) How would a user specify that?
On a separate note, and with no intention to start a flame war, this process would have been easier if we had had a more accurate timeline on the 7.8 release. When some of this debate started in October, we debated under the "late hour" premise, as well. The RCs hadn't gone out, obviously, but any less-than-almost-fully-baked idea was discarded as "too much work too late". If we had known that we had a few months to work out a proposal and implement it, it's possible that we'd be in a better place today. Of course, schedules slip, but communicating a best guess (even as that guess changes) would have been helpful.
I'll admit to liking the general flavor of ticket:8827#comment:80725, but the details elude me somewhat. What, precisely, would go after the word deriving?
Well, either data MyList a = [a] deriving Coercible, which will give you the same instance as described in the paper, but independent of the scope of the constructor.
Or deriving instance Coercible a b => Coercible (Map k a) (Map k b), which allows you to control the coercing
This is even strictly more powerful that our current system: It would allow the author of Map to export the instance above, while still using coerce in his code (with constructors in scope and no abstraction to follow) to coerce the key, if he wishes to do so.
What's the interaction between derived instances and role annotations? Could a derived instance be more restrictive than the assigned roles? (It certainly couldn't be less restrictive!) How would a user specify that?
As you say: The derived instance have to adhere the roles, but may be more restrictive (if created using a standalone deriving instance). The non-standalone-deriving instance would be the one that we have currently.
OTOH, this gets hairy once we mix tycons with exported constructors and tycons without, but with exported Coercible instances, in a new data declaration and try to find out when we can coerce under that... and that issue is well handled by roles and role inference. *shrug*
deriving Coercible a b => Coercible (Map k a) (Map k b)
is somewhat in line with what I've been playing around with to try to work out how we can lift coercions over complex data types.
e.g.
class Representational (t :: k1 -> k2) where rep :: Coercion a b -> Coercion (t a) (t b) default rep :: Phantom t => Coercion a b -> Coercion (t a) (t b) rep _ = phantomclass Representational t => Phantom t where phantom :: Coercion (t a) (t b) default phantom :: Coercible (t a) (t b) => Coercion (t a) (t b) phantom = Coercion
Then easy cases we can already handle work:
instance Representational Proxyinstance Phantom Proxyinstance Representational Taggedinstance Phantom Taggedinstance Representational (Tagged a) where rep Coercion = Coercioninstance Representational Const where rep Coercion = Coercioninstance Representational (Const a)instance Phantom (Const a)instance Representational Coercion where rep = unsafeCoerceinstance Representational (Coercion a) where rep Coercion = Coercioninstance Representational (->) where rep Coercion = Coercioninstance Representational ((->) a) where rep Coercion = Coercion
But with a few helpers
coerce1 :: Coercible a b => Coercion a c -> Coercion b ccoerce1 = coercecoerce2 :: Coercible b c => Coercion a b -> Coercion a ccoerce2 = coerce-- from Control.Lens as a placeholdernew :: (Rewrapping s t, Coercible (Unwrapped s) s, Coercible (Unwrapped t) t) => Coercion (Unwrapped s) (Unwrapped t) -> Coercion s tnew = coerce1 . coerce2-- I don't see how to implement this one directlyeta :: forall (f :: x -> y) (g :: x -> y) (a :: x). Coercion f g -> Coercion (f a) (g a)eta = unsafeCoerce
we can write several hard cases that are currently beyond our reach:
instance (Representational f, Representational g) => Representational (Compose f g) where rep = new.rep.repinstance Representational m => Representational (StateT s m) where rep = new.rep.rep.eta.repinstance Representational m => Representational (ReaderT e m) where rep = new.rep.repinstance Representational m => Representational (WriterT w m) where rep = new.rep.eta.rep
Then instead of lifting Coercible a b into Coercible (f a) (f b) based on the role of f's next argument, it'd lift using the Representational instance.
I'd been mostly exploring this as a straw man, but if we're throwing 'big changes' into the discussion, I felt it worth mentioning as a direction.
Mind you the code I have above is implementable and implemented with the existing Coercible machinery.
It isn't perfect though, e.g. I don't know a better way to implement
instance Representational f => Representational (Compose f) where rep = unsafeCoerce
is somewhat in line with what I've been playing around with to try to work out how we can lift coercions over complex data types.
Edward, I'm not following all the details of your comment here (like where is Coercion defined?), but it smells to me that you are hitting the the main limitation of the system as-implemented, namely the inability to abstract over a type constructor with a representational argument. Eg
data T f a = MkT (f a)
Can I do Coercible (T f Int) (T f Age) (where Age is a newtype for Int)? Only if we are guaranteed that f will be instantiated with type constructor with representational roles.
So you want higher-order roles. We know how to do that, but rejected it as Too Complicated. We could revisit that I guess.
I may also be misunderstanding your problem. Perhaps it would help to exhibit the simplest case that doesn't work.
Keep the status quo (as presented in the paper) for 7.8
But GND and Data.Coerce are both out of bounds for Safe Haskell
That's ok with me. Subsequent to 7.8, the Davids (or other Safe Haskell folk) may want to propose a concrete plan for getting them back in. Or maybe it just doesn't matter because Safe Haskell clients don't care (enough) about GND or Coercible.
FWIW I am keen to avoid any solution based on direct user control of Coercible instances. We have roles (we need them regardless to guarantee type-soundness); what we want can be expressed through roles or role signatures; adding another mechanism of control that does almost the same thing should be avoided if at all possible.
Indeed, I don't think in terms of instance declarations for Coercible at all; instead it's just a matter of what rules are available for solving Coercible constraints. To take an analogy, implicit parameters are internally implemented as type-class constraints, with some special rules. They share some stuff in common with type class constraints, but are best thought of separately. Same with Coercible.
The GHC 7.6 user manual used to say: 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..
But that was removed in the 7.8 user manual, which seems to contradict the conclusion in ticket:8827#comment:80866. Would someone like to fix the manual to say what it should say, whatever that now is?
It seems to me that there have been several competing goals mentioned here. However, I do not think they are impossible to mostly satisfy simultaneously, except perhaps for simplicity of the design. (In particular, I think it requires reinstating the constructor check.)
Code that is not annotated with roles should still largely enjoy the same module encapsulation as in H2010, so that module writers do not need to consider the implications of coerce or GND if they are not actually using them. With Safe Haskell, coerce and GND should not be able to create code based on such a module that couldn't be written "by hand".
Even without role annotations, coerce and GND should still be possible to use in Safe Haskell for most code that can be written by hand. (Preferrably as much as today without Safe Haskell enabled).
Safe Haskell should be inferrable without changing the semantics of a module.
Exporting all the constructors of a type from an Unsafe "Internal" module should not prevent data encapsulation by not reexporting them from a Trustworthy one.
Explicit role annotations, when used, should overrule all automatic restrictions on Safe mode, since that means the author has explicitly stated their intent.
Point 1 means that it is not ideal to make roles default to representational with no further checks. Point 2 means, similarly, that it is not ideal to make nominal the default. Point 4 means that any constructor export check cannot just be done by looking at the module defining the type.
Given this, I hope the following is compatible with all the goals above:
Default inferred role remains representational.
Any use of coerce (including via GND) must respect roles etc. as currently without Safe Haskell.
If allowed in general, a "lifting" use of coerce is compatible with Safe if either:
* The type has an explicit role annotation, or
* All of the type's data constructors are in scope.
Given this, I hope the following is compatible with all the goals above:
Default inferred role remains representational.
Any use of coerce (including via GND) must respect roles etc. as currently without Safe Haskell.
If allowed in general, a "lifting" use of coerce is compatible with Safe if either:
The type has an explicit role annotation, or
All of the type's data constructors are in scope.
For this to work out, the last check above must be recursive, looking at all datatypes mentioned in those in-scope data constructors, out to the leaves. Otherwise, a programmer could write a trivial wrapper around a type; all the data constructors would be in scope for the wrapper, and then the programmer could coerce away. It's the recursiveness of this check that's annoying.
Another (small) problem with this is that it means redundant role annotations are no longer a no-op. For example:
data Maybe1 a = Just1 a | Nothing1data Maybe2 a = Just2 a | Nothing2type role Maybe2 representational
Maybe1 and Maybe2 will have subtly different behavior with respect to Safe Haskell under this proposal. And just because the author of Maybe2 wanted to add some documentation about roles, much like most programmers add easy-to-infer type signatures.
I don't think the point I'm making should kill this proposal, but it is a downside.