데이터 킨으로 놀기 - 잘못된 매치 오류

Question

나는 타입 레벨 프로그래밍에 대해 가르쳐 왔으며 간단한 자연수 덧셈 형 함수를 작성하려고했다. 다음과 같이 작동 나의 첫 번째 버전은 다음과 같습니다

data Z 
data S n 

type One = S Z 
type Two = S (S Z) 

type family Plus m n :: * 
type instance Plus Z n = n 
type instance Plus (S m) n = S (Plus m n) 

그래서 GHCi에서 내가 할 수있는 : 예상대로 작동

ghci> :t undefined :: Plus One Two 
undefined :: Plus One Two :: S * (S * (S * Z)) 

.

data Nat = Z | S Nat 

그리고 플러스 제품군은 이제 Nat 종류의 반환 :

type family Plus m n :: Nat 

문제가 있지만, 수정 된 코드는 컴파일 난 다음에 Z 및 S 유형을 수정하여 DataKinds 확장을 시도하기로 결정 테스트 할 때 오류가 발생합니다.

Kind mis-match 
Expected kind `OpenKind', but `Plus One Two' has kind `Nat' 
In an expression type signature: Plus One Two 
In the expression: undefined :: Plus One Two 

Google에서 해결책을 찾았지만 실패했습니다. . 해결책이 존재합니까? 아니면 언어의 한계에 부딪 혔습니까?

Answer 1

테스트 방법이 올바르지 않다고 생각합니다. undefined은 종류가 * 인 모든 유형이 될 수 있습니다 (아마도 여기에 잘못되었습니다). 종류 :

당신은 여전히`ghci에

ghci>:kind! Plus One Two 
Plus One Two :: Nat 
= S (S (S 'Z))