[Agda] certain report

[Sergei Meshveliani]

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'.

Please, advise.

------
Sergei