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.