[Haskell-cafe] How to build an "Indicator Type" for a type class?

[Steffen Schuldenzucker]

Dear Cafe,

let:

> data True
> data False
>
> class C a

(arbitrary instances for C may follow)

Now, how to obtain an "Indicator Type" for C, i.e. a type IndC that is defined
via a type family / fundep / ... , so that

IndC a = True 	forall a which are instances of C
IndC a = False 	for all other a.

I've collected some failed approaches here[1]. My key problem is that if I
define (in the 3rd try):

> instance (C a) => IndC3 a True

, it does *not* mean "Define this instance for all a which are an instance of
C", but "Define the instance IndC3 a True for all types a, but it's not gonna
work if a is not an instance of C".

Does anyone have another idea?

Background:

After having implemented type-level lists[2] and a quicksort on them[3], I'd
like to have type-level sets. In their most simple implementation, sets are
just (unsorted) lists like this:

> data Nil
> data Cons a b
> class Elem x l
(instances for Elem so that Elem x l iff x is an element of the list l)

Now I want:

> type family Insert x s :: *

Insert x s = s 		forall (x, s) with (Elem x s)
Insert x s = Cons x s 	for all other (x, s).


Thanks a lot!

Steffen


[1] http://hpaste.org/fastcgi/hpaste.fcgi/view?id=25832#a25832
[2] Kiselyov, Peyton-Jones, Shan: "Fun with type functions"

http://research.microsoft.com/en-us/um/people/simonpj/papers/assoc-types/fun-with-type-funs/typefun.pdf
[3] I rewrote this algorithm using type families instead of fundeps:

http://www.haskell.org/haskellwiki/Type_arithmetic#An_Advanced_Example_:_Type-Level_Quicksort