[Haskell-cafe] Promoting associated data types

[Kosyrev Serge]

Kosyrev Serge <_deepfire at feelingofgreen.ru> writes:
> So, two type classes for Categories and Layouts -- this gives rise to two indices,
> a total of four types.
>
> For indexing the Category type class I can use a regular promoted ADT:
>
>> data CatName
>>     = Graph
>>     | Dag
>>     | Set
>>     deriving (Eq)
>> 
>> class Category (a ∷ CatName) where
>>     data CatX a ∷ *
>
> ..which suddenly allows to do something I couldn't figure out how to do
> without XDataKinds -- a simple decision procedure over a list of existentials:
>
>> data CatEntry where
>>     CatEntry ∷ Category a ⇒ (a, (CatX a)) → CatEntry
>>
>> data CatAssoc where
>>     CatAssoc ∷ [CatEntry] → CatAssoc
>>
>> prefer ∷ Category c ⇒ c → CatEntry → CatX c → CatX c
>> prefer cat (CatAssoc xs) defx =
>>     case find (\(CatEntry (icat, _)) → cat == icat) xs of
>>       Just (CatEntry (icat, x)) → x
>>       Nothing                   → defx
>
> Basically, DataKinds allows constraining the type class index, so that its
> members become directly comparable.

Sadly, even this doesn't fly, because:

> The first argument of a tuple should have kind '*', but 'a' has kind 'CatName'.

..which doesn't really change even if I replace the tuple with a product type
within the CatEntry itself.

Basically GHC refuses to constrain the kind of constructor argument types
beyond the granularity provided by '*'.

And so I wonder if this is one restriction among those that you aim to remove.. : -)


-- 
respectfully,
Косырев Серёга