It finally occurred to me how to get most of what I want,  at least from a functional perspective.    Here&#39;s a sample GADT,  with four categories of constructor:<div><br></div><div><div>data Foo :: Bool -&gt; Bool -&gt; Bool -&gt; Bool -&gt; * where</div>
<div>    A :: Foo True b c d</div><div>    B :: Foo True b c d</div><div>    C :: Foo a True c d</div><div>    D :: Foo a b True d</div><div>    E :: Foo a b c True</div></div><div><br></div><div>Given an Eq instance,  we can easily compare two constructors for equality;   we can put some constructors in a list and tell which categories appear in the list,   and it plays reasonably nicely with the case coverage analyzer,  which I think is important from a software engineering standpoint.    For example,  this function will compile without warning:</div>
<div><br></div><div>fooVal :: Foo a b False False -&gt; Int</div><div>fooVal  x = </div><div>   case x of</div><div>      A -&gt; 0</div><div>      B -&gt; 1</div><div>      C -&gt; 2</div><div><br></div><div><div>The only thing this doesn&#39;t do that I wish it did is infer the type of fooVal above.    Rather,  GHC  infers the type  :: Foo a b c d -&gt; Int,   and then warns me that I&#39;m missing cases.   But this is admittedly a strange form of type inference,   completely alien to the Haskell landscape,   which I realized only shortly after sending my original email.   My original description of ranges of sets of types wasn&#39;t sufficient to fully capture my intention.   </div>
<div><br></div><div>That said,  this solution falls rather flat in several software engineering respects.  It doesn&#39;t scale with complexity;   types quickly become overbearing even with modest numbers of categories.    If you want to add additional categories,   you have to modify every type constructor instance you&#39;ve ever written down.    You could mitigate some of this via the existing type-level machinery,  but it seems a band-aid,  not a solution.  </div>
<div><br></div><div>For comparison,  here is the best I had when I wrote my original email:</div><div><br></div><div><div>data Category = W | X | Y | Z</div><div><br></div><div>data Foo :: [Category] -&gt; * where</div><div>
    A :: (Member W ub) =&gt; Foo ub</div><div>    B :: (Member W ub) =&gt; Foo ub</div><div>    C :: (Member X ub) =&gt; Foo ub</div><div>    D :: (Member Y ub) =&gt; Foo ub</div><div>    E :: (Member Z ub) =&gt; Foo ub</div>
</div><div><br></div><div><div>class Member (a :: x) (bs :: [x])</div><div>instance Member a (a &#39;: bs)</div><div>instance Member a bs =&gt; Member a (b &#39;: bs)</div></div><div><br></div><div>The code is closer to what I want,  in terms of expression,  though it mostly fails on the functional requirements.    Case analysis doesn&#39;t work,   I can&#39;t compare two constructors without additional type annotations,   and while I can find out which categories of constructors appear in a list,   it doesn&#39;t seem I can actually turn those contexts into many useful things,  automatically.   <br>
<br>So while I didn&#39;t have any trouble computing set operations over unordered lists at the type level,   I couldn&#39;t figure out out to put it to use in the way I wanted.    Perhaps there is a clever way to emulate unification,  but I really like the new features that reduce the need to be clever when it comes to type-level computation.</div>
<div><br></div><div>Best,</div><div>Leon</div></div>