[Agda] enigmatic `with'

[Sergei Meshveliani]

I need to add the following.
The signature for   e  needs a blank before  ∷ .
But 
a) Agda understands this  ∷,  b) inserting a blank does not change the
report.


On Thu, 2015-01-01 at 21:57 +0400, Sergei Meshveliani wrote:
> People,
> I have 
> 
>   foo : ∀ k u v ps → ... → 
>         ins (k , v) (ins (k , u) ps)  =pn  ins (k , comb k v u) ps
> 
>   foo k _ _ []    with k ≟ k
>   ...                  | yes _  =  =pn-refl
>   ...                  | no k≉k =  ⊥-elim $ k≉k ≈refl
> 
>   foo k u v ((k' , w) ∷ ps)  with k ≟ k'
>   ...
>       | no k≉k'  =  anything   -- so far
>   ... | yes k≈k' =  e  
>       where
>       ...  -- a certain prelude
>       ...
>       e : ins (k , v) (ins (k , u) ((k' , w )∷ ps)) =pn
>           ins (k , comb k v u) ((k' , w) ∷ ps)
>       e =
>         begin-pn
>           ins kv (ins ku (k'w ∷ ps))    =pn[ =pn-reflexive e2 ]
>           ins kv ((k' , ckuw) ∷ ps)     =pn[ =pn-reflexive e3 ]
>           (k' , comb k v ckuw) ∷ ps     =pn[ e0 ∷pn =pn-refl ]
>           (k' , comb k ckvu w) ∷ ps     =pn[ =pn-reflexive $ PE.sym e4 ]
>           ins (k , ckvu) (k'w ∷ ps)
>         end-pn
> 
> 1) `e' itself is type-checked, 
> 2) the signature for  e  is exactly the one required in  foo,
> 3) Agda-2.4.2.2  reports of a wrong type for  e  in the branch 
>    " yes k≈k' =  e".
> 
> Why Adga is so? What may be a way out?
> 
> Thanks,
> 
> ------
> Sergei
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>