Benchmark regressions

[allanrenucci]

• "inductive implicits" significantly regressed in Use correct type equality in divergence check #6163
• "exhaustivity S" and "exhaustivity T" significantly regressed in Fix #4225: always do reachability check #4253

[milessabin]

The inductive implicits regression is on my TODO list.

[liufengyun]

The benchmark regression in #4253 is intended behavior, it's explained here #4253 (comment) .

[smarter]

Looks like all fixable regressions have been fixed.