Let's say I have some data

    data Config = Conf (len :: Nat) (turboEncabulate :: Bool)

Using DataKinds, we can promote Config to a kind and Conf to a type.

However, it does not appear that GHC supports e.g.

    data Thing (conf :: Config) = Thing

    data Count (n :: Nat) = Count

    foo :: Thing conf -> Count (len conf)

    foo Thing = Count

That is, it does not appear to properly replace "len conf" with the value of len from conf.

Instead, the way I've found to do this is to define 

Now, 

    foo :: Thing conf -> Count (Len conf)

works fine. So manually defining a type function that intuitively does the exact same thing as "len" seems to work.

Is there a particular reason behind this?

Thanks,

Will