Exploring kind-indexed type constraints in GHC 7.6

GHC_Query

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

-- this gist demonstrates some GHC 7.6 behaviors that I'm seeing as some type errors (example at the bottom).

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))

-- constrains @ts@ to be a list of @()s@ that is @n@ long
class NUnits (n :: Nat) (ts :: [k])

instance ('[] ~ ps) => NUnits Z ps
instance ((() ': pstail) ~ ps, NUnits n pstail) => NUnits (S n) ps

-- a handle to test the behavior of NUnits
-- (I get the same behaviors if I fold CountArgs into the declaration
--  and instances of NUnits)
demonstrate_NUnits :: NUnits (CountArgs ('KindProxy :: KindProxy k)) ts =>
  Proxy (t :: k) -> Proxy (ts :: [*])
demonstrate_NUnits _ = Proxy

{- some NUnit behaviors

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

-- the above looks correct; k is unconstrained, so nothing is known about ts

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

-- apparently k defaults to *; but now shouldn't NUnits accordingly constrain ts to be '[]?

-- note that @NUnits * (CountArgs * ('KindProxy *)) ts@, if simplified, matches an instance head,
-- but remains unsimplified

*GHC_Query> :t demonstrate_NUnits (Proxy :: Proxy Int)
demonstrate_NUnits (Proxy :: Proxy Int) :: Proxy [*] ('[] *)

-- if we provide Int, that forces k to * and then ts _is_ subsequently forced to be '[]: the
-- NUnit constraint has been reduced and ts expanded accordingly

*GHC_Query> :t demonstrate_NUnits (Proxy :: Proxy (,,))
demonstrate_NUnits (Proxy :: Proxy (,,))
  :: Proxy [*] ((':) * () ((':) * () ((':) * () ('[] *))))

-- it also works the same way at higher kinds; that last type is just '[(), (), ()]

-}

{-

As in the case where NUnit is unexpectedly not simplified, I get this error from the instance of CLASS below.

    Could not deduce (ts ~ '[] *)
    from the context (NUnits * ('KindProxy *) ts)

I believe GHC can deduce that--it _does_ deduce that in the Proxy Int example behavior above, but not in the ":t demonstrate_NUnits" case and not in the following instance.

-}

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

class CLASS (t :: k) where
  method :: NUnits (CountArgs ('KindProxy :: KindProxy k)) ts => Proxy t -> GADT ts

-- this instance causes the error
instance CLASS (t :: *) where method _ = GZ