[Agda] Non-termination change in Agda 2.3.3

[Mateusz Kowalczyk]

Hi,

I'm running Agda 2.3.3, built yesterday. While trying to help someone in
#agda, one of their functions was highlighted in salmon to indicate
non-termination. We have stripped down the example to [1]. As you can
see at [2], my emacs highlights filterN as potentially non-terminating
but 2 people in #agda with Agda 2.3.2.2 report that the code is all
fine. See a session screenshot from one of them at [3].

Is this a regression or an improvement? What changed? Did older Agda
admit a function it shouldn't have been or is this just a bug in newer Agda?

Thanks

[1]: http://lpaste.net/101716
[2]: http://fuuzetsu.co.uk/images/1395779363.png
[3]: http://i.imgur.com/2Iy1Gkx.png
-- 
Mateusz K.