[Agda] Vezzosi's patch

[Wolfram Kahl]

On Mon, Apr 10, 2017 at 03:17:51PM +0300, Sergei Meshveliani wrote:
> Wolfram wrote recently
> 
> > Have you tried this with Andrea Vezzosi's patch from
> > https://github.com/agda/agda/issues/1625#issuecomment-132196576
> 
> I have looked there. This patch is about 
>   src/full/Agda/TypeChecking/Conversion.hs
> 
> I have  Development Agda of March 21, 2017  (ghc-7.10.2, Debian Linux)
> And the patch is probably the difference file for some old Agda.
> Is this all right?

For me, it is still working at least on 2.5.2.

> Well, I named the patch  V.diff  and commanded
> 
>   > mv V.diff  src/full/Agda/TypeChecking/
> 
>   > cd src/full/Agda/TypeChecking
> 
>   > patch Conversion.hs < V.diff
> 
> It reports that this point is found, and issues  Conversion.hs
> with is about 500 byte longer.
> 
> Is this a correct way to use this patch?

Looks good.

> Then, I install the obtained Agda, and install the standard library.
> Then I type-check my application. 

Did you remove all .agdai files? (Apparently you used a separate
standard library installation --- good.)  With the patch, some .agdai
files are different; I haven't tried to analyse this.

> But its error report is different. The original Agda succeeds, and the
> patched Agda first type-checks several files and then reports something
> like a wrong type in a certain .agda file.

I haven't had such a case yet --- if you can isolate this, it would
probably be very useful if you could report that example under
https://github.com/agda/agda/issues/1625 .



Wolfram