Port to Agda 2.4.0

Fix the only typechecking error with Agda 2.4.0. I did not retest all the code inside `spec` environments though.