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

问题描述

我是 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

这是一个错误吗？

最初，我试图证明一个应该很明显的愚蠢定理，但 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

解决方法

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

在检查 Pi 活页夹时纠正多重性

我们一直只使用 0，如果函数运行，这是不正确的 用于运行时模式匹配。现在正确计算，以便 我们明确说明了在运行时使用了哪些类型级别的变量。

这可能会导致一些程序无法编译，如果他们使用 计算 Pi 类型的函数。解决办法是让那些 函数显式为 0 多重性。如果这不起作用，你可以 不小心尝试在运行时仅使用编译时数据 时间！

修复 #1163

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

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