伊德里斯统一惊人的失败

Question

我试图让人们可以称之为伊德里斯的可判断的分析器。起初我只是在分析自然数，但遇到了意想不到的问题。产生它的代码的最小例子是这样的：

data Digit : Char -> Type where 
    Zero : Digit '0' 
    One : Digit '1' 

digitToNat : Digit a -> Nat 
digitToNat Zero = 0 
digitToNat One = 1 

natToChar : Nat -> Char 
natToChar Z = '0' 
natToChar (S Z) = '1' 

natToDigit : (n : Nat) -> Digit (natToChar n) 
natToDigit Z = Zero 
natToDigit (S Z) = One 

我希望它可以编译，而是我得到

When elaborating right hand side of natToDigit: 
Can't unify 
     Digit '0' 
with 
     Digit (natToChar 0) 

Specifically: 
     Can't unify 
       '0' 
     with 
       natToChar 0 

但natToChar 0显然等于'0'，所以我不明白是什么这里的问题是。

更新

我还问了一个问题更直接关系到什么，我试图做here。

Answer 1

类型检查器不会减少natToChar，因为它不是全部 - 这基本上是为了防止您使用某个部分定义的函数来证明某些事情不是真实的。

如果你正在写这对数据的工作，其在运行时轮番上涨，可能你需要的是Dec或Maybe：

natToChar : (n : Nat) -> Maybe Char