2

我收到一个错误

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
4

1 回答 1

7

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

{-# 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. 好吧，我们知道ahas *，因为我们正在编写instance OpCode ()and () :: *; 我们知道OpCtxt a有 kind Constraint，因为我们在类声明中这么说。所以 GHC 放弃了尝试统一a，OpCtxt a甚至在它开始之前 - 他们没有相同的种类，所以不能平等！

()要了解为什么会收到您所做的确切错误消息，您需要留下的唯一技巧是坚持a无处不在（因为这是我们正在尝试编写的实例）。

翻译回您的设置：您要求

Determines a b
Determines a ctxt

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

于 2022-01-26T03:08:58.303 回答