檔案開頭無用的種類相等錯誤

我收到一個錯誤

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

uj5u.com熱心網友回復：

這是一個小得多的檔案，它具有基本相同的錯誤：

{-# 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

where we know b :: * because it appears as the second argument to Reifies :: k -> * -> Constraint, and we know ctxt :: Constraint because we said so in the OpCode class declaration. So the functional dependency can't possibly work out right. Then you get the error you saw by putting OpCtxt "load_val" s b for ctxt, and then reducing to (Set s, Set b).

標籤：

上一篇：Haskell函式的記憶

下一篇：如何在地板和天花板上使用sqrt？