Carefully implement coercion zapping

Tickets: #8095 #27336 #27518

This MR vastly improves the compilation speed of type-family-heavy programs by zapping chains of type family reductions in the rewriter. See the commit message for more details.

TODO:

  • Benchmark results.
  • Compile singletons-base.
  • Compile chesskell.
  • Assess the impact of (ZapDepsRecording). (Seems it has basically no impact?)
  • Do we want to disable coercion zapping when building base and other core libraries? Answer: "no" as zapping does not imperil soundness.
  • Investigate the impact of the changes to smart constructors and in particular mkInstCo (and whether we want to propagate a zapped argument coercion).
  • Clean up the commit history.
Edited by sheaf

Merge request reports

Loading