haskell - PolyKinds 的模糊种类变量

鉴于以下代码

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

最佳答案

这只是部分答案。

我试图使这种类型明确。

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 。

关于haskell - PolyKinds 的模糊种类变量，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/47200944/