How does the undecidability of Extensional Martin-Löf Type Theory apply to real type-checking compilers? It is claimed in many sources (for example, here) that adding a rule like &quot;if Id(X,Y) then X really equals Y&quot; to a type theory is &quot;problematic&quot; because then its type-checking becomes undecidable. I have read Martin Hoffman's proof (&quot;Extensional concepts in intensional type theory&quot;, Section 3.2.2), as well as this SE question, but I still don't see how this creates a problem for a &quot;down-to-earth&quot; programming language.
I understand that deciding whether x:A has type B can get difficult, because there might exist a proof of Id(A,B). But the purpose of any &quot;normal&quot; type-checker is to verify, not to decide, so how is it problematic?
As I see it, nothing prevents the compiler from functioning like this: whenever the user tries to use a value of type X where a Y belongs, if the user has previously provided a proof that Id(X,Y), then we allow it, as if X and Y were syntactically identical. But if such a proof hasn't been provided, we treat it as an error, because the user &quot;hasn't made his case&quot;.
My question is: what difficulties, if any, can arise from treating identity types like that?
You can't expect to find a ready-to-use proof of Id(a,b) when you need one. For instance, you have proofs of Id(a,c) and Id(c,b), but not of Id(a,b). You would need some intelligence to find automatically new proofs of equality, and avoid always having to ask the user to do the job manually. But there is no perfect algorithm to implement such an intelligence: whatever you implement, it will always have limitations.
There are however solutions to this difficulty, see for instance the Andromeda project.