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