%hint 注释是否导入/Dec 和自动注释？

Question

我有一个依赖于谓词 P : a -> Type 的数据类型，这意味着它的一些数据构造函数引用了一个隐式 P x 作为参数。我希望 idris 能够自动推断出这个隐含的。为此，我使用关键字 auto 对隐式进行了注释，并在类型声明之前编写了一个带有 %hint 注释的函数 isP : (x : a) -> Dec (P x)。即，类似：

module P

P : a -> Type

%hint
isP : (x : a) -> Dec (P x)

在一个单独的文件中

module Main

import P

data Foo : Type where
  Bar : (x : a) -> .{auto prf : P x} -> Foo

也就是说，我不能声明 Foo 类型的值，因为 Idris 声称它无法推断 prf。

这是因为 prf 的类型是 P x 而不是 Dec (P x) 还是因为没有导入 %hint 标志？

在任何一种情况下，如何让 Idris 使用 Dec 值来尝试查找隐式？

Answer 1

%hint 标志被导入，正如你猜想的那样，这是因为 Dec (P x) 与 P x 不同。

不过有一个技巧，你可以使用这个数据类型：

data IsYes : prop -> Type where
  SoTrue : IsYes (Yes prop)

（基本上，您定义了一个包含给定属性的Yes 的类型） 然后您可以使用default 而不是auto 来检查该属性是否成立：

data Foo : Type where
  Bar : (x : a) -> .{default SoTrue prf : IsYes (isP x)} -> Foo

注意：有了这个技巧，你甚至不再需要%hint，你只需在编译时检查isP 的结果。