Hi David,
Joachim, Simon, and I have been trying to figure out how roles and newtype
coercions fit in with Safe Haskell. (See, for example
http://www.haskell.org/pipermail/ghc-devs/2013-September/002526.html, which I
will try to summarize here.)
It all boils down to this: Does Safe Haskell strive to guarantee that a
datatype whose constructors are not visible is actually abstract?
With roles implemented, GeneralizedNewtypeDeriving (GND) and the newtype
coercions (implemented through a Coercible "class") are fully type-safe.
However, there are various ways of using these features to end-run abstraction.
I infer from #5498 that Safe Haskell *does* strive to maintain abstraction
barriers, and then we need to think hard about how to fit GND and Coercible
into Safe Haskell. Bug #5498 demonstrates how GND breaks abstraction (this
behavior is unchanged with roles), and here is an example of how Coercible can,
too:
> module A (Abstract) where
> data Abstract a = MkAbs a
>
> abstractInt :: Int -> Abstract Int
> abstractInt = MkAbs
>
------
> module B where
> import A
> import GHC.Prim -- or wherever Coercible lives
>
> newtype Age = MkAge Int
> notSoAbstract :: Abstract Age
> notSoAbstract = coerce (abstractInt 5)
Does this behavior eliminate the use of `coerce` within Safe Haskell? Does
#5498 eliminate GND from Safe Haskell? And, do the fixes proposed in the email
thread linked above fix these problems? To wit, under Safe Haskell, we propose
that coercions and GND work only when all constructors of the relevant datatype
(and, recursively, all constructors of datatypes mentioned in the top-level
datatype, going all the way down) are visible.
Thanks,
Richard
_______________________________________________
ghc-devs mailing list
ghc-devs@haskell.org
http://www.haskell.org/mailman/listinfo/ghc-devs
