#8827: Inferring Safe mode with GeneralizedNewtypeDeriving is wrong -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: 7.12.1 Component: Compiler | Version: 7.9 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #8226, #8745 | Differential Revisions: -------------------------------------+------------------------------------- Comment (by oerjan): I think what was wrong with my first attempt was forgetting that ''role annotations'' also need the safety check. Also the safety of an explicit role annotation has two sides: * When ''using'' an explicit role annotation, the recursive check for that type is disabled at the use site. I.e. an explicit role annotation is to be interpreted as explicit permission to do the implied coercions `Safe`ly without further ado thereafter. * However, the annotation ''itself'' should not be `Safe` (nor the module containing it) unless the coercions implied by it can be written by hand using what's in scope in the module, plus `coerce` for other types with explicit annotations. This means a recursive check for all its non-`nominal` parameters. Putting this together, the recursive check, when it happens, should cut off whenever an explicit role annotation is reached. A role annotation for a type transfers coercion `Safe`ty responsibility from the module using the role to the module declaring it. So I'll modify point 5, and add a point 6 that became apparent: 5. Explicit role annotations, when used, transfer the responsibility for the `Safe`ty of `coerce`ing a type to the annotating module. 6. To avoid breaking code, none of the new restrictions will apply outside of `Safe` mode. ---- So, to sum up the modified design: * Default inferred role remains `representational`. * Explicit role annotations do indeed have subtly different semantics from implicitly inferred ones: they are considered stated author permission to `coerce` a type, even when not all constructors are in scope at the use site. * Declaring a role annotation, `coerce`ing types, or GND require checking the (non-`nominal`) parameter roles for `Safe`ty. Failure of the check means the module is not `Safe`, but has no other semantic effect. My non-expert attempt to define the recursive `Safe`ty check, probably similar to what GHC used to do: * A nominal role is always `Safe`. * The role of a parameter from an explicit role annotation is `Safe`. * The role of a parameter from a type's implicitly inferred role annotation is `Safe` if: * The type's data constructors are all in scope, and * the roles of all nested type parameters containing the given parameter on the right side of the datatype declaration are `Safe`. ---- A few more thoughts/options: * As I mentioned, there probably should be an extension to make implicitly inferred roles behave as explicit ones for types declared in a module. Maybe `RoleAnnotations` itself will do, or at least imply it. * Since this proposal makes implicit and explicit role annotations subtly different, someone might want to have a way to explicitly declare a role annotation that behaves like an inferred one. Maybe the `inferredRepresentational` idea from my previous message. * By point 6, module encapsulation can still be broken nilly-willy by non-`Safe` modules, even by accident. Perhaps this is a bad idea, and an explicit extension (`NoScopedRolesRestriction`?) should be required to disable the recursive check for non-`Safe` modules. However, this would break backwards compatibility, and probably need a deprecation period. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8827#comment:42 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler