[Ur] Two kind-related polymorphism questions

[Ziv Scully]

Hi all,

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.

(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 harder to infer than in, say, Haskell.

(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).

Thanks for any ideas!
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.impredicative.com/pipermail/ur/attachments/20160522/478df66f/attachment.html>