Бесполезная ошибка равенства рода в начале файла

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

редактирование: уменьшенная версия, спасибо Кшиштофу Гоголевскому

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

с функциональной зависимостью в области действия, которая говорит, что должно быть достаточно, чтобы обработать другой аргумент для Determines. Ну, мы знаем, *, потому что мы пишем instance OpCode ()а также () :: *; и мы знаем, имеет вид Constraint, потому что мы сказали это в объявлении класса. Поэтому GHC отказывается от попыток унифицировать и OpCtxt aеще до того, как это начнется - у них разные виды, поэтому они не могут быть равными!

Единственный трюк, который вам нужен, чтобы увидеть, почему вы получаете именно то сообщение об ошибке, которое вы делаете, это придерживаться ()за aвезде (потому что это экземпляр, который мы пытаемся написать).

Возвращаясь к вашей настройке: вы просите

      Determines a b
Determines a ctxt

откуда мы знаем b :: *потому что он появляется как второй аргумент Reifies :: k -> * -> Constraint, и мы знаем ctxt :: Constraintпотому что мы сказали так в OpCodeобъявление класса. Таким образом, функциональная зависимость не может работать правильно. Затем вы получите ошибку, которую видели, поставив OpCtxt "load_val" s bза ctxt, а затем сводится к (Set s, Set b).