[Agda] list equality decision procedure fails termination check with Agda 2.4.0.1?

[Brent Yorgey]

Hi everyone,

I have been using Nils' "equality" repo, here:

  http://www.cse.chalmers.se/~nad/repos/equality

I just upgraded to Agda 2.4.0.1 and now compiling the library generates the error

  Termination checking failed for the following functions:
    Decision-procedures.List.Dec._≟_
  Problematic calls:
    ((x ∷ xs) ≟ (y ∷ ys)) (x ≟A₁ y)
      (at /home/brent/src/equality/Equality/Decision-procedures.agda:238,14-15)
  when scope checking the declaration
    import Equality.Decision-procedures as .#Equality.Decision-procedures-131098778

The code in question can be found here:

  http://www.cse.chalmers.se/~nad/listings/equality/Equality.Decision-procedures.html#6997

under the comment "List preserves decidability of equality".

It seems to me intuitively that this code should pose no problem for
the termination checker.  Is this a bug?  Or can someone suggest a way
to rewrite the code so it will pass the termination checker?  I've
read some other discussion of changes to the termination checker but
can't figure out whether this is related.

Thanks!

-Brent