Feature Request: Allow `i:` and `o:` on `func` and `->`

[Janno]

It would be great if all the following declarations were valid.

pred f i:(A -> B -> C -> prop). /* the HO argument defaults to `pred o:A, o:B, o:C`  */
pred f i:(i:A -> i:B -> o:C -> prop).
pred f i:(func A, B -> C).
pred f i:(func i:A, i:B -> o:C).
/* .. and the same with `func f` instead */

The following should not typecheck (or perhaps not be valid syntax), of course:

pred f:(func i:A, o:B -> o:C). (* functional inputs must be `i:` *)
pred f:(func i:A, i:B -> i:C). (* functional outputs must be `o:` *)

I am porting a lot of elpi 2 code that contains (1) coq-elpi derive passes declared with pred and (2) higher-order predicates that are declared exclusively using pred hofun i:(A -> B -> prop) ... -> prop whose arguments now default to pred o:A, o:B but usually need at least one o: to be an :i. As a result, I am rewriting a whole lot of declarations and it is becoming a bit tedious, especially when I go back and forth between pred and func and have to remove/add i: and o:. It would be nice if all I had to do was to change func to pred. For higher-order predicates, not having to switch from -> notation to pred would also reduce the amount of churn.