Add Evidence parameter to identity reduce operations

[johnynek]

This makes use of our Leibniz-like type EqTypes to remove several casts. This equips operations that are doing identity reduces to prove to scalac that the input value type is the same as the output.

The main value here is just to remove casts in current and future optimization code. Each cast is a danger, even when correct, because it

1. makes is more tolerant of casts which in other cases may be unsafe
2. may incorrectly become unsafe due to code change, but not detected by the compiler during refactoring.

[johnynek]

@non @erik-stripe can you take a look at this one?

I think you are very familiar with these Leibniz tricks.

[non]

LGTM 👍 (love that Leibniz!)