# [Agda] certain report

Sergei Meshveliani mechvel at botik.ru
Mon Aug 19 17:58:53 CEST 2013

Dear Agda developers,

(I failed to connect to the Agda home page, nor to its bug tracker.
Is the Agda site all right?
).

Does the below program present a bug in Agda-2.3.2.1 (lib-0.7) ?

------------------------------------------------------------------
open import Level            using (Level) renaming (zero to 0L)
open import Function         using (case_of_)
open import Relation.Nullary using (Dec; yes; no)
open import Relation.Unary   using (Decidable)
open import Relation.Binary  using (Rel; Setoid; module Setoid;
DecSetoid; module DecSetoid)
open import Relation.Binary.Core using (_Respects_)
open import Data.Empty    using (⊥-elim)
open import Data.Maybe    using (Maybe; just; nothing)
open import Data.Product  using (_×_; _,_)
open import Data.List     using (List; []; _∷_)
open import Data.List.Any using (Any; module Any)

-------------------------------------------------------------------------
toMaybe' : ∀ {p} {C : Set} {P : C → Set p} → Decidable P → C → Maybe C
toMaybe' P? x  with P? x
...                      | yes _ =  just x
...                      | _     =  nothing

record Triple {p} {C : Set} {P : C → Set p} (P? : Decidable P) : Set 0L
where
constructor trp

field  X : C

P?x : Dec (P X)
P?x = P? X
mb : Maybe C
mb = toMaybe' P? X

filterTriples : ∀ {p} {C : Set} {P : C → Set p} {P? : Decidable P} →
List (Triple P?) → List (Triple P?)
filterTriples []      = []
filterTriples (t ∷ ts)  with  Triple.P?x t
...                      | yes _ =  t ∷ (filterTriples ts)
...                      | no _  =  filterTriples ts

open Triple

foo : ∀ {l p} (A : Setoid 0L l) →
let
open Setoid A using (_≈_) renaming (Carrier to C)
in
(P : C → Set p) → (P? : Decidable P) → P Respects _≈_ → (x : C) →
P x → (ts : List (Triple P?)) → Any (\ t → x ≈ (X t)) ts →
Any (\ t → x ≈ (X t)) (filterTriples {P? = P?} ts)

open Any

foo {l} {p} A P P? pCong x Px (t ∷ ts) (here x=Xt)

with P?x t
...      | yes q = _

{-
= case P?x t of \
{ (no ¬Px-t) → let PX-t : P (X t)
PX-t = pCong x=Xt Px
in  ⊥-elim (¬Px-t PX-t)
(yes q) → _
}
-}
-----------------------------------------------------------------------

1. The report is of kind

Inaccessible (dotted) patterns from the parent clause must also be
inaccessible in the with clause, when checking the pattern {trp},
when checking that the clause
foo {l} {p} A P P? pCong x Px (t ∷ ts) (here x=Xt) with P?x t
foo {l} {p} A P P? pCong x Px (t ∷ ts) (here x=Xt) | yes q = _
has type
...

2. Comment out the two lines of  with'  and un-comment the case'
variant.
The report is

Not in scope:
q at /home/mechvel/doconA/0.03/source/demoTest/Report.agda:61,29-30
when scope checking q

Why not in scope?  Here it must be a value  q : P (X t).

2.1. Change q' to _'
The report is
"Incomplete pattern matching for .extendedlambda0.
Missing cases: ... "

Summary:
(2.1) loooks natural,
(2) is strange,
(1) and (2.1) present a strange a strange difference between with and
case'.

------
Sergei

`