Type Families and enhanced constraints (at run-time)

[Jim Burton]

On Sat, 2007-12-01 at 11:33 +1000, Matthew Brecknell wrote:
[...]
> Seems impossible. With GADTs, you can of course go the other way:
> 
> > data A
> > data B
> > 
> > data Chr a where
> >   AChr :: Chr A
> >   BChr :: Chr B
> > 
> > toChar :: Chr a -> Char
> > toChar AChr = 'A'
> > toChar BChr = 'B'
> 
> So perhaps insert should have a type something more like:
> 
> > type family ChrSetIns a t :: *
> >
> > insert :: Chr a -> ChrSet t -> ChrSet (ChrSetIns a t)
> 
> I'm not sure how to make the set type parametric in the element type,
> though.
> 

Thanks -- I think I see your point but I'm not sure how to make 
use of it...(perhaps I'm trying to run before I can walk). 
The way I was picturing things, the A, B ... types would 
need to take a parameter so they can be collected/consed, 
so my next attempt tries to incorporate both ideas:

data A
data B 
data Nil
data t ::: ts -- consing the phantom types

data Chr a where
    AChr :: Chr A
    BChr :: Chr B

toChar :: Chr a -> Char
toChar AChr = 'A'
toChar BChr = 'B'

data TInfo t where
    Nil  :: TInfo Nil
    InsA :: TInfo t -> TInfo (A ::: t)
    InsB :: TInfo t -> TInfo (B ::: t)

data ChrSet t = ChrSet (TInfo t) [Char]

type family ChrSetIns c s :: * 
type instance ChrSetIns (Chr a) (TInfo t) = TInfo (a ::: t)

insert :: Chr a -> ChrSet t -> ChrSet (ChrSetIns a t)
insert c (ChrSet tinfo cs) = case c of
                            AChr -> ChrSet (InsA tinfo) ((toChar c):cs)
                            _   -> error "not a label"

`insert' is still the problem -- how to form the 1st param 
of ChrSet. (InsA tinfo) isn't an instance of ChrSetIns, but 
I don't see how to fix that...? The error:
-------------------------------------------
Couldn't match expected type `ChrSetIns A t'
	   against inferred type `A ::: t'
      Expected type: TInfo (ChrSetIns A t)
      Inferred type: TInfo (A ::: t)
    In the first argument of `ChrSet', namely `(InsA tinfo)'
    In the expression: ChrSet (InsA tinfo) ((toChar c) : cs)
Failed, modules loaded: none.

Thanks,

Jim