GADT Type Inference with Higher-Kinded Types

Question

I've got some code that compiles:

{-# LANGUAGE ScopedTypeVariables, KindSignatures, GADTs, 
             FlexibleContexts #-}

module Foo where

data Foo :: (* -> *) where
  Foo :: c m zp' -> Foo (c m zp)

f :: forall c m zp d . Foo (c m zp) -> d
f y@(Foo (x :: c m a)) = g x y

g :: c m a -> Foo (c m b) -> d
g = error ""

The key thing I need in my real code is to convince GHC that if y has the type Foo (c m zp) and x has the type c' m' zp', then c' ~ c and m' ~ m. The above code achieves this because I am able to call g.

I want to change this code in two orthogonal ways, but I can't seem to figure out how to make GHC compile the code with either change.

First change: Add -XPolyKinds. GHC 7.8.3 complains:

Foo.hs:10:11:
    Could not deduce ((~) (k2 -> k3 -> *) c1 c)
    from the context ((~) * (c m zp) (c1 m1 zp1))
      bound by a pattern with constructor
                 Foo :: forall (k :: BOX)
                               (k :: BOX)
                               (c :: k -> k -> *)
                               (m :: k)
                               (zp' :: k)
                               (zp :: k).
                        c m zp' -> Foo (c m zp),
               in an equation for ‘f’
      at Foo.hs:10:6-21
      ‘c1’ is a rigid type variable bound by
           a pattern with constructor
             Foo :: forall (k :: BOX)
                           (k :: BOX)
                           (c :: k -> k -> *)
                           (m :: k)
                           (zp' :: k)
                           (zp :: k).
                    c m zp' -> Foo (c m zp),
           in an equation for ‘f’
           at Foo.hs:10:6
      ‘c’ is a rigid type variable bound by
          the type signature for f :: Foo (c m zp) -> d
          at Foo.hs:9:13
    Expected type: c1 m1 zp'
      Actual type: c m a
    Relevant bindings include
      y :: Foo (c m zp) (bound at Foo.hs:10:3)
      f :: Foo (c m zp) -> d (bound at Foo.hs:10:1)
    In the pattern: x :: c m a
    In the pattern: Foo (x :: c m a)
    In an equation for ‘f’: f y@(Foo (x :: c m a)) = g x y

Foo.hs:10:11:
    Could not deduce ((~) k2 m1 m)
    from the context ((~) * (c m zp) (c1 m1 zp1))
    ...

Second change: Forget about -XPolyKinds. Instead I want to use -XDataKinds to create a new kind and restrict the kind of m:

{-# LANGUAGE ScopedTypeVariables, KindSignatures, GADTs, 
             FlexibleContexts, DataKinds #-}

module Foo where

data Bar

data Foo :: (* -> *) where
  Foo :: c (m :: Bar) zp' -> Foo (c m zp)

f :: forall c m zp d . Foo (c m zp) -> d
f y@(Foo (x :: c m a)) = g x y

g :: c m a -> Foo (c m b) -> d
g = error ""

I get similar errors (can't deduce (c1 ~ c), can't deduce (m1 ~ m)). DataKinds seems to be relevant here: if I restrict m to have kind Constraint instead of kind Bar, the code compiles fine.

---

I've given two examples of how to break the original code, both of which use higher-kinded types. I've tried using case statements instead of pattern guards, I've tried giving a type to node instead of x, my usual tricks aren't working here.

I'm not picky about where the type for x ends up/what it looks like, I just need to be able to convince GHC that if y has the type Foo (c m zp), then x has the type c m zp' for some unrelated type zp'.

Answer 1

I greatly simplified the original question to the following, which compiles without {-# LANGUAGE PolyKinds #-} but fails to compile with PolyKinds.

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

data Pair1 :: (* -> *) where
  Pair1 :: Pair1 (c a, c b)

data D p a where
    D :: p (a, b) -> D p a -> D p b

f :: forall c z. D Pair1 (c z) -> D Pair1 (c z)
f y@(D Pair1 x) |
    (_ :: D Pair1 (c z)) <- y,
    (_ :: D Pair1 (c z')) <- x = y

With PolyKinds enabled the compiler error is

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

This error strongly suggests what I already suspected, that an answer depends on whether polykinded type application is injective. 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 -}

Polykinded type application is injective, but ghc doesn't know it. In order for ghc to deduce that the type application is injective, we need to provide kind signatures so that the compiler is aware the kinds are equivalent.

I haven't found sufficient kind annotations for your original, over-simplified version of the problem. When simplifying problems juggling types, reducing a type to essentially a Proxy is sometimes excessive, as it leaves fewer places to attach type signatures. You have found places to attach kind signatures to a more meaningful problem.

Answer 2

The problem can be resolved by adding kind signatures.

For example, when using -XPolyKinds, the following code compiles:

{-# LANGUAGE ScopedTypeVariables, KindSignatures, GADTs, 
             FlexibleContexts, PolyKinds #-}

module Foo where

data Foo :: (* -> *) where
  Foo :: (c :: k -> * -> *) m zp' -> Foo (c m zp)

f :: forall (c :: k -> * -> *) m zp d . Foo (c m zp) -> d
f y@(Foo x) = g x y

g :: c m a -> Foo (c m b) -> d
g = error ""

For the -XDataKinds version, I also need a kind signature on g:

{-# LANGUAGE ScopedTypeVariables, KindSignatures, GADTs, 
             FlexibleContexts, DataKinds #-}

module Foo where

data Bar

data Foo :: (* -> *) where
  Foo :: (c :: Bar -> * -> *) m zp' -> Foo (c m zp)

f :: forall (c :: Bar -> * -> *) m zp d . Foo (c m zp) -> d
f y@(Foo x) = g x y

g :: forall (c :: Bar -> * -> *) m a b d . c m a -> Foo (c m b) -> d
g = error ""

Not sure why I need more sigs for DataKinds, and it's a bit annoying to have to copy them everywhere, but it does get the job done.