idris中类型计算函数结果的模式匹配

Question

考虑以下片段：

import Data.List

%default total

x : Elem 1 [1, 2]
x = Here

type : Type
type = Elem 1 [1, 2]

y : type
y = Here

这给出了错误：

检查 y 的右侧时： 类型不匹配 Elem x (x :: xs) (这里的类型) 和 iType（预期类型）

y的类型，查询时为：

type : Type
-----------
y : type

是否可以在y的类型归属期间或之前强制评估type，使y的类型为Elem 1 [1, 2]？

我的用例是我希望能够定义通用谓词，以返回正确的命题术语以进行证明，例如：

subset : List a -> List a -> Type
subset xs ys = (e : a) -> Elem e xs -> Elem e ys

thm_filter_subset : subset (filter p xs) xs

Answer 1

类型声明中以小写字母开头的名称是隐式绑定的，因此它将“类型”视为类型参数。您可以给“type”一个以大写字母开头的新名称（按照惯例，这是大多数人在 Idris 中所做的），或者您可以使用它所在的模块明确限定名称（Main，here）。

Idris 曾经尝试猜测诸如“类型”之类的名称是隐含的还是意指全局的，就像这里一样。但是，要做到这一点，需要各种巫术，所以它经常失败，所以它现在实现了这个更简单的规则。在这种情况下有点烦人，但另一种行为通常更烦人（而且更难解释）。