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

[Dominique Devriese]

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 ⊤ : Set where tt : ⊤

  data P : ⊤ → Set where
    pt : P tt

  test : (t : ⊤) → P t
  test t with t
  test t | tt = {!result!}
    where postulate result : P t

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:
  test₂ : (t : ⊤) → P t
  test₂ t = go t t
    where go : (t : ⊤) → (t' : ⊤) → P t
          go t tt = result
            where postulate result : P t

By the way, in your case, the occurrence of the with-scrutinee in the
result type of your function is hidden by some calls, but Agda looks
through this and I believe the problem is the same as what I've
described above.

Regards
Dominique


2013/3/5 Serge D. Mechveliani <mechvel at botik.ru>:
> On Sun, Mar 03, 2013 at 08:25:44AM +0100, Andreas Abel wrote:
>> Sorry, I cannot explain this, because I cannot run your example
>> (incomplete). --Andreas
>>
>
>
>     http://botik.ru/pub/local/Mechveliani/agdaNotes/rep.zip
>
> contains the precise  Main.agda  and  readme.agda
> (please, read first  readme.agda).
> I am sorry: the proggram is large.
> I tried to present a small example, but have failed.
> Of course, it can be reduced, say, 10 times, but this would need a
> considerable effort.
> It looks like I am currently stuck in my attempt to write a library.
>
> Thank you in advance for help,
>
> -------
> Sergei
>
>
>
>> On 02.03.13 10:43 AM, Serge D. Mechveliani wrote:
>> >Dear all,
>> >the attachement  t.agda.zip
>> >
>> >contains a small code example where the same declaration of kind
>> >                                         postulate p : <signature>
>> >is taken in   Agda-2.3.2 MAlonzo
>> >as a correct type for  p  or not  -- depending on whether  p  is set
>> >directly after ` = ' or in the last branch for `with'.
>> >
>> >Can you, please, explain this?
>> >
>> >
>> >
>> >_______________________________________________
>> >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/
>>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda