# How much type information do Hindley-Milner proof assistants need to remain sound?

A known benefit of the HM type system is that you can usually infer a term's most general type with no user-provided type annotations. For example, if my theory contains the standard axiom: $$\forall p, (p(T) \wedge p(F)) = \forall x, p(x)$$ HM can easily infer that $$p$$ has type Bool -> Bool and $$x$$ has type Bool.

But IIUC, theorems don't always prove the most general interpretation of a proposition. For example, say that I prove $$T = T$$ and $$F = F$$, and use these with the above axiom to prove $$\forall x, x = x$$

In this case, the proof assistant must explicitly keep track of the fact that $$x$$ had type Bool, right? Without this extra information, the type system would infer that $$x$$ could be any arbitrary $$\alpha$$, even though we've only proved the $$x :$$ Bool case. (I know that equality should probably be reflexive in every type, but one shouldn't be able to prove this for all types from just checking $$T$$ and $$F$$).

How do existing proof assistants combat this issue? How much "extra" type information do they need to track to avoid accidentally "over-generalizing"?* Is this a phenomenon which has been encountered/documented in existing proof assistants (whether they use HM or more complex dependent type systems)?

* I initially believed that you could resolve this issue by just tracking the types of all bound variables, but this doesn't seem to work: Suppose in our theory we define the predicate $$\mathrm{reflexive}(f) = \forall x, f(x, x)$$, then we can use the above theorem to prove $$\mathrm{reflexive}(=)$$. This proposition has no bound variables, but again we must somehow keep track of the fact that it has only been proven for equality over type Bool.

• It is unclear how you intend to use such a proof assistant (I take it you have in mind HOL-style proof assistants) to get from $T = T$ to $F = F$. I suggest that you either provide an actual example, or a more detailed description of what you have in mind, or choose a better example. The one you have is double unfortunate for being both true and blatantly polymorphic. Mar 24 '21 at 13:31
• To be precise, the murky part of your question is "and use these with the above axiom to prove". What exactly do you tell the proof assistant when you "use" $T = T$"? Mar 24 '21 at 13:32
• I'm not sure of the exact HOL-style syntax. But from $T = T$ and $F = F$ you can prove $(T = T) \wedge (F = F)$, which is beta equivalent to $(\lambda y, y = y)(T) \wedge (\lambda y, y = y)(F)$. Therefore you can apply the axiom to get $\forall x, (\lambda y, y = y)(x)$ which beta-reduces to the theorem. Mar 24 '21 at 13:45
• A better example of an theorem which is "obviously wrong when over-generalized" would be: $\forall f \forall x, f(x) = f(f(f(x)))$. The proof assistant must track that $x$ has type Bool to remain sound, even though $x$ could have a more general inferred type. Mar 24 '21 at 13:47
• I see. Well, there is no problem. As soon as you use your axiom, it will force $x$ in $\forall x, x = x$ to get type $\mathtt{bool}$. Mar 24 '21 at 15:23

Generally, HM type inference should be a part of the I/O interface, far away from the inference kernel. This constraint will drive your design to ensure that this won't be a problem. In your $$\mathrm{reflexive}$$ example, there are two polymorphic constants at play:
$$\mathrm{reflexive} : (\alpha \to \alpha \to \mathrm{bool}) \to \mathrm{bool}$$ $$(=) : \alpha \to \alpha \to \mathrm{bool}$$
In general, most HOL systems I'm aware of identify constants and variables by their (name, type) pair in the kernel. That is, $$x_{bool}$$ and $$x_{nat}$$ are different variables, but when they both occur in the same context, the parsing and printing logic are allowed to complain. This is a nice way to think about the logic...