Sergei, you seem to compute with records a lot, so I wonder: what will happen if you try to type check your development with the --no-eta-equality flag enabled? Or at least some part of it, if you actually use eta-rules somewhere. https://github.com/agda/agda/blob/14b9fbb11264a136f6b1e92373ee4a9149d006e4/CHANGELOG#L299