It is claimed in many sources (for example, here) that adding a rule like "if
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?