[Agda] strange `case' requirement

[Wolfram Kahl]

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
> ".
> 
> 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?

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.

You can prove the propositional equality corresponding to the third case
as a lemma (with two cases), and then use that in appropriate circumstances.

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

(I don't really know --- but this is possibly not the dot of pattern matching,
 but the prefix given to names that are not in scope --- this comes from the
 type declaration of ``goal''?)


Wolfram