GHC.TypeLits에서 비교를 사용하는 방법

Question

GHC.TypeLits과 관련된 문제가 발생했습니다. 다음 GADT을 고려

data Foo :: Nat -> * where 
    SmallFoo :: (n <= 2) => Foo n 
    BigFoo :: (3 <= n) => Foo n 

나의 이해는 이제 모든 n를 들어, 유형 Foo n의 (a SmallFoo 또는 n의 값에 따라 BigFoo 중 하나 인) 정확히 하나 개의 값으로 채워집니다이었다. 다음과 같이 지금 구체적인 인스턴스를 구성하려면

는하지만 :

myFoo :: Foo 4 
myFoo = BigFoo 

그런 GHC를 (7.6.2)는 다음과 같은 오류 메시지가 뱉어 :

No instance for (3 <= 4) arising from a use of `BigFoo' 
Possible fix: add an instance declaration for (3 <= 4) 
In the expression: BigFoo 
In an equation for `myFoo': myFoo = BigFoo 

이 이상한 것을 - I 이러한 유형 수준의 nat 비교에 대해 미리 정의 된 인스턴스가 있어야합니다. 유형 생성자를 사용하여 데이터 생성자에서 이러한 종류의 제약을 어떻게 표현할 수 있습니까?

Answer 1

TypeLists 용 솔버는 현재 GHC에 없습니다. status page에 따르면 10 월에 GHC 7.8 또는 일부 기능을 수행 할 가능성이 있습니다.

지금은 other packages을 사용하는 것이 더 좋을지도 모릅니다.

Answer 2

이것은 type-nats 브랜치의 현재 헤드에서 컴파일됩니다. (잘하면) 7.8로 병합되어야합니다.

$ /Source/ghc/inplace/bin/ghc-stage1 /tmp/blah.hs 
[1 of 1] Compiling X    (/tmp/blah.hs, /tmp/blah.o) 

/tmp/blah.hs:16:13: 
    Couldn't match type ‛3 <=? 1’ with ‛'True’ 
    In the expression: BigFoo 
    In an equation for ‛myFoo’: myFoo = BigFoo 

:

{-# LANGUAGE DataKinds #-} 
{-# LANGUAGE FlexibleContexts #-} 
{-# LANGUAGE GADTs #-} 
{-# LANGUAGE KindSignatures #-} 
{-# LANGUAGE TypeOperators #-} 

module X where 

import GHC.TypeLits 

data Foo :: Nat -> * where 
    SmallFoo :: (n <= 2) => Foo n 
    BigFoo :: (3 <= n) => Foo n 

myFoo :: Foo 4 
myFoo = BigFoo 

myFoo 경우는 종류가 x <= y 클래스 제약 조건이 (x <=? y) ~ 'True 평등 제약으로 확장됩니다 아마도 때문에, 컴파일에 실패 Foo 1의로 변경