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

[Brent Yorgey]

On Thu, Jun 19, 2014 at 03:50:16PM -0500, Andrés Sicard-Ramírez wrote:
> On 19 June 2014 11:24, Brent Yorgey <byorgey at seas.upenn.edu> wrote:
> 
> > I just upgraded to Agda 2.4.0.1 and now compiling the library generates
> > the error
> >
> >
> Please note that Agda 2.4.0.1 is an unreleased version (but I know it
> is in Hackage).

I don't understand.  What does it mean for Agda 2.4.0.1 to be
"unreleased" if it is on Hackage?

> >    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
> >
> 
> It is due to a change on the behaviour of the termination-checker when
> using the --without-K option (by removing this option, the function is
> accepted).

Can you be more precise?  I understand that the behavior of the
termination-checker changed; but is the code I linked now expected to
fail termination checking?

-Brent