Idris에서 놀랄만 한 통합 실패

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' 동일 얻을, 내가 이해하지 못하는 것 여기 문제가 있습니다.

업데이트

은 또한 더 직접적으로 내가 here을하려고하고있는 무슨에 관련된 질문을했다.

Answer 1

유형 검사기는 총계가 아니기 때문에 natToChar을 줄이지 않습니다. 기본적으로 부분적으로 정의 된 함수를 사용하여 사실이 아닌 것을 증명하는 것을 방지합니다.

당신이 실행시까지 회전하는 데이터 작업이 작성하는 경우, 아마도 당신이 필요 Dec 또는 Maybe :

natToChar : (n : Nat) -> Maybe Char