Skip to content

Inferring Safe mode with GeneralizedNewtypeDeriving is wrong

See a detailed write up here SafeHaskell,GNDandRoles

Consider the following modules:

module A (List, ints) where

data List a = Nil | Cons a (List a)
infixr 4 `Cons`

ints :: List Int
ints = 1 `Cons` 2 `Cons` 3 `Cons` Nil
{-# LANGUAGE GeneralizedNewtypeDeriving #-}

module B where

import A

newtype Age = MkAge Int
  deriving C

class C a where
  cList :: List a

instance C Int where
  cList = ints
{-# LANGUAGE Safe #-}

module C (ages) where

import A
import B

ages :: List Age
ages = cList

Module C compiles without a hiccup. But, it shouldn't: the coercion between ages and ints (performed by !GeneralizedNewtypeDeriving in module B) isn't Safe, as it breaks through List's abstraction. (Note that the constructors of List are not exported from module A!)

If module B includes {-# LANGUAGE Safe #-}, it duly doesn't compile, because of the stringent "constructors-must-be-in-scope" check done by the Coercible mechanism. The problem is that safety can be inferred without this check taking place.

You may also want to read the commentary on #8745 (closed) for related discussion.

Edited by dterei
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information