InferRecordTypes-1.agda:5,7-17
There are no records in scope
when checking that the expression record { } has type _1