More sensitive name freshening for PiBox types

[tsani]

Bound mvars from PiBox types are too eagerly renamed. For example, consider the type {S : |- step M M'} [ |- halts M' ] -> [|- halts M] and suppose we want to prove this in Harpoon. The variables S, M, and M' will be introduced and added to Delta. In the interactive prompt, suppose we forget the type of the theorem we're proving, so we run type halts_step. Harpoon produces this output:

- halts_step : {S1 : ( |- step M1 M'1)} [ |- halts M'1] -> [ |- halts M1]

Notice that all the variables now have a 1. This is because the type command synthesizes the type for an expression in the current context (so it works on partial applications, too, for instance). The printer for PiBox types checks whether the bound variable name occurs in Delta and freshens it (by incrementing a counter) until the variable name does not occur in Delta. This is a general solution to the problem of ensuring that the names are unique, but it is unnecessary in this case, since it just so happens that the type of halts_step is closed. In other words, it is only necessary to freshen a name if a conflict can occur.

More precisely, a conflict is when the offset of a variable doesn't match the offset obtained from a lookup of that variable name. For example, suppose we have cD = A : (|- foo) and we want to print the type tau = PiBox A : U. B [|- A@2]'. I write A@2 to mean "the variable named A but at de Bruijn index 2. So this A is referring to the variable that's in Delta. If we naively extend Delta when we go under the PiBox during printing, we get a new context cD' = A : (|- foo), A : U. When we wish to print [|- A@2], we have a conflict, because looking up A in the context gives offset 1, but the real offset of the variable to print is 2.

I'm not sure how one can implement this in such a way that avoids repeatedly analyzing the type to see what names it actually uses. It might be worthwhile to add a generic system of "annotations" to the internal syntax. Then one can traverse the expression once to do a "name analysis" and use this information during printing to avoid unnecessary freshening.