haskell - 类中的种类多态性

Question

我recently ran into a problem对 GADT 使用种类多态性。那里的答案是为我的数据类型提供“完整的用户指定类型”(CUSK)。我已阅读 relevant documentation ，但是当我尝试将其应用于类时，我仍然遇到基本相同的错误。

具体来说，一旦我给出了一个 CUSK，下面就会编译:

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

data Foo (x :: k) where
  C :: Foo x -> Foo '(x,x)

但是当我将该定义移动到一个类时:

{-# LANGUAGE DataKinds, PolyKinds #-}

class Foo (f :: k -> *) where
  foo :: (f :: k1 -> *) (x :: k1) -> (f :: (k1,k1) -> *) ('(x,x) :: (k1,k1))

我收到错误:

• Expected kind ‘(k1, k1) -> *’, but ‘f’ has kind ‘k -> *’
• In the type signature:
    foo :: (f :: k1 -> *) (x :: k1) -> (f :: (k1, k1) -> *) ('(x, x) :: (k1, k1))
  In the class declaration for ‘Foo’

我希望我需要做一些小事来说服 GHC f在第二个例子中是种类多态的。

Answer 1

这是 GHC 8 和 TypeInType 的工作，这允许更多有趣的依赖形式。以下对您的代码类型检查进行小幅编辑。

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

module KP where

import Data.Kind

class Foo (f :: forall k. k -> *) where
  foo :: (f :: k1 -> *) (x :: k1) -> (f :: (k1,k1) -> *) ('(x,x) :: (k1,k1))

至关重要的是，使用 forall 不再是语法错误。在类型类参数的(哈哈!)类型中。