I've been toying with some type-level programming ideas I just can't quite make work, and it seems what I really want is a certain kind of type unification. Basically, I'd like to introduce two new kind operators: kind Set as -- a finite set of ground type terms of kind as kind Range as = Range (Set as) (Set as) -- a greatest lower bound and a least upper bound A type expression of kind (Set as) would either be a type variable of kind (Set as), or set of *ground* type terms of kind (as). A type expression of kind (Range as) would be a type variable of kind (Range as), or two type expressions of kind (Set as). To unify ground terms of these types, one would compute as follows: unifySets xs ys | xs == ys = Just xs | otherwise = Nothing unifyRanges (Range glb0 lub0) (Range glb1 lub1) | glb' `subset` lub' = Just (Range glb' lub') | otherwise = Nothing where glb' = glb0 `union` glb1 lub' = lub0 `isect` lub1 I say sets of ground types, because I have no idea what unification between sets of non-ground types would mean, and I really don't need it. Among applications that came to mind, one could use this to create a restricted IO abstraction that could tell you which kinds of actions might be taken (read from mouse, talk to network, etc), and be able to run only those scripts that are restricted to certain resources. Or, one could define a singular GADT that represents messages/events decorated by various categories, and then define functions that only operate on selected categories of messages. E.G. for something vaguely IRC-ish, one could write something like: data EventCategory = Channel | Presence | Information | Conversation data Event :: Range EventCategory -> * where ChanCreate :: ... -> Event (Range (Set '[Channel]) a) ChanJoin :: ... -> Event (Range (Set '[Channel]) a) ChanLeave :: ... -> Event (Range (Set '[Channel]) a) PresAvailable :: ... -> Event (Range (Set '[Presence]) a) PresAway :: ... -> Event (Range (Set '[Presence]) a) WhoisQuery :: ... -> Event (Range (Set '[Information]) a) WhoisResponse :: ... -> Event (Range (Set '[Information]) a) Message :: ... -> Event (Range (Set '[Conversation]) a) And then be able to write functions such as dispatch :: Event (Range a (Set '[Channel, Conversation])) -> IO () dispatch e = case e of ChanCreate{..} -> ... ChanJoin{..} -> ... ChanLeave{..} -> ... Message{..} -> ... In this case, the case analysis tool would be able to warn me if I'm missing any possible events in this dispatcher, or if I have extraneous events that I can't be passed (according to my type.) Anyway, I've been trying to see if I can't come up with something similar using existing type-level functionality in 7.6, with little success. (Though I'm not very experienced with type-level programming.) If not, might it be possible to add some kind of extensible unification mechanism, in furtherance of type-level programming? Best, Leon