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.