Your abstract says you prove uniqueness of typing. How do you prove that? IME to show this, you have to have the injectivity of judgmental equality at pi-types, and I've only ever been able to establish this via an argument involving logical relations. Is there some easier technique I've missed?

I am not sure I understand you. Are you saying that you expect $\prod_A B \equiv \prod_C D$ to imply $A \equiv C$ and $B \equiv D$? To be honest, I just started typing it up in Coq and then Coq wanted me to invent a more general induction hypothesis, and I did. The usual stuff. Let me put some comments into the relevant file and come back to you.

Oh, perhaps it's worth mentioning that the syntax is fully annotated. In particular, abstractions are written as $\lambda A . B . e$ and applications as $e_1 @^{A.B} e_2$, indicating both the domain and the codomain. Is that what worries you?

We're currently in the process of modifying syntax so that it becomes configurable. Then it should be clearer what assumptions precisely are needed for uniqueness.

Hi Andrej,

You have indeed understood what I meant.

If you try to prove that typing is unique up to judgmental equality for the usual syntax, you run into a problem in the application case. Induction tells you that ?AB??CD, but you can't conclude that A?C and B?D from that, which is what you need to get the proof to go through.

Adding annotations to applications and lambdas should fix this problem (and since you did it in Coq, it obviously does fix it). I didn't read your Coq development closely enough to realize that this is what you were doing, but your explanation makes things make sense to me now.

Injectivity of Pi-types usually requires a logical relation argument. See Abel/Scherer, LMCS 2012.