Exploring kind-indexed type constraints in GHC 7.6

GHC_Query

{-# LANGUAGE PolyKinds, GADTs, DataKinds, TypeFamilies, TypeOperators,
  MultiParamTypeClasses, FlexibleContexts, FlexibleInstances,
  UndecidableInstances #-}

module GHC_Query where

data Proxy (t :: k) = Proxy
data KindProxy (t :: *) = KindProxy  -- a type-level proxy for kinds

data Nat = Z | S Nat

-- count the number of type arguments that the kind specifies
type family CountArgs (kp :: KindProxy k) :: Nat
type instance CountArgs (kp :: KindProxy *) = Z
type instance CountArgs (kp :: KindProxy (kD -> kR))
  = S (CountArgs ('KindProxy :: KindProxy kR))

class NUnits (n :: Nat) where type Ts n :: [k]

instance NUnits Z where type Ts Z = '[]
instance NUnits n => NUnits (S n) where type Ts (S n) = () ': Ts n

-- a handle to test the behavior of NUnits
demonstrate_NUnits :: (n ~ CountArgs ('KindProxy :: KindProxy k), NUnits n) =>
  Proxy (t :: k) -> Proxy (Ts n :: [*])
demonstrate_NUnits _ = Proxy

data GADT :: [*] -> * where
  GZ :: GADT '[]
  GS :: GADT ts -> GADT (() ': ts)

class CLASS (t :: k) where
  method :: (n ~ CountArgs ('KindProxy :: KindProxy k), NUnits n) => Proxy t -> GADT (Ts n)

-- this compiles now
instance CLASS (t :: *) where method _ = GZ

-- testing in GHCi
{-

*GHC_Query> :i demonstrate_NUnits
demonstrate_NUnits ::
  (n ~ CountArgs k ('KindProxy k), NUnits n) =>
  Proxy k t -> Proxy [*] (Ts * n)
  	-- Defined at frisby.hs:31:1

-- I think :i just regurgitates the signature from the source file?

*GHC_Query> :t demonstrate_NUnits
demonstrate_NUnits
  :: NUnits (CountArgs * ('KindProxy *)) =>
     Proxy * t -> Proxy [*] (Ts * (CountArgs * ('KindProxy *)))

-- Uses * instead of k as before, substitutes in our 'n' tyvar, doesn't simplify the output type (as before)

*GHC_Query> :set -XPolyKinds -XDataKinds
*GHC_Query> :t demonstrate_NUnits
demonstrate_NUnits
  :: NUnits (CountArgs k ('KindProxy k)) =>
     Proxy k t -> Proxy [*] (Ts * (CountArgs k ('KindProxy k)))

-- Now it's using k

*GHC_Query> :t demonstrate_NUnits (Proxy :: Proxy Int)
demonstrate_NUnits (Proxy :: Proxy Int) :: Proxy [*] (Ts * 'Z)
*GHC_Query> :t demonstrate_NUnits (Proxy :: Proxy Maybe)
demonstrate_NUnits (Proxy :: Proxy Maybe)
  :: Proxy [*] (Ts * ('S 'Z))
*GHC_Query> :t demonstrate_NUnits (Proxy :: Proxy (,))
demonstrate_NUnits (Proxy :: Proxy (,))
  :: Proxy [*] (Ts * ('S ('S 'Z)))

-- It's still not simplifying the output type, but this might be just a for-display thing
-- Wasn't there a version of :t added at some point which simplified away type functions? :t! or :k! or something? neither of those were recognized when I tried them
-- anyway, using the usual workaround...

*GHC_Query> show $ demonstrate_NUnits (Proxy :: Proxy Int)

<interactive>:9:1:
    No instance for (Show (Proxy [*] ('[] *)))
      arising from a use of `show'
    Possible fix:
      add an instance declaration for (Show (Proxy [*] ('[] *)))
    In the expression: show
    In the expression: show $ demonstrate_NUnits (Proxy :: Proxy Int)
    In an equation for `it':
        it = show $ demonstrate_NUnits (Proxy :: Proxy Int)

-- Now we see that it does get the correct type

*GHC_Query> show $ demonstrate_NUnits (Proxy :: Proxy Maybe)

<interactive>:10:1:
    No instance for (Show (Proxy [*] ((':) * () ('[] *))))
      arising from a use of `show'
    Possible fix:
      add an instance declaration for
      (Show (Proxy [*] ((':) * () ('[] *))))
    In the expression: show
    In the expression: show $ demonstrate_NUnits (Proxy :: Proxy Maybe)
    In an equation for `it':
        it = show $ demonstrate_NUnits (Proxy :: Proxy Maybe)

-- Also the correct type

*GHC_Query> show $ demonstrate_NUnits (Proxy :: Proxy (,))

<interactive>:11:1:
    No instance for (Show (Proxy [*] ((':) * () ((':) * () ('[] *)))))
      arising from a use of `show'
    Possible fix:
      add an instance declaration for
      (Show (Proxy [*] ((':) * () ((':) * () ('[] *)))))
    In the expression: show
    In the expression: show $ demonstrate_NUnits (Proxy :: Proxy (,))
    In an equation for `it':
        it = show $ demonstrate_NUnits (Proxy :: Proxy (,))

-- Also the correct type
-- Let's try something else

*GHC_Query> let foo :: Proxy '[]; foo = demonstrate_NUnits (Proxy :: Proxy Int)

<interactive>:12:29:
    Couldn't match kind `k' with `*'
      `k' is a rigid type variable bound by
          the type signature for foo :: Proxy [k] ('[] k)
          at <interactive>:12:12
    Expected type: Proxy [k] ('[] k)
      Actual type: Proxy [*] (Ts * 'Z)
    In the return type of a call of `demonstrate_NUnits'
    In the expression: demonstrate_NUnits (Proxy :: Proxy Int)
    In an equation for `foo':
        foo = demonstrate_NUnits (Proxy :: Proxy Int)

-- Hmm, that's not right... but it works if we add a kind signature:

*GHC_Query> let foo :: Proxy ('[] :: [*]); foo = demonstrate_NUnits (Proxy :: Proxy Int)

-- And higher kinds also work:

*GHC_Query> let foo :: Proxy '[()]; foo = demonstrate_NUnits (Proxy :: Proxy Maybe)
*GHC_Query> let foo :: Proxy '[(), ()]; foo = demonstrate_NUnits (Proxy :: Proxy (,))

-}