Type roles and confusing behavior by `coerce`

I have a type Id a and I'm trying to prevent accidentally coercing, e.g., an Id Double to an Id Int.

If I understand type roles correctly, the following should not compile.

{-# LANGUAGE RoleAnnotations #-}
import Data.Coerce (coerce)

type role Id nominal
newtype Id a = Id String

badKey :: Id Int
badKey = coerce (Id "I point to a Double" :: Id Double)

Unfortunately, it does:

Prelude> :load Id.hs
[1 of 1] Compiling Main             ( Id.hs, interpreted )
Ok, one module loaded.
*Main> :type badKey
badKey :: Id Int

What am I missing about type roles?

Solution

Coercible has three possible "types" of instances (which are automagically generated by the compiler, not defined by the user). Only one of them is actually affected by roles.

Every type is coercible to itself.
You can coerce "under" a type constructor, provided the affected type variables are representational or phantom. For example, you can coerce a Map Char Int into a Map Char (Data.Monoid.Sum Int) because for Map we have type role Map nominal representational.
You can always coerce a newtype to the underlying type and vice versa, provided the newtype constructor is in scope. This ignores all roles! The rationale is that, given that the constructor is available, you could always wrap and unwrap manually, so the role doesn't give you any safety anyway.

In your example, the third rule applies. Had the newtype been defined in another module and the constructor not imported, the coercion would have failed (to make it work again, you would need to switch the role to phantom).

The somewhat surprising special behaviour for newtypes is explained in this GHC issue.