Kindness of strangers (or strangeness of Kinds)

6 Jun 2012

      I'm confused about something with promoted Kinds (using an example with Kind-
promoted Nats).

This is in GHC 7.4.1. (Apologies if this is a known bug/limitation/already 
explained somewhere -- I know 7.4.1 is relatively experimental. I have 
searched the bug tracs and discussions I could find.)

Starting with nats at type level, this works fine:

{-# OPTIONS_GHC -XTypeFamilies -XFlexibleInstances -XUndecidableInstances
                -XScopedTypeVariables #-}

    data ZeT;	data SuT n

    class NatToIntT n
        where natToIntT :: n -> Int
    instance NatToIntT ZeT
        where natToIntT _ = 0
    instance (NatToIntT n) => NatToIntT (SuT n)
        where natToIntT _ = 1 + natToIntT (undefined :: n)

I converted naively to promoted Kinds:

{-# OPTIONS_GHC -XDataKinds -XPolyKinds -XKindSignatures	#-}

    data MyNat = Z | S Nat

    class NatToIntN (n :: MyNat)
        where natToIntN :: (n :: MyNat) -> Int
    instance NatToIntN Z
        where natToIntN _ = 0
    instance (NatToIntN n) => NatToIntN (S n)
        where natToIntN _ = 1 + natToInt (undefined :: n)

But GHC rejects the class declaration (method's type):
    "Kind mis-match
     Expected kind `ArgKind', but `n' has kind `MyNat'"
(Taking the Kind signature out of the method's type gives same message.)

Eh? MyNat is what I want the argument's Kind to be.

A PolyKinded version (cribbed from 'Giving Haskell a Promotion' on multi-
kinded TypeRep) also works fine:

    data Proxy a = Proxy

    class NatToInt (n :: MyNat)
        where natToInt :: Proxy (n :: MyNat) -> Int
    instance NatToInt Z	
        where natToInt _ = 0
    instance (NatToInt n) => NatToInt (S n)
        where natToInt _ = 1 + natToInt (Proxy :: Proxy n)

But this seems too Kind. I only ever want to supply Nats as arguments.

What does the `ArgKind' message mean?

(I've also seen messages with `AnyKind' -- what that?)

There's a discussion in SPJ's Records proposal last year 
http://hackage.haskell.org/trac/ghc/wiki/Records/OverloadedRecordFields#Shou...
ethaveaproxyargument
Is that related?

Do I need explicit Type/Kind application for this to work?

AntC