[Agda] strange `case' requirement

[Sergei Meshveliani]

On Sat, 2013-10-26 at 12:22 -0400, Wolfram Kahl wrote:
> On Sat, Oct 26, 2013 at 01:48:55PM +0400, Sergei Meshveliani wrote:
> > 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
> > ".
> > [..]
> > 1) Why is not the first version type-checked by normalization?


> Because the matching case here is the third case
> of your definition of _∙u_, which is only reached
> after matching the first two cases fails --- just like in Haskell.


But let us change the goal to      goal : (m : uC) → (m ∙u nothing) =u m
with remaining the implementation. 

Normalization is as follows:
(m ∙u nothing)  does not match the first rule of   _∙u_
                (uniformly for all values of  m),
and matches the second rule (uniformly for all values of  m).
The normalization result is  m.
So  uRefl  proves  m =u m,  and proves the goal.

But the report is similar, and negative. Why?

Regards,

------
Sergei