[Agda] pattern for All is not matched

[Sergei Meshveliani]

Please, why matching against  (x≤m ∷a xs≤m) 
is not type-checked below?

For the program 

-----------------------------------------------
open import Data.Nat  using (ℕ; _≤_)
open import Data.List using (List; _∷_)
open import Data.List.All as AllM using (All)
                                  renaming (_∷_ to _∷a_)

f :  (x m : ℕ) → (xs : List ℕ) → All (_≤ m) (x ∷ xs) → x ≤ m
f x m xs xxs≤m =  
               let  (x≤m ∷a xs≤m) = xxs≤m  in  x≤m
--------------------------------------------------

Agda 2.5.2 reports

  Expected record pattern
  when checking the let binding x≤m ∷a xs≤m = xxs≤m

In what place does it expect a record?
Is this a bug in Agda ?

The variant of 

    f x m xs (x≤m ∷a xs≤m) = x≤m

is type-checked.


In reality, I need to use the pattern like
   
  let (maximum′ m _ (x≤m ∷a xs≤m)) = maximum x xs         
  in
  foo m x≤m xs≤m,

where maximum′ is the constructor for the result record for the
`maximum' function.
Matching against
                (maximum′ m _ _)  
 
is type-checked under this `let', while matching against  
(maximum′ m _ (x≤m ∷a xs≤m))  
is not
(again, "Expected record pattern").

Thanks,

------
Sergei