[Agda] Challenge: can you exploit a known bug in Cubical Agda?

[Andreas Abel]

Tom Jack has found a bug in the implementation of transp for Glue (and 
hcomp for U) in Cubical Agda, where a system that should be

    [psi -> ..., forall i phi -> ...]

became

    [phi -> ..., forall i phi -> ...].

Details of the bug (and the fix) are at:

   https://github.com/agda/agda/pull/6197

Question: can one exploit this bug with reasonable resources?

In particular, we are using for a rather short test case that either
- makes Agda crash, or
- proves False.

Ideally, this test should run in reasonable time (less than a minute, 
say) using reasonable resources (not more than 4G memory), so we can add 
it to the regression test suite.

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www.cse.chalmers.se/~abela/