I've been reading "Towards Observational Type Theory". I'm new to type theory, so I have not been able to understand big chunks of the paper; hopefully as I read wider I'll understand more of it.

However, one rule which jumped out at me is this, on page 9, because it seems silly (apologies if my email client mangles this even after I've tried to fix it up - I've never tried pasting type rules from PDFs into it before): Γ |- S≡T Γ |- Q:S=T Γ |- s:S ------------------------------ T Γ |- s[Q>S ≡ s : T It seems silly to include a definitional equality as a premise, because I _thought_ the whole point of definitional equality was that S≡T means that S and T are freely co-substitutable, and type-checking will automatically substitute S for T or T for S _whenever_ required. (For example, it is often noted that Coq will automatically reduce (i.e. substitute) n+0 to n in a dependent type - but only if you write n+0 the "right" way round! I can't remember offhand which way round works.) So anyway, surely any derivation which needed that rule could also use this rule instead: Γ |- Q:S=S Γ |- s:S ------------------------------ S Γ |- s[Q>S ≡ s : S (which is trivial), substituting S for T before applying it, and substituting Ts for some of the Ss afterwards. Where have I gone wrong? -- Robin