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.
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
orMaybe
: