定义类型同义词 (GHC) 的类型同义词时出现奇怪错误

Question

背景

我在 Haskell (GHC) 中编写了以下代码：

{-# LANGUAGE 
  NoImplicitPrelude,
  TypeInType, PolyKinds, DataKinds,
  ScopedTypeVariables,
  TypeFamilies
#-}

import Data.Kind(Type)

data PolyType k (t :: k)

type Wrap (t :: k) = PolyType k t
type Unwrap pt = (GetType pt :: GetKind pt)

type family GetType (pt :: Type) :: k where
  GetType (PolyType k t) = t

type family GetKind (pt :: Type) :: Type where
  GetKind (PolyType k t) = k

这段代码的目的是让我可以将任意类型的类型包装成单一类型（即Type）的类型（即PolyType），然后稍后反转该过程（即解包） .

问题

我想为Unwrap 定义一个类型同义词，类似于以下内容：

type UnwrapSynonym pt = Unwrap pt

但是，上述定义会产生以下错误（GHC 8.4.3）：

* Invalid declaration for `UnwrapSynonym'; you must explicitly
  declare which variables are dependent on which others.
  Inferred variable kinds: pt :: *
* In the type synonym declaration for `UnwrapSynonym'

这个错误是什么意思？有没有办法绕过它来定义UnwrapSynonym？

我一直在做什么

到目前为止，我解决此问题的方法基本上是在我希望定义的任何高阶类型同义词中手动内联 Uwrap，但这感觉很恶心，我希望有更好的方法。

不幸的是，我对 GHC 的内部运作没有足够的经验，甚至无法确切地了解问题所在，更不用说弄清楚如何解决它了。

我相信我对我正在使用的扩展程序（例如TypeInType 和PolyKinds）的工作方式有相当的了解，但显然还不足以理解这个错误。此外，我还没有找到解决类似问题的资源。这部分是因为我不知道如何简洁地描述它，这也使得这个问题很难想出一个好的标题。

Answer 1

这个错误相当迟钝，但我认为它想说的是，GHC 已经注意到 UnwrapSynonym 的那种依赖，forall (pt :: Type) -> GetKind pt，它希望你显式地注释依赖：

type UnwrapSynonym pt = (Unwrap pt :: GetKind pt)

之所以要告诉它“哪些变量依赖于其他变量”是因为这个错误也可能出现在例如这种情况：

data Nat = Z | S Nat
data Fin :: Nat -> Type where
  FZ :: Fin (S n)
  FS :: Fin n -> Fin (S n)

type family ToNat (n :: Nat) (x :: Fin n) :: Nat where
  ToNat (S n) FZ = Z
  ToNat (S n) (FS x) = S (ToNat n x)

type ToNatAgain n x = ToNat n x -- similar error

ToNatAgain 应该有种类forall (n :: Nat) -> Fin n -> Nat，但是变量x 的类型取决于变量n 的类型。 GHC 想要明确注释，所以它告诉我告诉它哪些变量取决于哪些其他变量，它给了我它推断的类型来帮助做到这一点。

type ToNatAgain (n :: Nat) (x :: Fin n) = ToNat n x

在您的情况下，依赖关系在返回类型和参数类型之间。根本原因是相同的，但错误消息显然不是根据您的情况设计的，也不适合。您应该提交错误报告。

顺便说一句，您真的需要单独的Unwrap 和GetType 吗？为什么不让GetType 依赖？

type family GetType (pt :: Type) :: GetKind pt where
  GetType (PolyType k t) = t