[Agda] signature for `with' branch

[Sergei Meshveliani]

Who knows, please,

how to reliably set a signature for the `with' branch? 
Consider functions like

  f x  with  P? x
  ... | yes _ =  g x
  ... | no _  =  aux
                 where aux : ...

or
  f x y with  compare x y
  ... | tri< _ _ _ =  g x
  ... | tri> _ _ _ =  aux
                      where aux : ...

In some cases I manage to set a signature for  aux.
In other cases Agda (2.6.0-e384ae7) does not accept any signature at
all!
On the other hand, it does report of the needed signature.
But it rejects this signature when it is set explicitly, reporting
things like this:

  Not implemented: type checking of with application
  when checking that the expression   add a (x ∷ xs) | no a≢0  
  has type  List ℕ

So that I do not see any way out.
Because composing `with' many times often leads to error reports. It is
difficult to guess of the needed nested `with' sequence, particularly as
one needs to guess at each level of whether `inspect - rewrite ' is
needed. 
This leads to that I modify a `with' sequence in many ways, and
sometimes nothing helps. And then I start to suspect a bug in Agda.  
And spend many hours in this stupid occupation
(and to prepare a bug report also takes much of time). 

Sometimes I manage to set a signature for `aux' in the branch.
Then, this helps a lot, because from `aux', the `with' sequence can be
started by new, and the problem is split to parts.
But in many cases Agda rejects all explicit signatures for `aux', so
that it is not possible to introduce any function there.

Please, see a small example attached.

Thanks,

------
Sergei

-------------- next part --------------
open import Relation.Nullary using (yes; no; ¬_)
open import Relation.Binary  using (DecSetoid; DecTotalOrder; Tri; 
                                                       StrictTotalOrder)
open import Relation.Binary.PropositionalEquality as PE using (_≡_; _≢_)
open import Data.Empty    using (⊥-elim)
open import Data.List     using (List; []; _∷_; map)
open import Data.List.All using (All) renaming ([] to []a; _∷_ to _∷a_)
open import Data.Nat      using (ℕ; suc; _+_)
open import Data.Nat.Properties using (≤-decTotalOrder; strictTotalOrder) 

decSetoid = DecTotalOrder.Eq.decSetoid ≤-decTotalOrder
open DecSetoid        decSetoid        using (_≟_)
open StrictTotalOrder strictTotalOrder using (compare) 
open Tri

postulate anything : ∀ {a} {A : Set a} → A 

add : ℕ → List ℕ → List ℕ 
add a xs  
      with a ≟ 0
...   | yes _ =  xs
...   | no _  =  aux xs 
                 where
                 aux : List ℕ → List ℕ 
                 aux []        = a ∷ []
                 aux (x ∷ xs)  with compare a x 
                 ...           | tri> _ _ _ = a ∷ x ∷ xs
                 ...           | tri≈ _ _ _ = (a + x) ∷ xs
                 ...           | tri< _ _ _ = x ∷ (add a xs)


lemma :  ∀ a xs → a ≢ 0 → All (_≢ 0) xs → All (_≢ 0) (add a xs) 

lemma a [] a≢0 _  with a ≟ 0 
...               | yes _ = []a
...               | no _  = a≢0 ∷a []a

lemma a (x ∷ xs) a≢0 (x≢0 ∷a xs≢0)  with a ≟ 0 
...
    | yes a≡0  = ⊥-elim (a≢0 a≡0)
... | no _     = aux
                 where aux : All (\y → ¬ y ≡ 0) (add a (x ∷ xs)) -- | no a≢0
                       aux = anything

                    -- All (λ section → section ≡ 0 → Data.Empty.⊥)
                    --     (add a (x ∷ xs) | no .¬p)
{-
               with compare a x 
...            | tri> _ _ a>x =  a≢0 ∷a x≢0 ∷a xs≢0
...            | tri≈ _ a≡x _ =  a+x≢0 ∷a xs≢0
                                 where
                                 a+x≢0 = anything

...            | tri< a<x _ _ =  x≢0 ∷a (lemma a xs a≢0 xs≢0)
-}