8

GHC.TypeLitsで遊んでいると問題が発生しました。次の GADT を検討してください。

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

私の理解では、すべてnの について、型Foo nには 1 つの値 ( の値に応じて SmallFoo または BigFoo のいずれか) が入力されますn

しかし、次のように具体的なインスタンスを構築したい場合:

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

これは奇妙に思えます。私は、そのようなタイプ レベルの nat 比較用に定義済みのインスタンスがあることを期待していました。型レベルのナチュラルを使用して、データ コンストラクターでこれらの種類の制約を表現するにはどうすればよいですか?

4

2 に答える 2