parsing - イドリス統一の驚くべき失敗

Question

Idris で決定可能なパーサーと呼ばれるものを作ろうとしています。最初は自然数の解析だけを見ていましたが、予期しない問題に遭遇しました。それを生成するコードの最小限の例は次のとおりです。

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'ので、ここで何が問題なのかわかりません。

アップデート

また、私がここでやろうとしていることにより直接的に関連する質問もしました。