Agda now reduces types before checking that they are data types
for the purpose of termination checking --without-K (see [Issue 1023]).