[GHC] #8826: Allow more coercions in Safe Haskell
#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
#8826: Allow more coercions in Safe Haskell -------------------------------------+------------------------------------ Reporter: goldfire | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.9 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by simonpj):
Why do we need this? In order to forestall any possible abstraction breaking.
I don't buy this. Why are inferred '''roles''' different from inferred '''kinds'''? What bad things would happen if we simply abandoned the restriction that the constructors of the type must be in scope to do allow coercion from `(T Int)` to `(T Age)`? Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8826#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8826: Allow more coercions in Safe Haskell -------------------------------------+------------------------------------ Reporter: goldfire | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.9 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by goldfire): 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. Truth be told, my proposal above also violates this property, but in a more principled way. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8826#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8826: Allow more coercions in Safe Haskell -------------------------------------+------------------------------------ Reporter: goldfire | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.9 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Changes (by nomeata): * cc: mail@… (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8826#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8826: Allow more coercions in Safe Haskell
-------------------------------------+------------------------------------
Reporter: goldfire | Owner:
Type: feature request | Status: new
Priority: normal | Milestone:
Component: Compiler | Version: 7.9
Resolution: | Keywords:
Operating System: Unknown/Multiple | Architecture: Unknown/Multiple
Type of failure: None/Unknown | Difficulty: Unknown
Test Case: | Blocked By:
Blocking: | Related Tickets:
-------------------------------------+------------------------------------
Comment (by Richard Eisenberg
#8826: Allow more coercions in Safe Haskell -------------------------------------+------------------------------------ Reporter: goldfire | Owner: Type: feature request | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 7.9 Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Changes (by goldfire): * status: new => closed * resolution: => fixed Comment: Ticket #8827 is marked as "merge". I'm just closing this one. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8826#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8826: Allow more coercions in Safe Haskell
-------------------------------------+------------------------------------
Reporter: goldfire | Owner:
Type: feature request | Status: closed
Priority: normal | Milestone:
Component: Compiler | Version: 7.9
Resolution: fixed | Keywords:
Operating System: Unknown/Multiple | Architecture: Unknown/Multiple
Type of failure: None/Unknown | Difficulty: Unknown
Test Case: | Blocked By:
Blocking: | Related Tickets:
-------------------------------------+------------------------------------
Comment (by Joachim Breitner
#8826: Allow more coercions in Safe Haskell -------------------------------------+------------------------------------ Reporter: goldfire | Owner: Type: feature request | Status: merge Priority: normal | Milestone: 7.8.1 Component: Compiler | Version: 7.8.1-rc2 Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Changes (by goldfire): * status: closed => merge * version: 7.9 => 7.8.1-rc2 * milestone: => 7.8.1 Comment: Joachim's commit should get merged, as it goes with the fix to #8827. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8826#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8826: Allow more coercions in Safe Haskell -------------------------------------+------------------------------------ Reporter: goldfire | Owner: Type: feature request | Status: closed Priority: normal | Milestone: 7.8.1 Component: Compiler | Version: 7.8.1-rc2 Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Changes (by thoughtpolice): * status: merge => closed Comment: Merged in 7.8. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8826#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC