Hindley-Milner system with let expansion

Question

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.

Answer 1

I think something somewhat trivial is happening here, that is if the let binding is not used, then you can let bind an ill-typed term, e.g. if:

$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.