[Agda] Re: Issue 1402 in agda: Where clauses in rewrite RHS cause internal error

[Sergei Meshveliani]

On Sat, 2015-01-17 at 21:22 +0000, agda at googlecode.com wrote:
> Updates:
> 	Summary: Where clauses in rewrite RHS cause internal error
> 	Owner: andreas.... at gmail.com
> 	Labels: Rewrite Where
> 
> Comment #4 on issue 1402 by andreas.... at gmail.com: Where clauses in rewrite  
> RHS cause internal error
> https://code.google.com/p/agda/issues/detail?id=1402
> 
> Here is a simpled instance of the problem encounterd in the original report  
> (#1 might be a different problem).
> 
> open import Common.Equality
> 
> postulate eq : Set1 ≡ Set1
> 
> test : Set1
> test rewrite eq = bla
>    where bla = Set
> 
> It seems that somehow it is assumed that `rewrite` is not followed by  
> `where`.


So far, I have an obscure notion about using `inspect'.
Trying to guess how to use it on practice.
Also I use a certain successful piece of code:

  ...
  prove :  ins kv (ins ku (k'w ∷ ps))      =pn  
           ins (k , comb k v u) (k'w ∷ ps)
 
  prove with k ≟ k' | PE.inspect (_≟_ k) k'
  ... | yes _ | PE.[ eq ] rewrite eq =  e ∷pn =pn-refl
                     where
                     e : (k' , comb k v ckuw) =p (k' , comb k ckvu w)
                     e = (≈refl , sym-assoc-comb)
  ...

Here "rewrite eq" is followed by  "= foo where", and "rewrite eq" is
necessary for type check.
-- ??

I copy this to  agda at lists.chalmers.se  because I doubt that this is a
question about a bug.

Regards,

------
Sergei