[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):

 Replying to [comment:40 goldfire]:
 > 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.

 Oops. What's worse, this interacts with role annotations:

 {{{
 module A (A) where

 -- inferred type role A representable
 data A a = A' a

 ...

 {-# LANGUAGE Safe #-}
 module B where

 import A

 type role B representative

 newtype B b = B (A b)
 }}}

 By my literal proposal above, module `B` has just managed to achieve such
 a wrapper, just with a role annotation and ''without'' `A'` in scope.
 Which means my point 5 is unsupportable as given, and the closest option I
 can think of requires tracking `Coercible` separately from roles - `B`
 here should have the role given, since that's the inferred one, but it
 should ''not'' therefore automatically be `Coercible` to `A`, except where
 `A'` is in scope.

 Or wait, hm. Perhaps a simpler option might be to distinguish
 `representable` from `inferredRepresentable` (better name hereby
 solicited), and have the rule that `inferredRepresentable` can be treated
 as `representable` only when all necessary constructors are in scope,
 recursively until you reach a non-`inferred` role. (Similarly for
 `phantom`, I guess.) That makes the role annotation for `B` wrong because
 `A`'s role is `inferredRepresentable`, and `A'` is not in scope.

 Also, there should then probably be a pragma to automatically remove the
 "inferred" when possible for types declared in a module.

 Warning: the above was written in a bit of a hurry.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/8827#comment:41>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler