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

[Alan Jeffrey]

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.

A.

On 08/05/2011 09:12 AM, Andrés Sicard-Ramírez wrote:
> Hi,
>
> In the code below
>
> postulate
>    D   : Set
>    _∷_ : D → D → D
>
> data List : D → Set where
>    cons : ∀ x xs → List xs → List (x ∷ xs)
>
> tail : ∀ {x xs} → List (x ∷ xs) → List xs
> tail l = {!!}
>
> Try to split on l (using C-c C-c) I get the following error message:
>
> Cannot pattern match on constructor cons, since the inferred indices
> [x' ∷ xs'] cannot be unified with the expected indices [x ∷ xs] for
> some y, xs', x', xs, x when checking that the expression ? has type
> List .xs
>
> If I replace the postulates D and _∷_ by a data type, i.e.
>
> data D : Set where
>    _∷_ : D → D → D
>
> I got the expected pattern matching
>
> tail {x} {xs} (cons .x .xs xsL)
>
> Could someone explain me the different behavior?
>
> Thanks,
>
>