[Haskell-cafe] Type level sets with GADTs, fundeps etc

[J.Burton at brighton.ac.uk]

I have a problem with applying a type constraint in the 
constructor of a GADT...I wrote some type level code for sets 
using empty types and fundeps, along the lines of Conrad Parker's 
Instant Insanity and Oleg's Lightweight Static Resources. At this 
level things works OK so I have empty types A, B ... Nil with an 
infix cons (:::) and fundeps determining constraints like Member, 
Disjoint etc. (Links to code at the end of message.) Then I can 
evaluate:

> :t insert (undefined::A) (undefined:: A ::: Nil)
insert (undefined::A) (undefined:: A ::: Nil) :: A ::: Nil 

But what I really want to do is wrap this up so that it can be used 
at runtime, not just in the type-checker, so that (just a sketch) 
I could have

insert 'A' empty :: Set (A ::: Nil)

where the runtime value of the set is fully determined by its type. 
I got some help with this and existential boxing seems to be the 
answer. I got a version that uses this strategy working OK until it
comes to applying constraints (e.g. Member, needed when inserting an
element). My problem is below. Here's one with no constraints that 
will type-check:

----------------------
{-box for labels -}
data LBox = forall a. LBox (L a) 
{-box for sets of labels-}
data LSetBox = forall t. LSetBox (LSet t)
{-sets of labels -}
data LSet t where
    Nil :: LSet Nil
    -- 'dumb' insertion
    Ins :: L a -> LSet t -> LSet (a ::: t)
insert = Ins

empty :: LSetBox
empty = LSetBox Nil
 
{-take a Char into a boxed LSet-} 
insertChar :: Char -> LSetBox -> LSetBox
insertChar c (LSetBox s) = 
    case fromChar c of
      LBox t -> LSetBox (insert t s)
  
{-populate a box-}
fromChar :: Char -> LBox
fromChar 'A' = LBox AL
{- ... B, etc -- use Template Haskell to generate alphabet and the 
   various instances needed? -}
fromChar _   = error "fromChar: bad Char"
------------------------

With some Show instances then I can evaluate

> insertChar 'A' empty
LSet {A,}

But what about constraints on the Ins constructor, e.g. on insertion,
ignore elements that are already there:

---------------------
data LSet t where
    Nil :: LSet Nil
    --either add the new element or do nothing
    Ins :: (Member a t b
          , If b (LSet t) (LSet (a ::: t)) r) 
          => L a -> LSet t -> r
insert = Ins

[...]

class Member x ys b | x ys -> b
    where member :: x -> ys -> b

instance Member x Nil F 
instance (Eq x y b', Member x ys m, If b' T m b) => 
    Member x (y:::ys) b

class If p x y z | p x y -> z
    where if' :: p -> x -> y -> z
instance If T x y x 
instance If F x y y 

---------------------

But this evidently isn't the way to use fundeps -- here's
the error:

Malformed constructor result type: r
    In the result type of a data constructor: r
    In the data type declaration for `LSet'
Failed, modules loaded: none.

(The other place I tried putting the constraints is in the type
of `insert' rather than the Ins constructor...)

How can I express this constraint? BTW, I would rather be using type 
families for this, for forward compatibility and their greater
generality, so if I can also get round this with them I'd love to 
know how...

Thanks, and sorry for the long post!

Jim

[1] Purely type level version: http://jim.sdf-eu.org/TypeLevelSets2.hs
[2] Interactive version using GADTs/Existential boxing: http://jim.sdf-eu.org/Set-July08.hs