[Agda] strange "Unreachable clause"

[James Wood]

0# and 1# from Semiring are not constructors, so can't be used as
patterns. In the definition of f', “0#” and “1#” are interpreted as
names of pattern variables, shadowing the Semiring fields. You could
replace “0#” by “x”, for example, and the meaning would be the same.

In general, this pattern matching is not possible because it's not
possible in general to test whether a given value from the carrier set
is (definitionally or by _≈_) equal to 0# or 1#. A counterexample would
be having a semiring over K, and deriving from it the semiring over
Stream K where all of the operations are done pointwise. Then,
comparison to 0# (that is, 0# ∷ 0# ∷ 0# ∷ ...) is undecidable.

To do something like what you want to do, you'll need to assume a
decision procedure for _≈_ (see Relation.Binary, Decidable). You can
then take cases on x ≟ 0# and x ≟ 1#.

James


On 02/05/18 11:35, Sergei Meshveliani 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