伊德里斯統一驚人的失敗

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