Why isn't GeneralizedNewtypeDeriving a Safe Haskell?

Question

From GHC's manual, Section Safe Language:

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.

How can one break a module's invariants using GeneralizedNewtypeDeriving?

Barkeeper

Check out this ticket which links to elaborations. – Lancelle

Because it can be used to write unsafeCoerce. – Insolation

There's a safe, but much less powerful version than the one GHC has. – Unilateral

Or the paper about Safe Haskell, that's on the second and third page. research.microsoft.com/en-us/um/people/simonpj/papers/… – Inexecution

@Unilateral What are the limitations of the less powerful version? – Hargis

The less powerful version simply constructs the instance. You can imagine how this starts to break down when the type variable is used in a non-trivial way. Containers with a Functor instance work, but nothing more. Still, this is enough to derive all the regular type classes like Eq, Ord, Num, etc. – Unilateral

Answer 1

Luqui linked to my blog post on the subject. Basically, GeneralizedNewtypeDeriving as implemented in GHC assumes that a certain kind of isomorphism (namely the operationally irrelevant isomorphism implied by newtype) implies leibniz equality. This was true in Haskell 98 sort of--but is not at all true in Haskell plus extensions.

That is, a newtype provides a pair of functions

a -> b
b -> a

that don't do anything in the core, but it is not okay to conclude

forall f. f a -> f b

because f might be a type function or a GADT. This is the form of equality needed for GeneralizedNewtypeDeriving

Even in Haskell 98 it breaks module boundries. You can have things like

class FromIntMap a where
  fromIntMap :: Map Int b -> Map a b

instance FromIntMap Int where
  fromIntMap = id

newtype WrapInt = WrapInt Int deriving FromIntMap

instance Ord WrapInt where
  WrapInt a <= WrapInt b = b <= a

which will do bad things...

My blog post shows how to implement unsafeCoerce several ways using other extensions (all safe) and GeneralizedNewtypeDeriving. I have a better understanding of why this is now, and am much more confident that GeneralizedNewtypeDeriving is unable to produce unsafeCoerce without the "System FC" style extensions (type familes, GADTs). Sill, it is unsafe, and should be used with care if at all. My understanding is that Lennart Augustsson (user augustss) implemented it very differently in hbc, and this implementation was safe. A safe implementation would be more limited, and more complicated.

UPDATE: With new enough versions of GHC (all problems should be gone as of 7.8.1) GeneralizedNewtypeDeriving is safe because of the new roles system

Penultimate

Still not safe in GHC 7.8 or 7.10: mail.haskell.org/pipermail/haskell-cafe/2015-April/118970.html – Floats