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