Demonstration of the usefulness of NLong for type inference

further notes

I'm still in the experimentation stage and cannot completely explain/defend my design decisions.

The big picture is: this code is working as a polyvariadic version of generic-deriving. I've run
into the issue that my original email "seemingly inconsistent behavior for "kind-indexed" type
constraints in GHC 7.6" to the glasgow-haskell-users list is about when trying to add support
for representing indexed data types in a way that is 1) congruent with GHC's elaboration of
GADTs, and 2) uniquely (I think) enabled by the polyvariadism of my technique.

Like I said, I'm not certain about all of my design decisions. In particular, if you're wondering
why I am defining the W instances using the Nth type family, then I don't have a satisfying answer
for you. Simply, I get type errors (in instances of Generic) if I instead define instances of W by
directly matching on the ps argument. In fact, I get the same type errors that I've discussed in the
original email in this thread. That's why I lead with just NLong out of context; my need for it is
kind of circular from the perspective of these emails.

If you are still interested in more technical details than this gist provides, you might as well
dive into the library.

  https://github.com/nfrisby/polyvariadic-generic-deriving/blob/master/examples/Examples.hs

I'm totally available by email. Thanks for your time.

NLong_demo

-- naturals
data Nat = Z | S Nat

-- indexes in the type list
type family Nth (n :: Nat) (ts :: [k]) :: k
type instance Nth Z     (a ': as) = a
type instance Nth (S n) (a ': as) = Nth n as

-- represents an uncurried application of t
data family W (t :: k) :: [*] -> *

-- this instance of W handles one argument, there's infinitely many instances... 
newtype instance W (t :: * -> *) ps = W1 (t (Nth Z ps))
asW1 f = (\(W1 x) -> x) . f . W1

-- the NLong class, which was (poorly) abstracted as NUnits in https://gist.github.com/3842579
class NLong (n :: Nat) (ts :: [*])
instance (ts ~ '[]) => NLong Z ts
instance (ts ~ (t ': tstail), NLong n tstail) => NLong (S n) ts

-- Rep/Generic are like generic-deriving, except for the kind polymorphism
type family Rep (t :: k) :: [*] -> *
class Generic (t :: k) where
  toRep :: NLong (CountArgs ('KindProxy :: KindProxy k)) ps => W   t ps -> Rep t ps
  frRep :: NLong (CountArgs ('KindProxy :: KindProxy k)) ps => Rep t ps -> W   t ps

-- CountArgs, and KindProxy are the same as from https://gist.github.com/3842579

{-

OK, with all that in place, the ghci query

*> :t atW1 $ \x -> frRep (toRep x) `asTypeOf` x

which reads as "at kind * -> *, convert to the representation and back", returns the type

   Generic (* -> *) t => t a -> t a   .

If the NLong constraints weren't on toRep and frRep, that same expression would have the inferred type

   Generic (* -> *) t => t (Nth * 'Z ps) -> t (Nth * 'Z ps)   ,

which ultimately leads to "ambiguous type variable ps0" in the user's code.

-}