# 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 "if Id(X,Y) then X really equals Y" to a type theory is "problematic" because then its type-checking becomes undecidable. I have read Martin Hoffman's proof ("Extensional concepts in intensional type theory", Section 3.2.2), as well as this SE question, but I still don't see how this creates a problem for a "down-to-earth" 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 "normal" 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 "hasn't made his case".

My question is: what difficulties, if any, can arise from treating identity types like that?

• How difficult could it be to do it manually? I'm envisioning it like this: the user writes a special statement equate e1;, where e1 : Id(a,c), and then all the cs in the current scope magically turn into as, including the one in the definition of e2 : Id(c,b). So now the user can write equate e2; to accomplish what he wanted. Oct 22, 2020 at 11:36
• @L.Garde Are you saying that a transition from Id(a,c) and Id(c,b) into Id(a,b) is not part of the proof? I think that it is, and so has to be written out somehow, whether manually or as part of some standard library. It's not "helping the type checker", it's a logical step like any other. Oct 23, 2020 at 21:15