[Ur] Two kind-related polymorphism questions

[Adam Chlipala]

Unfortunately, neither of those patterns are supported at the moment.  
I'd be glad to accept patches adding them, though.

On 05/22/2016 04:37 AM, Ziv Scully wrote:
> 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!