How to use the comparison in GHC.TypeLits

Question

I ran into problems playing with GHC.TypeLits. Consider the following GADT:

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

My understanding was, that now for every n, the type Foo n is populated by exactly one value (which is either a SmallFoo or a BigFoo depending on the value of n).

But if I now want to construct a concrete instance as follows:

myFoo :: Foo 4
myFoo = BigFoo

Then GHC (7.6.2) spits out the following error message:

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

This seems odd - I expected there to be a predefined instance for such type level nat comparisons. How can I express these kinds of constraints in my data constructor using type level naturals?

Answer 1

Solver for TypeLists is not in GHC right now, according to status page there are some chances that it will be in GHC 7.8 in october or something.

Maybe it's better to use other packages for now.

Answer 2

This compiles on the current head of the type-nats branch, which should (hopefully) be merged for 7.8.

{-# 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

Where if myFoo is changed to be of type Foo 1 it fails to compile, presumably because the x <= y class constraint is expanded to the (x <=? y) ~ 'True equality constraint:

$ /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