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

[Dominique Devriese]

Darryl,

Maybe I should have mentioned this, but to see the problem, you should
use the unit type defined in the code I mentioned, not the standard
unit type.  The reason is that the standard one is defined as a
record, so it enjoys eta-equality (t = tt : T for any t), while I
defined it as a data type without eta-equality because this allowed me
to demonstrate a simplified version of Serge's problem.

Dominique

2013/3/6 Darryl McAdams <psygnisfive at yahoo.com>:
> Yeah, it works fine for me.
>
>
>
> $ agda --version
> Agda version 2.3.2
>
>
>
> Full code that I used was
>
>
>
> open import Data.Unit
>
> module Experiment where
>
> data P : ⊤ → Set where
>   pt : P tt
>
> test : (t : ⊤) → P t
> test t with t
> test t | tt = result
>   where postulate result : P t
>
>
>
> - darryl
>
>
> ________________________________
> From: Andreas Abel <andreas.abel at ifi.lmu.de>
> To: Darryl McAdams <psygnisfive at yahoo.com>
> Cc: Agda List <agda at lists.chalmers.se>
> Sent: Wednesday, March 6, 2013 1:56 PM
> Subject: Re: [Agda] with match changes the result type of a function
>
> If I give "result", then I get
>
>   t != tt of type ⊤
>   when checking that the expression result has type P tt
>
> Are you sure it works for you?  If yes which system do you have?
>
> Cheers,
> Andreas
>
> On 06.03.13 4:43 AM, Darryl McAdams wrote:
>> For what it's worth, the problematic code as quoted here type checks for
>> me. That is to say, this statement:
>>
>> "Note that result is not accepted"
>>
>> is false on my system.
>> - darryl
>> ------------------------------------------------------------------------
>> *From:* Dominique Devriese <dominique.devriese at cs.kuleuven.be>
>> *To:* Serge D. Mechveliani <mechvel at botik.ru>
>> *Cc:* Agda List <agda at lists.chalmers.se>
>> *Sent:* Tuesday, March 5, 2013 11:05 AM
>> *Subject:* Re: [Agda] with match changes the result type of a function
>>
>> 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
>> <mailto: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 <mailto: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 <mailto:andreas.abel at ifi.lmu.de>
>>  >> http://www2.tcs.ifi.lmu.de/~abel/
>>  >>
>>  > _______________________________________________
>>  > Agda mailing list
>>  > Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>>  > https://lists.chalmers.se/mailman/listinfo/agda
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>> https://lists.chalmers.se/mailman/listinfo/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/
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>