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

[Andreas Abel]

In this case, there is no normalization involved.  However,

   test t with t

at type (P t) abstracts t in the goal, \ t -> P t, and then the match 
against tt instantiates the goal to P tt.  The postulate has type P t, 
and Agda has "forgotten" that t is actually equal to tt, so it complains 
that result is not of the correct type.

Cheers,
Andreas

On 05.03.13 7:03 PM, Serge D. Mechveliani wrote:
> 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
>>> [..]
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/