It's possible with this: https://blog.jle.im/entry/verified-instances-in-haskell.html.

We need several extensions and the Singleton library.
And your functor become like this:

class Functor f where
    type Fmap a b (g :: a ~> b) (x :: f a) :: f b

    sFmap
        :: Sing (g            :: a ~> b)
        -> Sing (x            :: f a   )
        -> Sing (Fmap a b g x :: f b   )

    -- | fmap id x == x
    fmapId
        :: Sing (x :: f a)
        -> Fmap a a IdSym0 x :~: x

    -- | fmap f (fmap g x) = fmap (f . g) x
    fmapCompose
        :: Sing (g :: b ~> c)
        -> Sing (h :: a ~> b)
        -> Sing (x :: f a   )
        -> Fmap b c g (Fmap a b h x) :~: Fmap a c (((:.$) @@ g) @@ h) x

From: https://www.zhihu.com/question/65775009/answer/263094330

It's possible with this: https://blog.jle.im/entry/verified-instances-in-haskell.html.

We need several extensions and the Singleton library.
And your functor become like this:

{-# LANGUAGE MagicHash, RankNTypes, PolyKinds, GADTs, DataKinds,
         FlexibleContexts, FlexibleInstances,
         TypeFamilies, TypeOperators, TypeFamilyDependencies,
         UndecidableInstances, TypeInType, ConstraintKinds,
         ScopedTypeVariables, TypeApplications, AllowAmbiguousTypes,
         PatternSynonyms, ViewPatterns #-}
class Functor f where
    type Fmap a b (g :: a ~> b) (x :: f a) :: f b

    sFmap
        :: Sing (g            :: a ~> b)
        -> Sing (x            :: f a   )
        -> Sing (Fmap a b g x :: f b   )

    -- | fmap id x == x
    fmapId
        :: Sing (x :: f a)
        -> Fmap a a IdSym0 x :~: x

    -- | fmap f (fmap g x) = fmap (f . g) x
    fmapCompose
        :: Sing (g :: b ~> c)
        -> Sing (h :: a ~> b)
        -> Sing (x :: f a   )
        -> Fmap b c g (Fmap a b h x) :~: Fmap a c (((:.$) @@ g) @@ h) x

From: https://www.zhihu.com/question/65775009/answer/263094330