Skip to content

Draft: directed coercions

Adam Gundry requested to merge wip/amg/dcoercion into master

Work in progress. More to come soon [May 2023].

This MR introduces a slimmer version of coercions, directed coercions, which store fewer types within them. This more compact representation considerably speeds up programs which involve many type family reductions, as the coercion size no longer grows quadratically in the number of reduction steps.

Edited by sheaf

Merge request reports