[Agda] strange "Unreachable clause"

[Sergei Meshveliani]

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

[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

Post by Sergei Meshveliani
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
https://lists.chalmers.se/mailman/listinfo/agda

[Ulf Norell]

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

Post by Sergei Meshveliani
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
https://lists.chalmers.se/mailman/listinfo/agda

[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

Post by Ulf Norell
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
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
https://lists.chalmers.se/mailman/listinfo/agda