Idris2中Parity示例编译报错：j在此上下文不可访问问题求助

错误原因 #

Idris 2 0.7.0对with块的作用域处理逻辑和Idris 1有显著差异：Idris 1会自动将with匹配过程中产生的绑定变量（比如示例中的j）暴露给分支的模式匹配上下文，但Idris 2对作用域做了更严格的限制，不会自动提升这类变量，导致你在分支模式中引用j时出现“不可访问”的错误。这和multiplicity无关，核心是作用域规则的变化。

修复方案 #

假设你的原始代码类似以下结构：

data Parity : Nat -> Type where
  Even : Parity (n + n)
  Odd  : Parity (S (n + n))

helpEven : (j : Nat) -> Parity j -> Parity (S j)
helpEven j Even = Odd {n = S j}
helpEven j Odd  = Even {n = j}

helpOdd : (j : Nat) -> Parity j -> Parity (S j)
helpOdd j Even = Odd {n = j}
helpOdd j Odd  = Even {n = S j}

parity : (n : Nat) -> Parity n
parity Z = Even {n=Z}
parity (S k) with (parity k)
  parity (S (j + j))     | Even = Odd {n=j}
  parity (S (S (j + j))) | Odd  = Even {n=S j}

可以通过直接从Parity构造函数中提取绑定变量来修复，不需要在分支的左侧模式中展开k的结构：

parity : (n : Nat) -> Parity n
parity Z = Even {n=Z}
parity (S k) with (parity k)
  parity (S k) | Even {n=j} = Odd {n=j}
  parity (S k) | Odd {n=j}  = Even {n=S j}

原理说明 #

修改后，我们直接从Even/Odd构造函数的命名参数中获取j，而不是依赖with块自动传递模式匹配产生的变量。Idris 2会自动推导k和j的关系（比如k = j + j对应Even分支），完全满足类型检查要求，同时避免了作用域问题。

如果需要保留左侧的模式匹配写法，也可以通过proof参数显式捕获with块的上下文，但这种写法更繁琐：

parity : (n : Nat) -> Parity n
parity Z = Even
parity (S k) with (parity k) proof p
  parity (S k) | Even = case k of
    j + j => Odd {n=j}
  parity (S k) | Odd = case k of
    S (j + j) => Even {n=S j}

内容的提问来源于stack exchange，提问作者Johnny Liao