When they are unsafe, then no. #, I. # Unsafe?

Question

unsafeVacuous in Data.Void.Unsafe and .# and #. in Data.Profunctor.Unsafe both warn of the dangers of using these functions with functors / profilers that are GADT. 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 (fx) fmap f Q = P (f undefined) 

Here unsafeVacuous Q will create a Q constructor with a dummy type.

This example is not very worrying, because it does not even look remotely like a reasonable instance of Functor . Are there any examples? In particular, would it be possible to create useful ones that obey the laws of a functor / profuntor when manipulated only using their public API, but break terribly in the face of these unsafe functions?

Answer 1

I do not believe that there is a true functor where unsafeVacuous can cause a problem. But if you write a bad Functor , you can make your own unsafeCoerce , which means that it should be marked {-# LANGUAGE Unsafe #-} . The problem with this is in void .

Here unsafeCoerce I came up with

 {-# LANGUAGE GADTs #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} import Data.Void import Data.Void.Unsafe type family F ab where F a Void = a F ab = b data Foo ab where Foo :: F ab -> Foo ab instance Functor (Foo a) where fmap = undefined unsafeCoerce :: forall a b. (F ab ~ b) => a -> b unsafeCoerce a = (\(Foo b) -> b) $ (unsafeVacuous (Foo a :: Foo a Void) :: Foo ab) main :: IO () main = print $ (unsafeCoerce 'a' :: Int) 

which prints 97 .