Kosyrev Serge <_deepfire@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, Косырев Серёга