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

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 添加到类中。

这是代码

{-# 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，因为我们在类声明中这么说了。所以 GHC 在开始之前就放弃了统一 a 和 OpCtxt a 的尝试——它们的种类不同，所以不可能相等!

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

翻译回您的设置:您要求

Determines a b
Determines a ctxt

我们知道 b::* 因为它作为 Reifies::k -> * -> Constraint 的第二个参数出现，我们知道 ctxt::Constraint 因为我们在 OpCode 类声明中这么说了。所以函数依赖不可能正确解决。然后，通过为 ctxt 放置 OpCtxt "load_val"s b，然后简化为 (Set s, Set b)，您会得到您看到的错误。