Type Families and enhanced constraints (at run-time)

[Matthew Brecknell]

> > insert :: Char -> Set t Char -> Set t Char
> > insert c (Set tinfo cs) = case c of
> >                             'A' -> Set (InsA tinfo) (c:cs)
> >                             _   -> error "not a label"
> 
> gives me the error:
> >    Occurs check: cannot construct the infinite type: t = A t
> >     When generalising the type(s) for `insert'
> > Failed, modules loaded: none.

To do what you are trying to do, it seems that you would also need to be
able to write a function whose return type depended on a simple
parameter value:

foo :: Char -> ???

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.