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

bottom-type, functor, gadt, haskell

Solution

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.

Problem

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.)

Original source