Typo in the calculus of constructions paper? In the classic the calculus of constructions paper there is a rule that states


(page 7 of the pdf, page 101 of the original document)

This rule would mean that any context is reducible to a member of that context.  This seems like it shouldn't be correct, as it would entail

1 ≅ Nat
3 ≅ Nat
1 ≅ 3


if Nat is a context.

I think the best interpretation is that the lower delta was meant to be an M.  Especially considering the rules given on the next page.

So is this simply a typo, or some subtle logical rule that I don't understand?
You are correct, there is an error in that paper, and the rule should indeed read:
$$\frac{\Gamma\vdash M:\Delta}{\Gamma\vdash M\cong M} $$

the use of jugements of this style for equality (sometimes called "typed equality") originates already in Martin-Löf, I think (see here for example). It's often replaced with an untyped operational definition in modern treatments, where there is no jugement of the form $\Gamma\vdash N\cong M$, and conversion is defined on raw terms.

Somewhat counter-intuitively, proving that the system with typed conversion is equivalent to the one without types is very difficult, and was settled in 2010 by Siles and Herbelin.