[Agda] matching to Sum

[Sergei Meshveliani]

On Tue, 2013-10-15 at 01:07 +0200, Andreas Abel wrote:
> The pattern matching is incomplete.  It works with complete pattern 
> matching:
> 
> cons-hasRepetition A x (y ∷ xs) (inj₁ y∈xs) = inj₂ (inj₁ y∈xs)
> cons-hasRepetition A x (y ∷ xs) (inj₂ h)   = inj₂ (inj₂ h)
> cons-hasRepetition A x [] (Level.lift ())

I see. Thank you

Does the checker report need improvement?
("Incomplete pattern matching" 
 rather than 
 "Cannot split on argument of non-datatype"
).

I often advance with implementation by doing the first pattern.
After I get "Incomplete pattern matching", I see that the given patterns
are checked, and start with the next pattern.

And in this case I was mislead.
Where is an argument of non-datatype?

Regards,

------
Sergei


> 
> On 12.10.2013 21:38, Sergei Meshveliani wrote:
> > Please, why the pattern  (inj₁ y∈xs)   below is checked-out?
> >
> > I know that
> >         cons-hasRepetition A x xs hasRep-xs =  inj₂ hasRep-xs
> >
> > is sufficient.
> > But the question about the pattern  (inj₁ y∈xs)  still remains.
> >
> >
> > -----------------------------------------------------------------
> > module Report4 where
> > open import Level using (Level; _⊔_; Lift)
> > open import Relation.Binary using (Setoid; module Setoid)
> > open import Data.Empty    using (⊥)
> > open import Data.Sum      using (_⊎_; inj₁; inj₂)
> > open import Data.List     using (List; []; _∷_)
> > open import Data.List.Any using (module Membership)
> >
> > --------------------------------------------------------------------
> > hasRepetition : ∀ {c l} (A : Setoid c l) → List (Setoid.Carrier A) →
> >                                                          Set (c ⊔ l)
> > hasRepetition _ []       =  Lift ⊥
> > hasRepetition A (x ∷ xs) =  x ∈ xs  ⊎ (hasRepetition A xs)
> >                          where
> >                          open module MembA = Membership A using (_∈_)
> >
> > cons-hasRepetition :
> >          ∀ {c l} (A : Setoid c l) →
> >          let C = Setoid.Carrier A
> >          in
> >          (x : C) → (xs : List C) → hasRepetition A xs →
> >                                    hasRepetition A (x ∷ xs)
> >
> > cons-hasRepetition A x (y ∷ xs) (inj₁ y∈xs) =  inj₂ (inj₁ y∈xs)
> > --------------------------------------------------------------------
> >
> > The report is
> >
> >    Cannot split on argument of non-datatype   hasRepetition A xs
> >    when checking the definition of  cons-hasRepetition.
> 
>