[GHC] #8826: Allow more coercions in Safe Haskell

[GHC]

#8826: Allow more coercions in Safe Haskell
------------------------------------+-------------------------------------
       Reporter:  goldfire          |             Owner:
           Type:  feature request   |            Status:  new
       Priority:  normal            |         Milestone:
      Component:  Compiler          |           Version:  7.9
       Keywords:                    |  Operating System:  Unknown/Multiple
   Architecture:  Unknown/Multiple  |   Type of failure:  None/Unknown
     Difficulty:  Unknown           |         Test Case:
     Blocked By:                    |          Blocking:
Related Tickets:                    |
------------------------------------+-------------------------------------
 Suppose we have
 {{{
 newtype Age = MkAge Int
 }}}
 and we have `m :: Map String Int`. Is `coerce m :: Map String Age` allowed
 in Safe Haskell? Currently, no, because of the need to have `Map`'s
 constructor visible at the cite of the coercion. Why do we need this? In
 order to forestall any possible abstraction breaking. See
 [https://ghc.haskell.org/trac/ghc/ticket/8745#comment:3 this comment] for
 more information.

 But, it would seem that if the writer of `Map` supplies a role annotation,
 all should be forgiven. The author of the data structure is saying, with
 `type role Map nominal representational` that it is OK to coerce the
 second parameter. The annotation means that the author has considered
 roles and knows what the roles imply.

 So, I propose this: We allow coercions in Safe Haskell when the following
 algorithm permits it (and if the coercion is otherwise type-safe):
 Traverse down the tree of datatype definitions starting at the datatype to
 be coerced. At every datatype use, check if that datatype has a role
 annotation. If so, permit the coercion. Otherwise, require all
 constructors of the datatype to be in scope and recur on any datatypes
 mentioned in those constructors.

 Under that algorithm, we quickly discover that `Map` has a role annotation
 and permit (type-safe) coercions straightaway.

 This proposal is strictly a loosening of the current rules, and would
 allow strictly more programs to be accepted as Safe.

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