Comment by chii

> exist in your head if you're implementing a function like max(a, b)

surely, you have an idea of what you're using that function for, while you're writing it.

The compiler is doing a check to see if the function makes some minimal logical sense (ala, a typecheck), but it cannot read your mind. But this implies the types are actually an actualization of the thoughts in your head, in a formal manner.