Surprising failure of unification in Idris

问题:

I'm trying to make what one might call a decidable parser in Idris. At first I am just looking at parsing natural numbers, but have ran into an unexpected problem. A minimum example of the code that produces it is this:

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

I would expect this to compile, but instead I get

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

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

But natToChar 0 clearly equals '0', so I don't understand what the problem here is.

Update

I have also asked a question more directly related to what I am trying to do here.

回答1:

The type checker won't reduce natToChar because it isn't total - this is basically to prevent you using some partially defined function to prove something which isn't true.

If you're writing this to work on data which turns up at run-time, possibly what you need is Dec or Maybe:

natToChar : (n : Nat) -> Maybe Char