How would one create a proper polymorphic Functor instance failing on unsafeVacuous?

Question

When discussing Void on Haskell Libraries mailing list, there was this remark:

Back in the day it used to be implemented by an unsafeCoerce at the behest of Conor McBride who didn't want to pay for traversing the whole Functor and replacing its contents, when the types tell us that it shouldn't have any. This is correct if applied to a proper Functor, but subvertible in the presence of GADTs.

The documentation for unsafeVacuous also says:

If Void is uninhabited than any Functor that holds only values of the type Void is holding no values.

This is only safe for valid functors that do not perform GADT-like analysis on the argument.

How would such a mischievous GADT Functor instance look like? (Using only total functions of course, without undefined, error etc.)

Answer 1

It's certainly possible if you're willing to give a Functor instance that does not adhere to the functor laws (but is total):

{-# LANGUAGE GADTs, KindSignatures #-}

import Data.Void
import Data.Void.Unsafe

data F :: * -> * where
  C :: F Void
  D :: F a

instance Functor F where
  fmap f _ = D

wrong :: ()
wrong = case (unsafeVacuous C :: F Int) of D -> ()

Now evaluating wrong results in a run-time exception, even though the type-checker considers it total.

Edit

Because there's been so much discussion about the functoriality, let me add an informal argument why a GADT that actually performs analysis on its argument cannot be a functor. If we have

data F :: * -> * where
  C :: ... -> F Something
  ...

where Something is any type that isn't a plain variable, then we cannot give a valid Functor instance for F. The fmap function would have to map C to C in order to adhere to the identity law for functors. But we have to produce an F b, for unknown b. If Something is anything but a plain variable, that isn't possible.