Hi Will, On 09/01/16 23:23, William Yager wrote:

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

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.

Indeed, this is not yet supported. GHC doesn't currently have any form of promotion for functions (as opposed to datatypes), including record selectors. Thus when `len` is used in a type, it always refers to a type variable, not a function. You might be interested in the singletons package [1], which automatically generates promoted functions using Template Haskell. A full treatment of function promotion is an open research problem, because it requires reconciling the non-trivial differences between term-level functions and type families (which aren't really functions at all). In the meantime, your only options are separately defining type families corresponding to functions, either manually or via TH.

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

class Lengthed (a :: Config) where type Len a :: Nat instance Lengthed (Conf n) where type Len (Conf n t) = n

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.

Do note that the class isn't really necessary here: you could simply define type family Len (c :: Config) :: Nat where Len (Conf n t) = n Best regards, Adam [1] http://hackage.haskell.org/package/singletons -- Adam Gundry, Haskell Consultant Well-Typed LLP, http://www.well-typed.com/