Opened 3 years ago

Closed 3 years ago

#8826 closed feature request (fixed)

Allow more coercions in Safe Haskell

Reported by: goldfire Owned by:
Priority: normal Milestone: 7.8.1
Component: Compiler Version: 7.8.1-rc2
Keywords: Cc: mail@…
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:


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 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.

Change History (8)

comment:1 Changed 3 years ago 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)?


comment:2 Changed 3 years ago 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.

comment:3 Changed 3 years ago by nomeata

Cc: mail@… added

comment:4 Changed 3 years ago by Richard Eisenberg <eir@…>

In 59722295bb8da8f01d37356fbed6aef7321a8195/ghc:

Remove "Safe mode" check for Coercible instances

We assume that library authors supply correct role annotations
for their types, and therefore we do not need to check for
the availability of data constructors in Safe mode. See
discussion in #8725. This effectively fixes #8827 and #8826.

comment:5 Changed 3 years ago by goldfire

Resolution: fixed
Status: newclosed

Ticket #8827 is marked as "merge". I'm just closing this one.

comment:6 Changed 3 years ago by Joachim Breitner <mail@…>

In db4f5e5245d5b24a8f0a06a85ded89c6124fb4c7/ghc-prim:

Update Coercible docs due to Safe Haskell adjustment

This should go with [59722295bb8da8f01d37356fbed6aef7321a8195/ghc], see
bug #8826.

comment:7 Changed 3 years ago by goldfire

Milestone: 7.8.1
Status: closedmerge

Joachim's commit should get merged, as it goes with the fix to #8827.

comment:8 Changed 3 years ago by thoughtpolice

Status: mergeclosed

Merged in 7.8.

Note: See TracTickets for help on using tickets.