[Agda] Surprising type error in implementing decreasing lists

[Nils Anders Danielsson]

On 2010-07-20 09:20, Nils Anders Danielsson wrote:
> Indeed this seems to be the case. For some reason Agda believes that
> _lt_ is "constructor-headed"

Ulf, this can be fixed by removing the line

   Axiom{} -> return (Just $ ConHead f)

from Agda.TypeChecking.Injectivity. This breaks some examples, in
particular, functions like the following one from the test suite are no
longer constructor-headed (because String is a postulate):

   El : EqU -> Set
   El nat        = Nat
   El bool       = Bool
   El string     = String
   El unit       = Unit
   El (fin n)    = Fin n
   El (list u)   = List (El u)
   El (pair u v) = El u × El v

I think we should go ahead and remove this line anyway, in line with
feature request 170, which states that we should treat postulates as
parameters (because they can be seen as place-holders for ordinary
definitions):

   http://code.google.com/p/agda/issues/detail?id=170

Do you agree? (I have prepared a patch.)

--
/NAD