Is polykinded type application injective?

Question

Is polykinded type application injective?

When we enable PolyKinds, do we know that f a ~ g b implies f ~ g and a ~ b?

Motivation

When trying to answer another question, I reduced the problem to the point that I received the following error only with PolyKinds enabled.

Could not deduce (c1 ~ c)
from the context ((a, c z) ~ (c1 a1, c1 b))

If polykinded type application were injective, we could deduce c1 ~ c as follows.

(a,   c z) ~ (c1 a1,   c1 b)
(a,) (c z) ~ (c1 a1,) (c1 b) {- switch to prefix notation -}
      c z  ~           c1 b  {- f a ~ g b implies a ~ b -}
      c    ~           c1    {- f a ~ g b implies f ~ g -}
      c1   ~           c     {- ~ is reflexive -}

Type application is injective

In Haskell, type application is injective. If f a ~ g b then f ~ g and a ~ b. We can prove this to ourselves by compiling the following

{-# LANGUAGE GADTs #-}

import Control.Applicative

second :: a -> a -> a
second _ = id

typeApplicationIsInjective :: (Applicative f, f a ~ g b) => f a -> g b -> f b
typeApplicationIsInjective fa gb = second <$> fa <*> gb

Kind of type application is not injective

The kind of a type application is not injective. If we consider the following, which has kind (* -> *) -> *.

newtype HoldingInt f = HoldingInt (f Int)

We can ask ghci what kind something of kind (* -> *) -> * has when applied to something of kind * -> *, which is *

> :k HoldingInt
HoldingInt :: (* -> *) -> *
> :k Maybe
Maybe :: * -> *
> :k HoldingInt Maybe
HoldingInt Maybe :: *

This is the same kind as something of kind * -> * applied to something of kind *

> :k Maybe
Maybe :: * -> *
> :k Int
Int :: *
> :k Maybe Int
Maybe Int :: *

Therefore, it is not true that, borrowing syntax from KindSignatures, the first set of kind signatures implies anything in the second.

f :: kf, g :: kg, a :: ka, b :: kb, f a :: k, g b :: k
g :: kf, f :: kg, b :: ka, a :: kb

Answer 1

Polykinded type application is injective from the outside, but certainly not injective from inside Haskell.

By "injective from the outside" I mean that whenever there is a Refl with type f a :~: g b, then it must be the case that f is equal to g and a is equal to b, and since we know that types of different kinds are never equal, the kinds must be also the same.

The issue is that GHC only has homogeneous type equality constraints, and doesn't have kind equality constraints at all. The machinery for encoding GADTs using coercions exists only on the type and promoted type level. That's why we can't express heterogeneous equality, and why we can't promote GADTs.

{-# LANGUAGE PolyKinds, GADTs, TypeOperators #-}

data HEq (a :: i) (b :: k) :: * where
  HRefl :: HEq a a
-- ERROR: Data constructor ‘HRefl’ cannot be GADT-like in its *kind* arguments 

Also, here's a simple example of GHC not inferring injectivity:

sym1 :: forall f g a b. f a :~: g b -> g b :~: f a
sym1 Refl = Refl
-- ERROR: could not deduce (g ~ f), could not deduce (b ~ a)

If we annotate a and b with the same kind, it checks out.

This paper talks about the above limitations and how they could be eliminated in GHC (they describe a system with unified kind/type coercions and heterogeneous equality constraints).