Fixing two problems in chapter Inference

[hafniz]

As discussed on Piazza, the descriptions for M⁺ ::= M⁻ ↓ A and M⁻ ::= M⁺ ↑ should read "switch from inherited/synthesized" instead of "switch to inherited/synthesized", respectively.

In the second paragraph under section "Soundness and completeness", the arrows in the code blocks should be the other way round (Γ ⊢ M ↑ A in the synthesized case and Γ ⊢ M ↓ A in the inherited case) to be consistent with the earlier definition.

-Haofei

[wenkokke]

@hafniz Could you copy the Piazza discussion here, for the sake of documentation?

[wadler]

Thank you!

[hafniz]

@hafniz Could you copy the Piazza discussion here, for the sake of documentation?

My post:

The type signature and the first paragraph state that synthesize returns the evidence that Γ ⊢ M ↑ A holds (or not), but the second paragraph says that it "[delivers] ... evidence that Γ ⊢ M ↓ A". Similarly the second paragraph says Γ ⊢ M ↑ A for inherit where its type signature has Γ ⊢ M ↓ A in it. This seems contradictory and I think the arrows in the second paragraph should be the other way round. 
Also, to me M⁻ ↓ A looks like switching from inherited to synthesized rather than switching to inherited, since M⁻ is already a term with inherited type. Similarly, it seems that M⁺ ↑ should be switching from synthesized. 

Malin Altenmuller's comment:

I think you're right in both cases. As in:
(1) the arrows should be the other way round in the second paragraph.
"In the synthesised case, it will either deliver a pair of a type A and evidence that Γ ⊢ M ↑ A, or a function that given such a pair produces evidence of a contradiction. In the inherited case, it will either deliver evidence that Γ ⊢ M ↓ A, or a function that given such evidence produces evidence of a contradiction. "
(2) the comment in the pseudo code should read "from":
M⁺ ::= M⁻ ↓ A switch from inherited (to synthesized)
M⁻ ::= M⁺ ↑ switch from synthesized (to inherited)
Feel free to create a pull request on the repo!