Dear Agda developers, I have a function defined by several patterns, and it is type-checked. But the first pattern is a special case of the second one. And after its removal the program remains type-checked. Is Agda (Development, January 1, 2019) supposed to report about such overlaps? Thanks, ------ Sergei