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

[Andrés Sicard-Ramírez]

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,


-- 
Andrés