为什么 Idris 中的依赖类型不能处理这种情况？

Question

我想做以下事情：

data Foo : (a : Type) -> (b : Type) -> (c : a -> b -> Type) -> Type where
  Bar : a -> (c a) -> Foo a b c

但我收到以下错误：

When checking type of test.Bar:
When checking argument c to test.Foo:
    Type mismatch between
            Type -> Type (Type of c)
    and
            a -> b -> Type (Expected type)

    Specifically:
            Type mismatch between
                    Type
            and
                    b -> Type

这对我来说似乎应该是有效的。那就是c 在表达式Foo a b c 中有正确的类型，但Idris 认为它​​的类型是b -> Type，或者我认为的(c a)。

是我遗漏了什么，还是 Idris 的限制？

Answer 1

(c a) 的类型为b -> Type，而数据构造函数的所有字段都必须为Type 的类型。正如伊德里斯所说，这是一个错误。您的 c 类型构造函数接受两个参数，但您仅将其应用于单个 a。