文件开头无用的种类相等错误

Question

我收到一个错误

app\Main.hs:1:1: error:
    Couldn't match kind `*' with `Constraint'
    When matching types
      b :: *
      (Set b, Set s) :: Constraint
  |
1 | {-# LANGUAGE TypeFamilies #-}
  | ^

不知道为什么b和约束(Set b, Set s)要匹配？我希望约束在存在上量化类型 b 但为什么它会匹配它们？

我相信在出现错误之前我所做的最后一件事是将 OpOutcome 添加到 class。

这是代码

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE UndecidableSuperClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE RankNTypes #-}


module Main where

import GHC.TypeLits (Symbol)
import GHC.Exts (Constraint)
import Data.Reflection (Reifies, reflect)
import Data.Proxy (Proxy(..))

main :: IO ()
main = print 5


class ((a,b)::Constraint) => HasCtxt a b
instance (a,b) => HasCtxt a b
class Determines a b | a -> b
instance Determines a b => Determines a b
type Set b = (b ~ b)

type OpLayout a = (forall s ctxt b. (OpCtxt a s b ~ ctxt, Determines a b, Determines a ctxt,Reifies s b) => ( HasCtxt ctxt (Reifies s b))) :: Constraint


data Stack a where
  Cons :: OpConstructor a -> Stack b -> Stack a
  Nil  :: Stack "NIL"


class  OpLayout a => OpCode (a::Symbol) where
  type OpCtxt a s b = (ctxt :: Constraint) |  ctxt -> s b
  type OpOutcome a :: *
  data OpConstructor a
  opValue :: Determines a s => Proxy s
  opValue = Proxy
  popOP :: OpCtxt a s b => Stack a -> (b :: *)
  evalOP :: OpConstructor a -> Stack x -> OpOutcome a

instance OpCode "load_val" where
  type OpCtxt "load_val" s b  = (Set s, Set b)
  type OpOutcome "load_val" = Stack "load_val"
  data OpConstructor "load_val" = forall b. LOAD_VAL b
  popOP stack = reflect opValue
  evalOP op stack = op `Cons` stack

编辑：较小的版本，感谢 Krzysztof Gogolewski

{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE PolyKinds #-}

module Err where

import GHC.Exts (Constraint)

class Determines b | -> b
class (forall (b :: *) (c :: Constraint). (Determines b, Determines c) => c) => OpCode
instance OpCode

Answer 1

这是一个小得多的文件，但基本上有相同的错误：

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE FlexibleContexts #-}

module Test where

import GHC.Exts (Constraint)

class Determines a b | a -> b

class  (forall ctxt. (Determines a a, Determines a (OpCtxt a)) => ctxt) => OpCode a where
    type OpCtxt a :: Constraint

instance OpCode ()

这给出：

test.hs:1:1: error:
    Couldn't match kind ‘Constraint’ with ‘*’
    When matching types
      OpCtxt () :: Constraint
      () :: *
  |
1 | {-# LANGUAGE TypeFamilies #-}
  | ^

（顺便说一句，以后你可能应该尝试自己做一些类似的最小化，然后再问这里。）

GHC 使用如此无用的位置信息报告错误肯定是一个错误。然而，现在问题潜伏的地方太少了，我们可以很好地了解发生了什么。这里的情况是我们要求

Determines a a
Determines a (OpCtxt a)

在范围内具有功能依赖性 a 应该足以计算出 Determines 的另一个参数。好吧，我们知道 a 有 *，因为我们正在写 instance OpCode () 和 () :: *；我们知道 OpCtxt a 有种类 Constraint，因为我们在 class 声明中这么说了。所以 GHC 在开始之前就放弃了统一 a 和 OpCtxt a 的尝试——它们的种类不同，所以不可能相等！

要了解为什么会收到确切的错误消息，您唯一需要的技巧就是在所有地方为 a 粘贴 ()（因为这是我们尝试编写的实例）。

翻译回您的设置：您要求

Determines a b
Determines a ctxt

我们知道 b :: * 因为它作为 Reifies :: k -> * -> Constraint 的第二个参数出现，我们知道 ctxt :: Constraint 因为我们在 OpCode class 宣言。所以函数依赖不可能正确解决。然后，通过将 OpCtxt "load_val" s b 替换为 ctxt，然后减少到 (Set s, Set b).

，您会得到您看到的错误

文件开头无用的种类相等错误

Unhelpful Kind equality error at the start of file

haskell

type-families

type-kinds

constraint-kinds

polykinds