Hi all,<div><br></div>There are two things I've tried to do recently that I think aren't supported. I'm wondering primarily whether there are workarounds and secondarily whether they might be supportable in the future.<div><br></div><div>(1) Can datatypes take parameters of kinds other than `Type`? Lots of functor-y things come from allowing at least `Type -> Type` parameters, though I'm sure such parameters are<span></span> harder to infer than in, say, Haskell.</div><div><br></div>(2) Can classes be kind-polymorphic? I recently tried to make `equal :: K --> K -> K -> Type` a class. Everything compiled, but it wasn't treated as a class: instances weren't automatically generated, and the class argument had to be explicitly given with or without the @ sign. For now I'm fine with manually passing around proof terms, but having this and similar proof obligations as classes for some automation would be neat (though maybe not as important as (1) overall).<div><br></div><div>Thanks for any ideas!</div>