Unifying polykinded quantification variable with tuple kinded type

I have the following class representing categories where the object class is represented by a kind, and each hom class is represented by a type indexed by types of the aforementioned kind.

{-# LANGUAGE GADTs, DataKinds, KindSignatures, PolyKinds #-}

type Hom o = o -> o -> *

class GCategory (p :: Hom o)
  where
  gid :: p a a
  gcompose :: p b c -> p a b -> p a c

a simple example of an instance is:

instance GCategory (->)
  where
  gid = id
  gcompose = (.)

Now I want to model product categories. As a simple starting point, here's a type modeling the morphisms of a category corresponding to a product of -> with itself:

data Bifunction ab cd
  where
  Bifunction :: (a -> c) -> (b -> d) -> Bifunction '(a, b) '(c, d)

here's the corresponding operations:

bifunction_id :: Bifunction '(a, a') '(a, a')
bifunction_id = Bifunction id id

bifunction_compose :: Bifunction '(b, b') '(c, c') -> Bifunction '(a, a') '(b, b') -> Bifunction '(a, a') '(c, c')
bifunction_compose (Bifunction f1 g1) (Bifunction f2 g2) = Bifunction (f1 . f2) (g1 . g2)

but when I try to stick the operations into an instance of the class:

instance GCategory Bifunction
  where
  gid = bifunction_id
  gcompose = bifunction_compose

I run into the following issue:

• Couldn't match type ‘a’ with ‘'(a0, a'0)’
  ‘a’ is a rigid type variable bound by
    the type signature for:
      gid :: forall (a :: (*, *)). Bifunction a a
    at /tmp/ghc-mod29677/Bifunction29676-49.hs:28:3-5
  Expected type: Bifunction a a
    Actual type: Bifunction '(a0, a'0) '(a0, a'0)
• In the expression: bifunction_id
  In an equation for ‘gid’: gid = bifunction_id
  In the instance declaration for ‘GCategory Bifunction’
• Relevant bindings include
    gid :: Bifunction a a
      (bound at /tmp/ghc-mod29677/Bifunction29676-49.hs:28:3)

I believe the important part of the message is the following:

  Expected type: Bifunction a a
    Actual type: Bifunction '(a0, a'0) '(a0, a'0)

specifically that it can't unify the type forall x y. Bifunction '(x, y) '(x, y) with the type forall (a :: (*, *)). Bifunction a a.

Stripping away most of the domain specific stuff, we're left with the following minimal repro of the problem:

{-# LANGUAGE GADTs, DataKinds, KindSignatures, PolyKinds, RankNTypes #-}

module Repro where

data Bifunction ab cd
  where
  Bifunction :: (a -> c) -> (b -> d) -> Bifunction '(a, b) '(c, d)

bifunction_id :: Bifunction '(a, a') '(a, a')
bifunction_id = Bifunction id id

bifunction_id' :: Bifunction a a
bifunction_id' = bifunction_id

Is there a way I can unify bifunction_id with bifunction_id' above?

An alternative approach I've tried is to use type families, but that still doesn't completely solve the problem:

{-# LANGUAGE GADTs, DataKinds, KindSignatures, PolyKinds, RankNTypes, TypeFamilies #-}

module Repro where

type family Fst (ab :: (x, y)) :: x
  where
  Fst '(x, y) = x

type family Snd (ab :: (x, y)) :: y
  where
  Fst '(x, y) = y

data Bifunction ab cd = Bifunction (Fst ab -> Fst cd) (Snd cd -> Snd cd)

bifunction_id :: Bifunction '(a, a') '(a, a')
bifunction_id = Bifunction id id

-- This still doesn't work
-- bifunction_id' :: Bifunction a a
-- bifunction_id' = bifunction_id

-- But now I can do this successfully
bifunction_id' :: Bifunction a a
bifunction_id' = Bifunction id id

But I don't really understand why this identical expression works, and would rather not have to manage a somewhat non obvious distinction like this throughout the rest of the code.

Solution

forall (x :: k) (y :: l). p '(x, y) is less general than forall (a :: (k, l)). p a, mainly because there are things of kind (k, l) which are not pairs.

type family NotAPair :: () -> () -> () -> (k, l)

(Note that the type family has no parameters, it's not the same as NotAPair (u :: ()) (v :: ()) (w :: ()) :: ()). If NotAPair '() '() '() :: (k, l) were actually a pair '(,) x y, then we would have this nonsense: '(,) ~ NotAPair '(), x ~ '(), y ~ '().

See also Computing with impossible types https://gelisam.blogspot.com/2017/11/computing-with-impossible-types.html

And even if "all things of kind (k, l) are pairs", there are different ways to make that fact available in the language. If you make it implicit, so that you could for example implicitly convert a forall x y. p '(x, y) into a forall a. p a, you may (or may not) make typechecking undecidable. If you make it explicit, you will have to work to write that conversion (that's Coq for example).