Вывод типа GADT с типами высшего рода

У меня есть код, который компилируется:

{-# LANGUAGE ScopedTypeVariables, KindSignatures, GADTs, 
             FlexibleContexts #-}

module Foo where

data Foo :: (* -> *) where
  Foo :: c m zp' -> Foo (c m zp)

f :: forall c m zp d . Foo (c m zp) -> d
f y@(Foo (x :: c m a)) = g x y

g :: c m a -> Foo (c m b) -> d
g = error ""

Главное, что мне нужно в моем реальном коде, это убедить GHC, что если y имеет тип Foo (c m zp) а также x имеет тип c' m' zp', затем c' ~ c а также m' ~ m, Приведенный выше код достигает этого, потому что я могу позвонить g,

Я хочу изменить этот код двумя ортогональными способами, но я не могу понять, как заставить GHC скомпилировать код с любым изменением.

Первое изменение: Добавить -XPolyKinds, GHC 7.8.3 жалуется:

Foo.hs:10:11:
    Could not deduce ((~) (k2 -> k3 -> *) c1 c)
    from the context ((~) * (c m zp) (c1 m1 zp1))
      bound by a pattern with constructor
                 Foo :: forall (k :: BOX)
                               (k :: BOX)
                               (c :: k -> k -> *)
                               (m :: k)
                               (zp' :: k)
                               (zp :: k).
                        c m zp' -> Foo (c m zp),
               in an equation for ‘f’
      at Foo.hs:10:6-21
      ‘c1’ is a rigid type variable bound by
           a pattern with constructor
             Foo :: forall (k :: BOX)
                           (k :: BOX)
                           (c :: k -> k -> *)
                           (m :: k)
                           (zp' :: k)
                           (zp :: k).
                    c m zp' -> Foo (c m zp),
           in an equation for ‘f’
           at Foo.hs:10:6
      ‘c’ is a rigid type variable bound by
          the type signature for f :: Foo (c m zp) -> d
          at Foo.hs:9:13
    Expected type: c1 m1 zp'
      Actual type: c m a
    Relevant bindings include
      y :: Foo (c m zp) (bound at Foo.hs:10:3)
      f :: Foo (c m zp) -> d (bound at Foo.hs:10:1)
    In the pattern: x :: c m a
    In the pattern: Foo (x :: c m a)
    In an equation for ‘f’: f y@(Foo (x :: c m a)) = g x y

Foo.hs:10:11:
    Could not deduce ((~) k2 m1 m)
    from the context ((~) * (c m zp) (c1 m1 zp1))
    ...

Второе изменение: забыть о -XPolyKinds, Вместо этого я хочу использовать -XDataKinds создать новый вид и ограничить вид m:

{-# LANGUAGE ScopedTypeVariables, KindSignatures, GADTs, 
             FlexibleContexts, DataKinds #-}

module Foo where

data Bar

data Foo :: (* -> *) where
  Foo :: c (m :: Bar) zp' -> Foo (c m zp)

f :: forall c m zp d . Foo (c m zp) -> d
f y@(Foo (x :: c m a)) = g x y

g :: c m a -> Foo (c m b) -> d
g = error ""

Я получаю похожие ошибки (can't deduce (c1 ~ c), can't deduce (m1 ~ m)).DataKinds здесь уместно: если я ограничу m иметь вид Constraint вместо доброго Barкод компилируется нормально.

Я привел два примера того, как сломать исходный код, оба из которых используют типы с более высоким родом. Я пытался использовать case case вместо шаблонных охранников, я пытался дать тип node вместо xМои обычные трюки здесь не работают.

Я не требователен, где тип для x в конечном итоге / как это выглядит, я просто должен быть в состоянии убедить GHC, что если y имеет тип Foo (c m zp), затем x имеет тип c m zp' для некоторого несвязанного типа zp',

Источник

2 ответа

Решение

Я значительно упростил исходный вопрос до следующего, который компилируется без {-# LANGUAGE PolyKinds #-} но не компилируется с PolyKinds,

{-# LANGUAGE ScopedTypeVariables, KindSignatures, GADTs #-}
{-# LANGUAGE PolyKinds #-}

data Pair1 :: (* -> *) where
  Pair1 :: Pair1 (c a, c b)

data D p a where
    D :: p (a, b) -> D p a -> D p b

f :: forall c z. D Pair1 (c z) -> D Pair1 (c z)
f y@(D Pair1 x) |
    (_ :: D Pair1 (c z)) <- y,
    (_ :: D Pair1 (c z')) <- x = y

С PolyKinds включил ошибку компилятора

Could not deduce (c1 ~ c)
from the context ((a, c z) ~ (c1 a1, c1 b))

Эта ошибка говорит о том, что я уже подозревал, что ответ зависит от того, является ли приложение многоугольного типа инъективным. Если бы приложение типа polykinded было инъективным, мы могли бы вывести c1 ~ c следующее.

(a,   c z) ~ (c1 a1,   c1 b)
(a,) (c z) ~ (c1 a1,) (c1 b) {- switch to prefix notation -}
      c z  ~           c1 b  {- f a ~ g b implies a ~ b -}
      c    ~           c1    {- f a ~ g b implies f ~ g -}
      c1   ~           c     {- ~ is reflexive -}

Приложение типа Polykinded является инъективным, но ghc этого не знает. Чтобы ghc мог сделать вывод, что приложение типа является инъективным, нам нужно предоставить сигнатуры вида, чтобы компилятор знал, что типы эквивалентны.

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

Источник

Проблема может быть решена путем добавления добрых подписей.

Например, при использовании -XPolyKinds, следующий код компилируется:

{-# LANGUAGE ScopedTypeVariables, KindSignatures, GADTs, 
             FlexibleContexts, PolyKinds #-}

module Foo where

data Foo :: (* -> *) where
  Foo :: (c :: k -> * -> *) m zp' -> Foo (c m zp)

f :: forall (c :: k -> * -> *) m zp d . Foo (c m zp) -> d
f y@(Foo x) = g x y

g :: c m a -> Foo (c m b) -> d
g = error ""

Для -XDataKinds версия, мне тоже нужна добрая подпись на g:

{-# LANGUAGE ScopedTypeVariables, KindSignatures, GADTs, 
             FlexibleContexts, DataKinds #-}

module Foo where

data Bar

data Foo :: (* -> *) where
  Foo :: (c :: Bar -> * -> *) m zp' -> Foo (c m zp)

f :: forall (c :: Bar -> * -> *) m zp d . Foo (c m zp) -> d
f y@(Foo x) = g x y

g :: forall (c :: Bar -> * -> *) m a b d . c m a -> Foo (c m b) -> d
g = error ""

Не уверен, почему мне нужно больше сигналов для DataKindsи это немного раздражает, когда приходится копировать их повсюду, но это делает работу.

Источник
Другие вопросы по тегам