would support for kind equalities enable the following example?

[Carter Schonwald]

Hey all,

I've a use case in my code where It looks like it might be an example of
something that won't compile until we have type level GADTs

I'm essentially writing a vector api that
allows certain args to be mutable, pure or "dont care". (dont care = that
they're treated as being immutable). I'm using GADTs to model this. (using
GADTs rather than type classes partly because I want to make sure type
inference works out nicely, and partly to see how far i can go while not
adding any new type classes)

data Eff :: * -> * where
    Pure :: Eff ()
    Mut :: s -> Eff s

data EVector  :: * -> * -> * where
    PureVector :: S.Vector el  -> EVector Pure el
    MutVector :: SM.MVector s el -> EVector (Mut s) el

the above doesn't work because DataKinds only works at kind * currently,
however i can defunctionalize it to the following (while making it a tad
less pretty)
and it then works

data Eff = Pure | Mut

data EVector  :: Eff -> * -> * -> * where
    PureVector :: S.Vector el  -> EVector Pure () el
    MutVector :: SM.MVector s el -> EVector Mut s  el


am i correct in thinking that the first example *should* be possible once
we have fancier kind machinery (kind equalities and type level GADTs?)? I
suspect I'll be hitting *A LOT* more examples like the above, and if theres
any ways I can help push this along on the research or engineering side, I
please tell me :)

thanks!
-Carter
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20140224/72ea4d16/attachment.html>