[Agda] with match changes the result type of a function

[Serge D. Mechveliani]

On Tue, Mar 05, 2013 at 05:05:20PM +0100, Dominique Devriese wrote:
> Serge,
> 
> I've taken a brief look at your code, and I think this is a simplified
> version of your problem:
> 
>   module test where
> 
>   data T : Set where tt : T
> 
>   data P : T -> Set where
>     pt : P tt
> 
>   test : (t : T) -> P t
>   test t with t
>   test t | tt = {!result!}
>     where postulate result : P t
> 

(a have changed to `T' and `->').

What does this mean this denotation with "{!" ?

> Note that result is not accepted despite the fact that it has exactly
> the declared type of test's result, which I believe is what you are
> seeing in your code as well.  The problem is that test's result type
> is changed when you do a with-match on t, by substituting tt for t. 
> A solution is to replace your use of with by an explicit helper
> function, where you can tightly control exactly which occurrences of
> the with-scrutinee are replaced by the pattern:
>
> []

Thank you very much. I shall try.

This `with' issue is difficult to understand.
In the line of                           test t | tt = {!result!}

t  is an arbitrary value in the type  T.  Hence  (P t)  in `postulate'
must have the same type value as  (P t)  in the signature for `test'
-- ?

Could you or Andreas demonstrate on  this small example
how Agada plays this trick with normalizations which lead to different 
type normal forms?

Regards,

------
Sergei


> 2013/3/5 Serge D. Mechveliani <mechvel at botik.ru>:
> > [..]
> >     http://botik.ru/pub/local/Mechveliani/agdaNotes/rep.zip
> >
> > contains the precise  Main.agda  and  readme.agda
> > [..]