[GHC] #8827: Inferring Safe mode with GeneralizedNewtypeDeriving is wrong

[GHC]

#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