Typechecking anonymous parametrized module is much slower than expected #133

Note: I encounter this issue on non-cubical upstream v2.8.0, but am also filing an issue here as requested on IRC—

Type-checking certain parametrized module declarations is much slower than expected.

For instance, uncommenting the anonymous module in https://gist.github.com/jaycech3n/adb3268411cd1892d3023023445f4a44 increases typechecking time on my machine by about 30s.

Another, self-contained, example is https://gist.github.com/jaycech3n/62dac9d67fefb43ac51ecffcff864b16

Many thanks for the self-contained example. The issue is that the term traversal in DeadCode (specifically the traversal of metavariable types) is forcing (and visiting!) the quadratic piSorts in the types of the telescopes of the metavariables inserted for the arguments of _==_. Adding a generalizable variable forces enough metavariable instantiation to get rid of these time-bomb thunks.

For the curious I've attached a text file with what the telescope looks like before/after instantiation, but even that doesn't print the true scope of the problem (it is made worse by having to close over the meta types, which holds onto references to all of the previous metas).