[Agda] question on `Any'

[Sergei Meshveliani]

On Tue, 2013-08-13 at 14:34 +0200, Dominique Devriese wrote:
> Sergei,
> 
> 2013/8/13 Sergei Meshveliani <mechvel at botik.ru>:
> > Please, why is not this type-checked
> > (for  A : Setoid c l;  C = Carrier A)
> > ?
> >   open Any
> >   f : (x : C) → (ys : List C) → Any (_≈_ x) ys → List C
> 
> Try changing the following line
> 
> >   f x _  (here _) = []
> 
> to use a dot pattern
> 
>   f x ._  (here _) = []
> 
> For more info, see the Agda tutorial by Norell and Chapman for
> example.  They mention the following rule:
>    The rule for when an argument should be dotted is: if there is a unique
>    type correct value for the argument it should be dotted.
> 
> In this case, the value of the underscore is fixed by the type of (here _).


Thank you.

There are certain questions.

1) ``should be dotted'' or ``must be dotted'' ?

2) > the value of the underscore is fixed by the type of (here _)

But it is not fixed.
If  x ≈ a, x ≈ b,  then the value for the first underscore in the line
can be, say,
             a :: [],   b :: a :: c :: [],  ...

The pattern   .(_ :: _) 

probably, tells  ``some non-empty list over C'', 
it looks sensible, and it is checked. 
But what does this mean here          `._'  
-- this is a question. 
The fact that it is type-checked looks strange.

Regards,

------
Sergei