[Agda] strange `case' requirement

[Sergei Meshveliani]

People,
I write

  _∙u_ : Op₂ uC
  (just x) ∙u (just y) = just (x ∙ y)
  m        ∙u nothing  = m
  nothing  ∙u m        = m

for  uC = Maybe C,  and a semigroup operation  _∙u_ : Op₂ C
(this is extending a semigroup with  unity  represented as `nothing').
Then I prove

  goal : (m : uC) → (nothing ∙u m) =u m
  goal m =  IsEquivalence.refl uEquiv
            where
            uSetoid = Data.Maybe.setoid setoid
            uEquiv  = Setoid.isEquivalence uSetoid 
             
The report is
"
nothing ∙u .m != .m   of type  Maybe (Setoid.Carrier ......)
when checking that the expression uRefl has type  
nothing ∙u .m =u .m
".

After several minutes I guess to try
                                 goal nothing  = uRefl 
                                 goal (just _) = uRefl,
It does work. But looks ugly.

1) Why is not the first version type-checked by normalization?
Is this by a fundamental reason, or by a confusion that can be improved
in further type checker? 

2) Why  m  is dotted in the report, has this sense?

This is on  Agda of darcs about  August or September 2013.

Regards,

------
Sergei