Yes, I think using a singleton will solve your problem. It essentially acts like Proxy but keeps the parallelism between types and terms.

Here would be the definitions:

data Nat = Z | S Nat

-- This is the singleton type
data SNat (n :: Nat) where
SZ :: SNat Z
SS :: forall (n :: Nat). SNat n -> SNat (S n)

class NatToIntN (n :: Nat) where
natToIntN :: SNat n -> Int
instance NatToIntN Z where
natToIntN _ = 0
instance (NatToIntN n) => NatToIntN (S n) where
natToIntN (SS n) = 1 + natToIntN n

-------------
It might be worth noting that there is no need for a class to define natToIntN. The following would also work:

natToIntN :: SNat n -> Int
natToIntN SZ = 0
natToIntN (SS n) = 1 + natToIntN n

Please do check out our paper for more info at the link Pedro sent out.

Richard

On 6/7/12 8:28 AM, José Pedro Magalhães wrote:

Hi,

On Thu, Jun 7, 2012 at 2:46 AM, AntC <anthony_clayden@clear.net.nz> wrote:

What does the `ArgKind' message mean?

`ArgKind` and `OpenKind` is what previously was called `?` and `??` (or the other
way around; I can't remember).
http://hackage.haskell.org/trac/ghc/wiki/Commentary/Compiler/TypeType#Kindsubtyping

You might also want to have a look at Richard and Stephanie's latest paper draft, about
singletons, which is related to what you are trying in your example:
http://www.cis.upenn.edu/~eir/papers/2012/singletons/paper.pdf

Cheers,
Pedro
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users