The Current Coercible Rules are Dangerously Misleading

#24

@soundlogic2236 are you saying that

  1. There exist morally-coercible types that GHC can’t create automatic instances for
  2. Something stands in the way of users creating lawful instances of Coercible for these types on their own

You contrast this with Functor, where the user can define an instance manually (effectively saying, “trust me, compiler: you couldn’t do it, but I can”)

Furthermore, are you using the word “unsafe” to describe such manually-defined instances? In the sense that you have to do it by hand and may introduce bugs if done incorrectly.

1 Like
#25

So, the former is I think fine. Worst case I encode the collatz conjecture in some type level trickery and make a type which is coercible to void iff the collatz conjecture is false and coercible to unit iff the collatz conjecture is true. GHC is not obligated to solve open math problems just because I pose them to it. I might actually be able to do that even with the current coercible rules alone.

Now, it is impossible to create a Coercible instance which is annoying, but you can create Dict (Coercible A B) instances using unsafe code. It would also be nice to be able to actually make the compiler automatically find them, but that is an unrelated request.

My objection here is that there are Dict (Coercible A B) values that I think should exist and are actually unsound to have for very surprising reasons.

Specifically, Coercible A B not only is only created under a limited set of cases compared to where unsafeCoerce can be safely used, but implies something stronger in a surprising way. Also what exactly it implies is dependent on otherwise unexposed implementation details of the type.

Specifically the problem here is that sometimes GHC automatically enables function

extract :: Dict (Coercible (F a) (F b)) -> Dict (Coercible a b)
extract Dict = Dict

The exact rules for when it does this are dependent on implementation details of how the type F was originally declared, and it often will add this to types it is always sound to unsafeCoerce between, making exposing Dict (Coercible (F a) (F b) in any way, indirectly, through a function, etc unsound when it would otherwise be perfectly fine.

This can be gotten around with a hack. Rename your original declaration F with constructor MkF into Finner with constructor MkFinner. Create a new F as a newtype wrapper around Any. Use type role annotations to make the roles match. Use pattern synonyms that unsafely coerce between our F and a pattern match of Finner. Continue along with your day.

This will suppress extract from working. This is also a very hacky solution, and the fact that if you don’t do it you may accidentally expose something that is secretly unsafeCoerce is very surprising.

2 Likes
#26

As further evidence, I offer the following:

extract :: Coercion (Set a) (Set b) -> a :~: b
extract Coercion = Refl

Unless I made Set a newtype wrapper around something with representational role and set the nominal role only on the newtype wrapper. Once again showing how much better Coercible works around newtypes compared to data types. Even the role annotations work better!

It really seems like just about everyone intuitively expects Coercible to be, well, the safety condition for unsafeCoerce back and forth.

I believe this can be formalized and proven sound, and have written up part of such a thing. In the meantime however, at minimum I think Remove the Coercible decomposition rule by treeowl · Pull Request #276 · ghc-proposals/ghc-proposals · GitHub should be done (at least for the surface language) so people do not build code dependent on this dangerously intuitive behavior.

Further, I believe that as we move into dependent haskell, the way I’m trying to formalize coercible works even better, easily extending to things like value dependent coercions.

Oh, it also removes some eta expansions around type swizzling, which is just icing on the cake. And gives a more intuitive meaning to Coercible (f :: Type -> Type) (g :: Type -> Type). Really there are a lot of benefits.

But the first step is to plug the hole that blocks all these options from ever coming to fruition in any form, built in or library: Remove these extract functions from the stable surface language.