[Agda] Surprising type error in implementing decreasing lists

Nils Anders Danielsson nad at Cs.Nott.AC.UK
Tue Jul 20 12:17:57 CEST 2010


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



More information about the Agda mailing list