# Hindley-Milner system with let expansion

I'm reading these slides that present Hindley-Milner type inference. In the system HM, we have the following let rule:

$$\dfrac{\Gamma \vdash t:S \;\; \Gamma,x:S \vdash t':T }{\Gamma \vdash \text{let} \, x = t \, \text{in} \, t':T}$$

Here $$S$$ is a type scheme, i.e $$S ::= S | \forall a. S$$, which allows polymophism only on let expressions. Then, the following let rule is proposed for a system HM':

$$\dfrac{\Gamma \vdash t:T \;\; \Gamma \vdash [t|x]t':U }{\Gamma \vdash \text{let} \, x = t \, \text{in} \, t':U}$$

so all the occurrences of the binding are replaced and the result needs to be type checked. There is a theorem relating the two approaches:

$$\Gamma \vdash_{HM} t:S \iff \Gamma \vdash_{HM'} t: S$$

and as a consequence the following corollary is established:

Let $$t^*$$ be the result of expanding all let's in $$t$$ according to the rule. $$let \, x = t \, \text{in} \, t' \to [t|x]t'$$. Then, $$\Gamma \vdash_{HM} t:T \implies \Gamma \vdash_{F_1} t^*: T$$. Furthermore, if every let-bound name is used at least once, we also have the reverse $$\Gamma \vdash_{F_1} t^*: T \implies \Gamma \vdash_{HM} t:T$$.

Here $$F_1$$ is the simply-typed lambda-calculus.

I would like to gain some intuition on why this reverse direction holds. How does a let-bound name that is not used affect typing? Any reference is also appreciated.

• Presumably, in $F_1$ a $\lambda$-abstraction is not annotated with a type, i.e., it's written as $\lambda x . t$ (as opposed to $\lambda (x : T) . t$)? – Andrej Bauer Jan 6 at 16:40

$$t =\$$let x = (if 3 then 4 else false) in 5
then $$t^* =\$$ 5 which is well-typed in $$\mathrm{HM}$$, even though t is not. If every let-binding is used, though, then this pathology can't happen.