无法声明 MonadPlus 接口受 Monad 约束

我试图像这样声明 MonadPlus 接口：

module NanoParsec.Plus

%access public export

interface Monad m => MonadPlus m where
    zero : m a
    plus : m a -> m a -> m a

但有一个错误：

  |
5 | interface Monad m => MonadPlus m where
  |           ~~~~~~~
When checking type of constructor of NanoParsec.Plus.MonadPlus#Monad m:
When checking argument m to type constructor Prelude.Monad.Monad:
        Type mismatch between
                Type (Type of m)
        and
                Type -> Type (Expected type)

我做错了什么？如何解决这个问题？ Idris 没有自己的 MonadPlus 接口，我说得对吗？如果是这样，为什么？

在Idris中，定义接口时，参数类型默认为Type, so MonadPlus m这是缩写MonadPlus (m: Type)，伊德里斯对待m as a Type。这当然不符合约束条件Monad m，它期望Type -> Type.

如果你想对其他东西进行参数化，你必须明确，比如

interface Monad m => MonadPlus (m: Type -> Type) where
    zero : m a
    plus : m a -> m a -> m a

MonadPlus它本身超出了我的知识范围，所以我不知道它在伊德里斯中是否存在。