Making higher-dimensional boundary arguments implicit

[mikeshulman]

In my own experience so far coding in Narya, it seems that one of the more annoying things is having to give all the lower-dimensional arguments of a higher-dimensional application explicitly. For instance, if f2 : Id (A -> B) f0 f1, then given a0 a1 : A and a2 : Id A a0 a1, we have to write f2 a0 a1 a2 rather than just f2 a2. Of course in this simple case that's not so bad, but if a0 and a1 are long expressions, and when the function being applied is 2- or even 3-dimensional, it becomes quite tedious and verbose.

It also seems that in most cases, these lower-dimensional arguments are redundant: if the top-dimensional argument a2 is synthesizing, then its boundary must consist of the lower-dimensional arguments. One day we'll have full unification and implicit arguments, but this particular instance could probably be implemented now: when applying a higher-dimensional function, we choose whether to specify all the arguments or just the top-dimensional one, and in the latter case it must synthesize a type from which we recover the other arguments.

What should the syntax for this be? I'm tempted to say that the implicit case is the default, so that you can just write f2 a2 in the above case as long as a2 synthesizes, and if you want the explicit version you write something like f2 {a0} {a1} a2 which will presumably be the syntax for supplying general implicit arguments explicitly once we have those. (In this case there would be no halfway-point; you either give all the lower-dimensional arguments explicitly or none of them.) That would be a very breaking change, requiring changes to all existing Narya code. But hopefully the changes would be in the direction of simplifying it: just remove a bunch of arguments, and maybe in some cases add curly braces to some of them. So people who've been coding in Narya, like @FrozenWinters and @TOTBWF, what do you think?

If people want it, I could add a command-line flag that would restore the old behavior, at least for a while, so that old code wouldn't have to be updated immediately.

A related question is whether to apply the same principle to instantiations of higher-dimensional types. In the 1-dimensional case like Id A a0 a1 we can't omit anything, but in the 2-dimensional case Id (Id A) a00 a01 a02 a10 a11 a12 a20 a21 we could omit all but the highest dimensional faces to get Id (Id A) a02 a12 a20 a21, synthesizing the rest of the boundary from the types of these faces. I think this is probably also a good idea but I'm less sure.

One thing we would probably want to add along with this is an option to display the implicit arguments or not when printing, since sometimes it is useful to see the whole boundary of a type you're trying to inhabit. What else am I not thinking of?