Неоднозначная переменная вида с PolyKinds

Question

Учитывая следующий код

{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE PolyKinds #-}

type family Tagged (m :: * -> *) :: k

class Example (t :: k) (a :: *) where
  type Return t a
  a :: (Monad m, Tagged m ~ t) => a -> m (Return t a)

data A
data A' a
data B = B

instance Example A B where
  type Return A B = ()
  a B = return ()

-- This is why I want a PolyKinded 't'
instance Example A' B where
  type Return A' B = ()
  a B = return ()

Я получаю ошибку типа (указывая на строку a :: (Monad m ...)

• Could not deduce: Return (Tagged m) a ~ Return t a
  from the context: (Example t a, Monad m, Tagged m ~ t)
    bound by the type signature for:
               a :: (Example t a, Monad m, Tagged m ~ t) =>
                    a -> m (Return t a)
...
  Expected type: a -> m (Return t a)
    Actual type: a -> m (Return (Tagged m) a)
  NB: ‘Return’ is a type function, and may not be injective
  The type variable ‘k0’ is ambiguous
• In the ambiguity check for ‘a’
  To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
  When checking the class method:
    a :: forall k (t :: k) a.
         Example t a =>
         forall (m :: * -> *).
         (Monad m, Tagged m ~ t) =>
         a -> m (Return t a)
  In the class declaration for ‘Example’

Я могу представить аргумент a с Proxy t и это будет работать, если я дам подпись на сайте вызова: test = a (Proxy :: Proxy A) B но это то, чего я хочу избежать. Что я хотел бы это

newtype Test t m a = Test
  { runTest :: m a
  } deriving (Functor, Applicative, Monad)

type instance Tagged (Test t m) = t

test :: Monad m => Test A m ()
test = a B

я хочу t быть найденным из контекста Test A m () используя экземпляр типа. Кажется, что это должно быть возможно, если модуль будет скомпилирован после удаления аннотаций вида, PolyKindsи экземпляр для A', Где k0 приходящий из?

Я полагаю, что обходной путь должен был бы удалить PolyKinds и использовать дополнительные типы данных, такие как data ATag; data A'Tag; data BTag и т.п.

Answer 1

Это только частичный ответ.

Я пытался сделать вид явным.

type family Tagged k (m :: * -> *) :: k

class Example k (t :: k) (a :: *) where
  type Return k (t :: k) (a :: *)
  a :: forall m . (Monad m, Tagged k m ~ t) => a -> m (Return k t a)

И, после включения многих расширений, заметил это:

> :t a
a :: (Example k (Tagged k m) a, Monad m) =>
     a -> m (Return k (Tagged k m) a)

Следовательно, компилятор жалуется, потому что экземпляр Example k (Tagged k m) a не может быть определено a,m в одиночестве. То есть мы не знаем как выбрать k,

Я думаю, что технически у нас могут быть разные Example k (Tagged k m) a экземпляры, например, один для k=* и еще один для k=(*->*),

Интуитивно, зная t должен позволить нам найти k, но Return неинъективность мешает нам найти t,