Claim about DefaultSignatures is wrong

[RyanGlScott]

Currently, the README claims that:

You might have noticed that (->), Compose, and CNat, all of which have Category instances, all have identitical instances of Functor and Contravariant. In fact, this will be true for any Category, which makes it a great opportunity to use the DefaultSignatures language extension:

class (Category (Cat j), Category (Cat k)) => Functor (f :: j -> k) where
  fmap :: Cat j a b -> Cat k (f a) (f b)

  default fmap :: (f ~ Cat j x, k ~ Type) => Cat j a b -> Cat j x a -> Cat j x b
 fmap = (.)

class (Category (Cat j), Category (Cat k)) => Contravariant (f :: j -> k) where
  contramap :: Cat j a b -> Cat k (f b) (f a)

  default contramap :: (f ~ Cat j, k ~ j -> Type) => Cat j a b -> Natural (->) (f b) (f a)
  contramap h = Natural (.h)

However this doesn't compile in ghc-8.0.2; while DefaultSignatures lets us specialize over other constraints, it doesn't (yet?) allow us to specialize kinds.

This claim about DefaultSignatures is incorrect, since the issue has nothing to do with DefaultSignatures. You can see this for yourself if you try to make the default implementation into a top-level function:

fmapDefault :: Functor (f :: j -> k)
            => (f ~ Cat j x, k ~ Type)
            => Cat j a b -> Cat j x a -> Cat j x b
fmapDefault = (.)

Compiling this with GHC 8.0.2 yields:

    • Expected kind ‘j -> k’, but ‘Cat j x’ has kind ‘j -> Type’
    • In the second argument of ‘~’, namely ‘Cat j x’
      In the type signature:
        fmapDefault :: Functor (f :: j -> k) =>
                       (f ~ Cat j x, k ~ Type) => Cat j a b -> Cat j x a -> Cat j x b

Why doesn't this work? It's helpful to read the discussion in Trac #13337. The gist of it is that because k ~ Type is a lifted type (i.e., it is not inhabited by ⊥), GHC is unable to check whether the proof of k ~ Type is valid before using it in that type signature. (We may get unlifted equalities with the introduction of Dependent Haskell.)

So DefaultSignatures isn't to blame here - rather, the limitations of the type system are.

[rampion]

Ah, ok that makes sense. Thank you! Any objection to replacing

However this doesn't compile in `ghc-8.0.2`; while `DefaultSignatures` lets us specialize
over other constraints, it doesn't (yet?) allow us to specialize kinds.

With

However this doesn't compile in `ghc-8.0.2` [due to limitations in the type
system](https://github.com/rampion/kinder-functor/issues/1), though this may work in ghc-8.2.

[RyanGlScott]

That sounds agreeable. But it's certainly not going to compile in 8.2, nor will it in any future release, as you'd need to use a completely different equality constraint from ~ to make it work (which hasn't been implemented yet).

[rampion]

Ah, I misread your ticket resolution then. I'll just go with "in a future version of GHC".