Just when are unsafeVacuous, #., and .# unsafe?

Question

unsafeVacuous in Data.Void.Unsafe and .# and #. in Data.Profunctor.Unsafe both warn about the dangers of using those functions with functors/profunctors that are GADTs. Some dangerous examples are obvious:

data Foo a where
  P :: a -> Foo a
  Q :: Foo Void

instance Functor Foo where
  fmap f (P x) = P (f x)
  fmap f Q = P (f undefined)

Here, unsafeVacuous Q will produce a Q constructor with a bogus type.

This example isn't very troubling because it doesn't look even remotely like a sensible Functor instance. Are there examples that do? In particular, would it be possible to construct useful ones that obey the functor/profunctor laws when manipulated only using their public API, but break horribly in the face of these unsafe functions?

Answer 1

I don't believe there's any true functor where unsafeVacuous would cause a problem. But if you write a bad Functor you can make your own unsafeCoerce, which means it should to labeled with {-# LANGUAGE Unsafe #-}. There was an issue about it in void.

Here's an unsafeCoerce I came up with

{-# LANGUAGE GADTs               #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies        #-}
import Data.Void
import Data.Void.Unsafe

type family F a b where
  F a Void = a
  F a b    = b

data Foo a b where
  Foo :: F a b -> Foo a b

instance Functor (Foo a) where
  fmap = undefined

unsafeCoerce :: forall a b. (F a b ~ b) => a -> b
unsafeCoerce a = (\(Foo b) -> b) $ (unsafeVacuous (Foo a :: Foo a Void) :: Foo a b)

main :: IO ()
main = print $ (unsafeCoerce 'a' :: Int)

which prints 97.