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 比較用に定義済みのインスタンスがあることを期待していました。型レベルのナチュラルを使用して、データ コンストラクターでこれらの種類の制約を表現するにはどうすればよいですか?