The important context in the intro is, "The type checker needs to be able to determine that x and y have the same type, and reject the code if not. This is what we mean by computing canonical types."

There's a summary at the end titled, "what does this mean?" which says that undecidability doesn't bite in practice with real-world code, but the type system features discussed in the post have been the cause of bugs: "We are also aware of examples where we don't manage to canonicalize types properly, causing miscompiles and crashes. We've been fixing these gradually over time, but we continue to discover more problems as we fix them. This was a strong hint that the underlying approach was not correct, which is why I spent some time thinking about the fundamentals of this problem. Indeed, we can now see that the reason we have struggled with correctness in this area of the language is that a solution is impossible in the general case."

So the question arising from this undecidability is how to fix it: "What we need to do is come up with an appropriate restriction to the combination of SE-0142 and SE-0157. [...] I'm optimistic that introducing this restriction should have very little impact on real-world code."