Allow more coercions in Safe Haskell
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.
Trac metadata
Trac field | Value |
---|---|
Version | 7.9 |
Type | FeatureRequest |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |