# The Current Coercible Rules are Dangerously Misleading

**URL:** <https://discourse.haskell.org/t/the-current-coercible-rules-are-dangerously-misleading/10563>\
**Category:** Uncategorized\
**Created:** [October 19, 2024, 2:21am UTC](https://discourse.haskell.org/t/the-current-coercible-rules-are-dangerously-misleading/10563 "2024-10-19T02:21:20Z")\
**Posts on this page:** 1\
**Showing post:** 17

<div class="post-metadata">

**Author:** ![rhendric](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/rhendric/32/2689_2.png) [@rhendric](https://discourse.haskell.org/u/rhendric)\
**Post date:** [October 21, 2024, 3:21am UTC](https://discourse.haskell.org/t/the-current-coercible-rules-are-dangerously-misleading/10563/17 "2024-10-21T03:21:46Z")

</div>

> [@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 `Foo`s 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!

```hs
{-# LANGUAGE RoleAnnotations #-}

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

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

```

```haskell
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:

```hs
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?

---

_[View the full topic](https://discourse.haskell.org/t/the-current-coercible-rules-are-dangerously-misleading/10563)._