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!
_______________________________________________
Ur mailing list
[email protected]
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
