在Idris2中，不能直接检查if then else类型

Question

我是Idris的初学者。在Idris2版本0.3.0中，我观察到一个奇怪的行为。

为什么不检查代码类型？

f : Type -> Type -> Type
f a b = (c : Bool) -> if c then a else b

While processing right hand side of f. Main.case block in f is not accessible in this context.

虽然此代码类型检查没有问题：

f1 : Type -> Type -> Bool -> Type
f1 a b c = if c then a else b
f' : Type -> Type -> Type
f' a b = (c : Bool) -> f1 a b c

这是一个bug吗？

最初，我试图证明一个愚蠢的定理，它应该是显而易见的，但Refl不起作用。看起来它无法理解变量是否匹配。

module Main
import Data.Nat

t : Nat -> Nat -> Nat
t l r = if lte l r then l else r

prop : Nat -> Nat -> Type
prop a b = (t a b = if lte a b then a else b)

proof_prop : prop a b
proof_prop = ?imlost

Answer 1

在commit 04a0f5001f中使用程序的if_then_else_开始失败

检查Pi绑定器时的

正确重数

我们总是使用0，如果函数要在运行时模式匹配中使用，这是不正确的。现在正确计算，这样我们就可以清楚地知道在运行时使用了哪些类型级别的变量。

如果使用计算Pi类型的函数，这可能会导致某些程序无法编译。解决方案是显式地使这些函数为0重数。如果这不起作用，那么您可能无意中试图在运行时使用编译时数据！

修复#1163

解决方案是将f函数标记为仅限类型级别：

0 f : Type -> Type -> Type
f a b = (c : Bool) -> if c then a else b