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