[Agda] a strange "unsolved" report

[mechvel at scico.botik.ru]

Dear Agda developers,

There is a question about the following code fragment:

-----------------------------------------------------
+ms-assoc-aux {monᶜ a e ∷ mons} {monᶜ b e' ∷ mons'} {monᶜ c e'' ∷ 
mons''} ... =

     aux (<-cmp e e') (<-cmp e' e'') (<-cmp e e'')
     where
     m = monᶜ a e;  m' = monᶜ b e';   m'' = monᶜ c e''

     mmons = m ∷ mons                 -- *

     -- m'mons' : List Mon            -- (I-s)
     m'mons' = m' ∷ mons'             -- (I)

     m''mons'' = m'' ∷ mons''
     ...
-----------------------------------------------------

Agda 2.6.1 reports
"
Sort _1156  [ at ...Over-abelianGroup.agda:414,5-12 ]
_1157 : _1156  [ at ...Over-abelianGroup.agda:414,5-12 ]
_1159 : _1157  [ at ...Over-abelianGroup.agda:414,15-25 ]
"

I guess this is the kind of "unsolved metas".
And the first "unsolved" is about the line marked (I).

The previous line (marked *) is solved - while it is not any more clear 
than (I).

Then, after adding the signature (I-s), everything is type-checked.
1) This necessity to add signature in the middle of an array of short 
assignments of the same
    type looks strange.
2) There are many similar fragments in the program, and I never observed 
such an effect.

What might this mean?

--
SM