如何处理 Agda 不确定是否在 with 语句中生成构造函数的情况？

我有以下代码：

open import Data.Nat
open import Agda.Builtin.Char
open import Data.Maybe

digit' : ℕ → Maybe ℕ
digit' n with compare n (primCharToNat '9')
... | greater _ _ = nothing
... | _ = ?

digit : Char → Maybe ℕ
digit c = digit' (primCharToNat c)

不幸的是，emacs 中的 Agda“加载文件”命令失败并显示以下消息：

tmp.agda:7,1-8,12
I'm not sure if there should be a case for the constructor less,
because I get stuck when trying to solve the following unification
problems (inferred index ≟ expected index):
  m ≟ n
  suc (m + k) ≟ 57
when checking the definition of with-6

据我了解，Agda 认为primCharToNat '9'是一个常数，不确定是否有任何前提条件n总是小于primCharToNat '9'（57）。因此，不确定是否应该生成less情况（我认为情况也是如此equal案件）。我可以以某种方式强制 Agda 生成所有案例吗？

背景：我正在尝试写一个digit : Char → Maybe ℕ应该返回的函数just x如果传递的字符是十进制数字或nothing如果不是的话。我考虑以下算法：将参数转换为自然数（可能是 ASCII 代码）primCharToNat然后将其与primCharToNat '0' and primCharToNat '9'.

一个可能的解决方案在于抽象primCharToNat '9':

digit' : ℕ → Maybe ℕ
digit' n with primCharToNat '9' | compare n (primCharToNat '9')
... | _ | greater _ _ = nothing
... | _ | _ = {!!}