[Agda] strange let-in-case-let

[Sergei Meshveliani]

People, 
I have further problems with matching in let+case+let.
Consider the following two fragments.

open OfMax natDTO using (Maximum; maximum′; maximum ...)
open Maximum using (max; all≤max)           
                   -- Maximum is a record with constructor maximum′
...
--------------------------------------------------------- (I) ---
 ; (tri≈ _ e≡e' _) →
       let 
         es       = map proj₂ mons                              
         maxStruc = maximum e (e' ∷ es)   -- : Maximum (e ∷ e' ∷ es)
         m        = max     maxStruc       
         ee'es≤m  = all≤max maxStruc    
         e'es≡ees = PE.sym $ PE.cong (_∷ es) e≡e'
         ord-ees  = PE.subst DecrOrderedList e'es≡ees ord-e'es
                                                                                
         ees≤m : All (_≤ m) (e ∷ es)  
         ees≤m = DPrelude.anything 
       in 
       ((pol′ ((a + b , e) ∷ mons) ord-ees) , ees≤m)
------------------------------------------------------------------

----------------------------------------------------------- (II) ---
...  
 ; (tri≈ _ e≡e' _) →
       let 
         es = map proj₂ mons
       in
       case maximum e (e' ∷ es)
       of \
       { (maximum′ m _ ee'es≤m) →
             let
               e'es≡ees = PE.sym $ PE.cong (_∷ es) e≡e'
               ord-ees  = PE.subst DecrOrderedList e'es≡ees ord-e'es

               ees≤m : All (_≤ m) (e ∷ es)
               ees≤m = DPrelude.anything

               debug : All (_≤ m) (e ∷ e' ∷ es)    -- for more testing
               debug = ee'es≤m
             in
             ((pol′ ((a + b , e) ∷ mons) ord-ees) , ees≤m)
       }
----------------------------------------------------------------------

The difference is that in (I) the fields of the result of `maximum' are
extracted explicitly, by applying their labels. And in (II) their values
are found by matching against the record of the result.

(I) is type-checked.
And (II) leads to the report

------------------------
Cannot instantiate the metavariable _295 to solution All (λ section
→ section ≤ m) (e ∷ map proj₂ mons) since it contains the variable
m which is not in scope of the metavariable or irrelevant in the
metavariable but relevant in the solution
when checking that the expression ees≤m has type
_B_295 upComR a e b e' mons ord-e'es .¬a e≡e' .¬c
(pol′ ((a + b , e) ∷ mons)
 (PE.subst DecrOrderedList
  (PE.sym $ PE.cong (λ section → section ∷ map proj₂ mons) e≡e')
  ord-e'es))
------------------------

in Agda 2.5.2.

This report refers to the line after last "in".
I also add the two "debug" lines to make sure that the value of  m
is valid in the body of "in". 

Does this effect show a bug in Agda?

(Generally, matching against a record makes many programs nicer).

Thank you in advance for explanation,

------
Sergei