Type check example expressions.
Multiple possible types and example of type schema.
Consider lambda with variable capture, with naive substitution. Example of evaluation. What scoping policy is this? Show that type checking soundness fails.
formally capture-avoiding and capture non-avoiding substitution, and showing that subject reduction property for type systems fails to hold if you do not have capture avoiding substitution.
I guess one example (in two lines) is:
(%b:int. (%x:int.(%b:bool. if b then x else 5)) b)) 2
and then you start by reducing the inner application (%x…)b .