[Agda] again `with' vs `case'

[Sergei Meshveliani]

On Tue, 2013-08-27 at 13:31 +0200, Nils Anders Danielsson wrote:
> On 2013-08-26 20:35, Sergei Meshveliani wrote:
> > cong2-∈ {A = A} x (u ∷ xs) (v ∷ ys) (u=v ∷p =tail) x∈u-xs =
> 
> Note that the left-hand side above is rejected, even if you replace the
> right-hand side with a question mark.
> 

What does this mean "rejected" ?
If it was a type mismatch in the LHS, then it would be another message.
Does this mean and an un-accessible pattern?
How can this rejection be detected?

1) I replace the rhs with `?', and the report is again 
   "Missing cases:  cong2-∈ {_} {_} {_} _ ._ ._ ListPoint.[] _ "

2) Then I change this all to the two clauses
  
  cong2-∈ {A = A} x (u ∷ xs) (v ∷ ys) (u=v ∷p =tail) x∈u-xs =  _
  cong2-∈ {_}     _ _        _        _              _      =  _
,
and the checker reports of  unsolved metas  for the two RHS points.
If the LHS of the first clause was un-accessible, maybe, it must have
issued some more message (?)
  
And why the first LHS is not accessible?
(to my mind it is accessible). 


(A minor improvement to my initial letter:
for the "without-case" variant to type-check, it is needed to insert  
{A = A}  after  `(cong2-∈ ' in the last line
).

Thanks,

------
Sergei