图案上的类型的计算功能在伊德里斯结果

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 

是否有可能迫使type期间或y类型归属之前进行评估，从而使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'视为一个类型参数。你可以给'type'一个以大写字母开头的新名字（按照惯例，这是大多数人在Idris中做的），或者你可以明确地使用它所在的模块（Main，here）来限定名字。

Idris用于尝试猜测名称（如'type'）是作为隐式还是意图指向全局，如此处所示。尽管如此，所有这些都涉及到巫术，所以它经常失败，所以它现在实现了这个更简单的规则。在这种情况下，这有些恼人，但另一种行为往往更令人讨厌（而且更难以解释）。