[Agda] strange "Unreachable clause"

[Sergei Meshveliani]

Thanks to James and Ulf !
I have indeed forgotten of that 0# and 1# are not constructors.
Probably, I have to require _≟_ and to use it.

------
Sergei


On Wed, 2018-05-02 at 12:52 +0200, Ulf Norell wrote:
> 0# and 1# are not constructors that you can match against. You can
> tell
> from them being highlighted in a different colour than d1 and d2.
> 
> 
> 
> It wouldn't make sense to be able to match on 0# and 1# since
> depending
> 
> on the semiring they could be the same value, or have a type that
> doesn't
> 
> have decidable equality.
> 
> 
> 
> / Ulf
> 
> 
> On Wed, May 2, 2018 at 12:35 PM, Sergei Meshveliani <mechvel at botik.ru>
> wrote:
>         Please, what is wrong in f' below? 
>         Why Agda-2.5.3 type-checks f and does not type-check f' ? 
>         
>         ---------------------------------------------------------
>         open import Level    using () renaming (zero to 0ℓ)
>         open import Algebra  using (Semiring)
>         open import Data.Nat using (ℕ)
>         
>         data Expr : Set  where c1 : ℕ → Expr
>                                c2 : Expr → Expr → Expr
>         f : Expr → ℕ
>         f (c1 _)        =  0
>         f (c2 (c1 0) _) =  0
>         f (c2 (c1 1) _) =  0
>         f (c2 _      _) =  0
>         
>         postulate R : Semiring 0ℓ 0ℓ
>         open Semiring R using (Carrier; 0#; 1#)
>         
>         data Expr' : Set  where d1 : Carrier → Expr'
>                                 d2 : Expr' → Expr' → Expr'
>         f' : Expr' → ℕ
>         f' (d1 _)         =  0
>         f' (d2 (d1 0#) _) =  0
>         f' (d2 (d1 1#) _) =  0
>         f' (d2 _       _) =  0
>         ----------------------------------------------------------
>         
>         Agda reports  Unreachable clause  for the third pattern in
>         f',  as if
>         it was shadowed by previous pattern. But it is not shadowed.
>         
>         Is this a bug in Agda-2.5.3 ?
>         
>         ------
>         Sergei  
>         
>         _______________________________________________
>         Agda mailing list
>         Agda at lists.chalmers.se
>         https://lists.chalmers.se/mailman/listinfo/agda
> 
>