[Agda] Surprising type error in implementing decreasing lists

[Nils Anders Danielsson]

On 2010-07-20 09:05, Conor McBride wrote:
> If I were a betting man, I'd bet Agda is making some attempt to
> guess which functions are injective, in order to invert them, and
> has somehow guessed wrongly about the nature of _lt_.

Indeed this seems to be the case. For some reason Agda believes that
_lt_ is "constructor-headed" (see
http://wiki.portal.chalmers.se/agda/agda.php?n=ReferenceManual.FindingTheValuesOfImplicitArguments).
When it sees the constraint ?₀ lt ?₁ = true it infers that ?₀ is zero
and ?₁ is suc ?₂.

--
/NAD