[Agda] Re: Agda's unification: postulates versus data types

[Stefan Monnier]

> For tail to typecheck, you need ∷ to be invertable, since the unification
> engine can generate the constraint x ∷ xs = y ∷ ys, from which it needs to
> deduce x = y and xs = ys. Datatype constructors are invertable, but
> functions in general, including postulates, aren't.

> It would be nice if there was a way to prove to Agda that a function is
> invertable, in this case you could then add a couple of postulates stating
> invertability of ∷, but as far as I know this isn't doable.

Actually, as long as it's only used for type-inference and not for
type-checking, we could let users "postulate" that a particular function
is injective and then let the unification use it during type inference.


        Stefan