[Agda] certain report

[Sergei Meshveliani]

On Tue, 2013-08-20 at 08:46 +0200, Andreas Abel wrote:
> See below.
> 
> On 19.08.13 5:58 PM, Sergei Meshveliani wrote:
> > open import Level            using (Level) renaming (zero to 0L)
> > open import Function         using (case_of_)

> [..]

> > 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 = _

> [..]
> > -----------------------------------------------------------------------
> >
> > 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
> [..]

> This is fixed in the darcs version of Agda.


All right. Thank you.
Now, I have got       Agda of darcs of August 20, 2013,

and it type-checks the `with' program version.
But the precisely similar `case' version is not type-checked.
Can you tell, please?
The precise code is

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

{- -- this works 
foo A P P? pCong x Px (t ∷ ts) (here x=Xt)  with P?x t
 
...     | yes _    = here x=Xt                                    
...     | no ¬Px-t = ⊥-elim (¬Px-t PX-t)  where                
                                          PX-t : P (X t) 
                                          PX-t = pCong x=Xt Px
                                                                                       
foo A P P? pCong x Px (t ∷ ts) (there t∈byX-ts)  with P?x t

...       | no _  = foo A P P? pCong x Px ts t∈byX-ts 
...       | yes _ = there (foo A P P? pCong x Px ts t∈byX-ts) 
-}

foo A P P? pCong x Px (t ∷ ts) (here x=Xt) =

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

foo A P P? pCong x Px (t ∷ ts) (there t∈byX-ts) =

    case P?x t of \
               { (no _)  → foo A P P? pCong x Px ts t∈byX-ts
               ; (yes _) → there (foo A P P? pCong x Px ts t∈byX-ts)
               }
----------------------------------------------------------------------

The report is 
---------------------
_x_143 A P P? pCong x Px t ts x=Xt ∷
_xs_144 A P P? pCong x Px t ts x=Xt
!= filterTriples (t ∷ ts) | P? (X t) of type List (Triple P?)
when checking that the expression
case P?x t of
(λ {(yes _) → here x=Xt;
    (no ¬Px-t) → ⊥-elim (¬Px-t (pCong x=Xt Px))})
has type Any (λ t → (A Setoid.≈ x) (X t)) (filterTriples (t ∷ ts))
--------------------


How to fix the `case'  version?

Thanks,

------
Sergei