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'.

In the type signatures you give for x and y, zp and zp' are completely unrelated types. You have mentioned zp in the type signature of the function, but zp' is mentioned nowhere else. How can you expect the compiler to infer some relation between them? — user2407038
@user2407038 I don't. I just want the c and m to be the same. — crockeea
The stub for g doesn't work in f with the provided type. It does work in f with g :: ASTF dom (c m a) -> ASTF dom (c m b) -> ASTF dom (c m b). The type of g is suspiciously similar to the type of f; it doesn't convince me that there are any interesting functions that require this proof. — Cirdec
I've asked a (hopefully) related question about type equality implying kind equality. — Cirdec

Cirdec Cirdec · Accepted Answer · 2015-01-16T06:13:28

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.

GADT Type Inference with Higher-Kinded Types

2 Answers