Default method (/ type family) can't be given at a more specific kind

Motivation

Haskell is very stubborn about kinds :) if I have the following type class

{-# Language DataKinds      #-}
{-# Language KindSignatures #-}
{-# Language PolyKinds      #-}
{-# Language TypeFamilies   #-}

import Prelude hiding (Functor (..))
import qualified Prelude
import Data.Kind
import Data.Type.Equality

type Cat ob = (ob -> ob -> Type)

class Functor (f :: src -> tgt) where
 type Source f :: Cat src
 type Target f :: Cat tgt
 fmap :: Source f a a' -> Target f (f a) (f a')

I might want to do two things that GHC doesn't let me do, this issue is about the latter

• Default Source f and Target f to be (->)
• Default fmap = Prelude.fmap when f::Type->Type, Source f = Target f = (->).. and there is a Prelude.Functor f instance.

The first is quite easily remedied by defining Source f = Target f = (-->)

type          (-->)
type family   (-->)       :: Cat ob
type instance (-->) @Type = (->)

But the second one is more complicated.

Proposal

I think this should work:

 default fmap :: (Prelude.Functor f, Source f ~ (->), Target f ~ (->)) => Source f a a' -> Target f (f a) (f a')
 fmap = Prelude.fmap

If GHC detects that the class variable is used at a different kind then it should only instantiate the default definition at that kind. It's understandable that f::s->t can't be used as ::Type->Type but since it's for defaulting I think it's not problematic

 -- • Expected kind ‘* -> *’, but ‘f’ has kind ‘src -> tgt’
 -- • In the first argument of ‘Functor’, namely ‘f’
 --   In the type signature:
 --     fmap :: (Functor f, Source f ~ (->), Target f ~ (->)) =>
 --             Source f a a' -> Target f (f a) (f a')

We can even index default methods on their kind

Workaround

This is my workaround to package all the necessary facts to use Prelude.fmap as default

• Default fmap = Prelude.fmap when f::Type->Type, Source f = Target f = (->).. and there is a Prelude.Functor f instance.

type OldFunctor :: (src -> tgt) -> Type
data OldFunctor f where
 OldFunctor :: (Prelude.Functor f, Source f ~ (->), Target f ~ (->)) => OldFunctor @Type @Type f

type  OldFunctorC :: (src -> tgt) -> Constraint
class OldFunctorC (f :: src -> tgt) where
 oldfunctor :: OldFunctor @src @tgt f
instance (f ~~ f', Prelude.Functor f', src ~ Type, tgt ~ Type, Target f' ~ (->), Source f' ~ (->)) => OldFunctorC (f :: src -> tgt) where
 oldfunctor :: OldFunctor @Type @Type f
 oldfunctor = OldFunctor

class .. where
 fmap :: Source f a a' -> Target f (f a) (f a')
 default fmap :: OldFunctorC f => Source f a a' -> Target f (f a) (f a')
 fmap | OldFunctor <- oldfunctor @src @tgt @f = Prelude.fmap