Странная ошибка при определении синонима типа синонима типа (GHC) - PullRequest
Новая
       31

Странная ошибка при определении синонима типа синонима типа (GHC)

0 голосов
/ 22 сентября 2018

Справочная информация

Я написал следующий код на Haskell (GHC): 

{-# LANGUAGE 
  NoImplicitPrelude,
  TypeInType, PolyKinds, DataKinds,
  ScopedTypeVariables,
  TypeFamilies
#-}

import Data.Kind(Type)

data PolyType k (t :: k)

type Wrap (t :: k) = PolyType k t
type Unwrap pt = (GetType pt :: GetKind pt)

type family GetType (pt :: Type) :: k where
  GetType (PolyType k t) = t

type family GetKind (pt :: Type) :: Type where
  GetKind (PolyType k t) = k

Цель этого кода - позволить мне обернуть тип произвольного вида втип (а именно PolyType) одного вида (а именно Type), а затем позже обратный процесс (то есть распаковка).

Проблема

Я хотел бы определить синоним типадля Unwrap сродни следующему: 

type UnwrapSynonym pt = Unwrap pt

Однако приведенное выше определение приводит к следующей ошибке (GHC 8.4.3): 

* Invalid declaration for `UnwrapSynonym'; you must explicitly
  declare which variables are dependent on which others.
  Inferred variable kinds: pt :: *
* In the type synonym declaration for `UnwrapSynonym'

Что означает эта ошибка?Есть ли способ, которым я могу обойти это, чтобы определить UnwrapSynonym?

Что я делал

Мой подход к этой проблеме до сих пор состоит в том, чтобы по существу вручную включить Uwrap влюбые синонимы типа высшего порядка, которые я хотел бы определить, но это кажется странным, и я надеюсь, что есть лучший способ.

К сожалению, я недостаточно опытен во внутренней работе GHC, даже понимаю, в чем именно проблема, и гораздо меньше разбираюсь, как ее решить.

Полагаю, у меня есть приличное понимание того, как работают используемые мной расширения (например, TypeInType и PolyKinds), но, по-видимому, оно недостаточно глубокое, чтобы понять эту ошибку.Кроме того, мне не удалось найти ресурсы, которые решают аналогичную проблему.Отчасти это объясняется тем, что я не знаю, как кратко описать это, что также затруднило придумывание хорошего названия для этого вопроса.

1 Ответ

0 голосов
/ 22 сентября 2018

Ошибка довольно тупая, но я думаю, что она пытается сказать, что GHC заметил, что тип UnwrapSynonym зависит, forall (pt :: Type) -> GetKind pt, и хочет, чтобы вы явно аннотировали зависимость: 

type UnwrapSynonym pt = (Unwrap pt :: GetKind pt)

Причина, по которой он говорит «какие переменные зависят от других», заключается в том, что эта ошибка также может появляться, например, в такой ситуации: 

data Nat = Z | S Nat
data Fin :: Nat -> Type where
  FZ :: Fin (S n)
  FS :: Fin n -> Fin (S n)

type family ToNat (n :: Nat) (x :: Fin n) :: Nat where
  ToNat (S n) FZ = Z
  ToNat (S n) (FS x) = S (ToNat n x)

type ToNatAgain n x = ToNat n x -- similar error

ToNatAgain должно иметь вид forall (n :: Nat) -> Fin n -> Nat, но тип переменной x зависит от типа переменной n.GHC хочет, чтобы это явно аннотировалось, поэтому он сообщает мне, какие переменные зависят от каких других переменных, и дает мне то, что он выводит в качестве своего рода, чтобы помочь в этом. 

type ToNatAgain (n :: Nat) (x :: Fin n) = ToNat n x

В вашем случаезависимость находится между возвращаемым видом и видом аргумента.Основная причина та же, но сообщение об ошибке, очевидно, не было разработано с учетом вашего случая и не подходит.Вы должны отправить отчет об ошибке.

В дополнение, вам действительно нужны отдельные Unwrap и GetType?Почему бы не сделать GetType зависимым? 

type family GetType (pt :: Type) :: GetKind pt where
  GetType (PolyType k t) = t
...