Preserve locations in type checking

[lukaszcz]

The locations are currently not preserved when substituting holes. The location of the hole should be preserved, but instead we preserve the location of the expression substituted into the hole. This can mess up location in error messaging and in the translation to Isabelle/HOL.

The PR

• Fix locations in Internal hole substitution (only for the case of substituting identifiers) #2995

provides a partial fix by adjusting the location of identifiers substituted into holes, but it doesn't adjust the locations of more complex expressions.