The Current Coercible Rules are Dangerously Misleading

[rhendric]

@soundlogic2236

And in the case with the Functor you would have to write unsafe code yourself as well. instance Functor Foo would be unsafe code, which would be surprising, but if you didn’t write such things you would be safe.

There’ve been a lot of Foos thrown around, so I don’t know what point you’re making here. If you implement the instance with unsafe code, then you’ve written unsafe code. If you implement the instance with safe code, or ask GHC to derive it (and it doesn’t raise an error in the process of doing so), there are no issues that I’m aware of.

@soundlogic2236

sound as long as you don’t do certain things.

That’s not a very convincing standard for soundness. Everything is sound as long as you don’t do certain things.

@soundlogic2236

This is unsound. newtype Foo a = Dict (CoercibleB Void a) has a representational parameter.

No it doesn’t!

{-# LANGUAGE RoleAnnotations #-}

import Data.Coerce
import Data.Constraint
import Data.Void

type role Foo representational
newtype Foo a = MkFoo (Dict (Coercible Void a))

Main.hs:7:1: error: [GHC-29178]
    • Role mismatch on variable a:
        Annotation says representational but role nominal is required
    • while checking a role annotation for ‘Foo’
  |
7 | type role Foo representational
  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

But even so, let’s write something like it that does have a representational role and see whether there’s a problem:

type role Foo' representational
data Foo' a = Coercible Void a => MkFoo'

test :: Coercible a b => Foo' a -> Foo' b
test = coerce

GHC is happy with this. And why shouldn’t it be? It’s permitting you to coerce something that captures a coercion between Void and a into something that captures a coercion between Void and b if there is a coercion from a to b. The Coercible relation is transitive, so this is all right. Everything appears to be working as intended here. Where’s the unsoundness?