<div dir="ltr">Hello all,<div><br></div><div>Let's say I have some data</div><div><br></div><div>    data Config = Conf (len :: Nat) (turboEncabulate :: Bool)</div><div><br></div><div>Using DataKinds, we can promote Config to a kind and Conf to a type.</div><div><br></div><div>However, it does not appear that GHC supports e.g.</div><div><br></div><div>    data Thing (conf :: Config) = Thing</div><div>    data Count (n :: Nat) = Count</div><div>    foo :: Thing conf -> Count (len conf)</div><div>    foo Thing = Count</div><div><br></div><div>That is, it does not appear to properly replace "len conf" with the value of len from conf.</div><div><br></div><div>Instead, the way I've found to do this is to define </div><div><br></div><div><div>    class Lengthed (a :: Config) where</div><div>        type Len a :: Nat</div><div>    instance Lengthed (Conf n) where<br></div><div>        type Len (Conf n t) = n</div></div><div><br></div><div>Now, </div><div><br></div><div>    foo :: Thing conf -> Count (Len conf)</div><div><br></div><div>works fine. So manually defining a type function that intuitively does the exact same thing as "len" seems to work.</div><div><br></div><div>Is there a particular reason behind this?</div><div><br></div><div>Thanks,</div><div>Will</div></div>