具有更高种类类型的 GADT 类型推断

我有一些可以编译的代码：

{-# 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 ""

我在实际代码中需要的关键是让 GHC 相信如果y有类型Foo (c m zp) and x有类型c' m' zp', then c' ~ c and m' ~ m。上面的代码实现了这一点，因为我可以调用g.

我想以两种正交的方式更改此代码，但我似乎无法弄清楚如何使 GHC 通过这两种更改来编译代码。

第一个更改：添加-XPolyKinds。 GHC 7.8.3 抱怨：

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

第二个变化：忘记-XPolyKinds。相反我想用-XDataKinds创造新的种类并限制新的种类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 ""

我遇到类似的错误（can't deduce (c1 ~ c), can't deduce (m1 ~ m)). DataKinds似乎与这里相关：如果我限制m有善良Constraint而不是善良Bar，代码编译良好。

我给出了两个如何破坏原始代码的示例，这两个示例都使用更高级的类型。我尝试过使用 case 语句而不是模式保护，我尝试过给出一种类型node代替x，我惯用的伎俩在这里不起作用。

我对类型不挑剔x最终结果/看起来是什么样子，我只需要能够说服 GHC 如果y有类型Foo (c m zp), then x有类型c m zp'对于一些不相关的类型zp'.

我将原来的问题大大简化为以下内容，无需编译{-# LANGUAGE PolyKinds #-}但无法编译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启用编译器错误是

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

这个错误强烈暗示了我已经怀疑的事情，答案取决于是否多类类型应用是单射的 https://stackoverflow.com/questions/27990891/does-type-equality-imply-kind-equality。如果多类类型应用是单射的，我们可以推断c1 ~ c如下。

(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 -}

多类类型应用是单射的 https://stackoverflow.com/a/27993048/414413，但 ghc 不知道。为了让 ghc 推断类型应用程序是单射的，我们需要提供种类签名，以便编译器知道这些种类是等效的。

对于您最初的、过于简化的问题版本，我还没有找到足够的注释。当简化处理类型的问题时，将类型简化为本质上的Proxy有时过多，因为它留下的附加类型签名的位置较少。你有找到了可以附加友好签名的地方 https://stackoverflow.com/a/27993521/414413到一个更有意义的问题。