依赖型签名中的多态常量？

Question

假设我想定义一种类型的证明，某些向量具有一定的总和。我也喜欢这个证据适用于任何Monoid型t。我的第一次尝试是这样的：

data HasSum : Monoid t => t -> Vect n t -> Type where
    EndNeutral : Monoid t => HasSum Prelude.Algebra.neutral []
    Component : Monoid t => (x : t) -> HasSum sum xs -> HasSum (x <+> sum) (x :: xs)

不幸的是，编译器认为它是Can't find implementation for Monoid t。所以我尝试使用隐式参数，以便我可以指定其类型：

    EndNeutral : Monoid t => {Prelude.Algebra.neutral : t} -> HasSum Prelude.Algebra.neutral []

这编译，但这不是：

x : HasSum 0 []
x = EndNeutral

奇怪地声称它Can't find implementation for Monoid Integer。

我最后的尝试是用大写字母名称定义一个助手常量，这样Idris就不会把它混淆为一个绑定变量：

ZERO : Monoid t => t
ZERO = neutral

data HasSum : Monoid t => t -> Vect n t -> Type where
    EndNeutral : Monoid t => HasSum ZERO []
    Component : Monoid t => {rem : t} -> (x : t) -> HasSum rem xs -> HasSum (x <+> rem) (x :: xs)

但现在它无法猜测ZERO（EndNeutral）定义中Can't find implementation for Monoid t的类型。所以我再次尝试使用隐式绑定：

    EndNeutral : Monoid t => {ZERO : t} -> HasSum ZERO []

但现在ZERO成为一个绑定变量，虽然它编译，但它不能按预期工作，因为它允许构造一个具有任意和的空矢量证明。

在这一点上，我没有想法。有谁知道如何在Idris类型中表达多态常量？

Answer 1

好像我终于找到了答案。它可能不是最好的，但它是我现在唯一知道的。所以需要明确指定neutral的类型而不添加隐式参数（这会将neutral转换为绑定变量）。当然，功能the可以达到这个目的：

data HasSum : Monoid t => t -> Vect n t -> Type where
    EndNeutral : Monoid t => HasSum (the t Prelude.Algebra.neutral) []
    Component : Monoid t => {rem : t} -> (x : t) -> HasSum rem xs -> HasSum (x <+> rem) (x :: xs)

编辑：

看看neutral的类型提出了另一个解决方案：

> :doc neutral
Prelude.Algebra.neutral : Monoid ty => ty

看来neutral的具体类型实际上是它的隐含论据。因此：

EndNeutral : Monoid t => HasSum (Prelude.Algebra.neutral {ty = t}) []

也有效。