Better type error reporting

[marcoeilers]

Addressing issue #642 (at least in most cases).

For the example in #642, Viper now reports

Silicon found 2 errors in 1.16s:
  [0] Type error in the expression at test.vpr@6.10. Expected Int but got Foo. (test.vpr@6.10--6.29)
  [1] Type error in the expression at test.vpr@6.33. Expected Int but got Foo. (test.vpr@6.33--6.52)

Additionally, in some cases, Viper used to mention internal type variables in error messages, e.g. Expected type Ref, but found #R#1451 at the expression at test.vpr@15.8 (test.vpr@15.8--15.11). This PR fixes that to be Expected type Ref, but found Foo[Bool, Perm] at the expression at test.vpr@17.6 (test.vpr@17.6--17.17) instead.

[fpoli]

Someone should probably run an auto formatter on these files at some point; spaces around symbols are not used uniformly.

[fpoli]

For the example in #642, Viper now reports

Silicon found 2 errors in 1.16s:
  [0] Type error in the expression at test.vpr@6.10. Expected Int but got Foo. (test.vpr@6.10--6.29)
  [1] Type error in the expression at test.vpr@6.33. Expected Int but got Foo. (test.vpr@6.33--6.52)

That means that the position of the errors is now

Position: assert new_foo(new_foo(1)) == new_foo(new_foo(1))
                 ^^^^^^^^^^^^^^^^^^^    ^^^^^^^^^^^^^^^^^^^

I find it unusual and perhaps a bit confusing that the errors are precise about the types but not about the positions. The actual expressions that have type Foo but should be Int are

Position: assert new_foo(new_foo(1)) == new_foo(new_foo(1))
                         ^^^^^^^^^^             ^^^^^^^^^^

With the imprecise error positions, I would prefer an error message saying "Type error in a subexpression of ..." to remember that I should check all the arguments myself.

[marcoeilers]

For the example in #642, Viper now reports

Silicon found 2 errors in 1.16s:
  [0] Type error in the expression at test.vpr@6.10. Expected Int but got Foo. (test.vpr@6.10--6.29)
  [1] Type error in the expression at test.vpr@6.33. Expected Int but got Foo. (test.vpr@6.33--6.52)

That means that the position of the errors is now

Position: assert new_foo(new_foo(1)) == new_foo(new_foo(1))
                 ^^^^^^^^^^^^^^^^^^^    ^^^^^^^^^^^^^^^^^^^

I find it unusual and perhaps a bit confusing that the errors are precise about the types but not about the positions. The actual expressions that have type Foo but should be Int are

Position: assert new_foo(new_foo(1)) == new_foo(new_foo(1))
                         ^^^^^^^^^^             ^^^^^^^^^^

With the imprecise error positions, I would prefer an error message saying "Type error in a subexpression of ..." to remember that I should check all the arguments myself.

Positions are also fixed now. New output:

Silicon found 2 errors in 1.18s:
  [0] Type error in the expression at test.vpr@6.18. Expected type Int but found Foo. (test.vpr@6.18--6.28)
  [1] Type error in the expression at test.vpr@6.41. Expected type Int but found Foo. (test.vpr@6.41--6.51)