Safe Haskell and abstraction

[Richard Eisenberg]

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20130917/af61338d/attachment.htm>