[Agda] More aggressive `with`: Please check your Agda-2.4.2 developments!

[Sergei Meshveliani]

I have tried it on  docon-A-0.03 
(see 
     http://www.botik.ru/pub/local/Mechveliani/docon-A/0.03/ 
).

   
  agda-2.4.2.5 $agdaLibOpt +RTS -M3G -RTS Structures0.agda

reports

------------
...
  Skipping OfMaps (/home/mechvel/doconA/0.03/source/OfMaps.agdai).
  piApply t = El {_getSort = Type (Max [Plus 1 (UnreducedLevel (Var 1
[]))]), unEl = Sort (Type (Max [Plus 0 (UnreducedLevel (Var 1 []))]))}
  args = [[]r(Var 0 [Proj Structures0.UpMagma.magma])]
An internal error has occurred. Please report this as a bug.
Location of the error: src/full/Agda/TypeChecking/Substitute.hs:374
------------

(Structures0.agda  is in the beginning of the application).
This bug seems familiar to me.
And docon-A-0.03 is announced as checked under  agda 2.4.2.2.

Regards,

------
Sergei



On Thu, 2015-11-19 at 14:16 +0100, Andreas Abel wrote:
> Dear Agda users and developers,
> 
> please check your larger Agda-2.4.2 developments with the version at
> 
>    https://github.com/andreasabel/agda-issue-1692/tree/maint-2.4.2
> 
> You can get it with
> 
>    git clone https://github.com/andreasabel/agda-issue-1692.git
>    cd agda-issue-1692
>    git checkout maint-2.4.2
>    make install-bin
> 
> This version is making `with` more agressive and hopefully more 
> intuitive (at least it removes the stumbling block reported in issue #1692).
> 
> The change is not fully backwards compatible. However, the breakage 
> should be small. Nothing broke for the std-lib. Only a single test case 
> broke, which uses with on a function argument (a variable):
> https://github.com/agda/agda/blob/master/test/lib-succeed/Issue846/DivModUtils.agda#L99
> The breakage was easy to fix, the new `with` is simpler: the `with` on 
> the variable could be removed.
> 
> Please check the amount of breakage on your Agda developments and report 
> back, with self-contained test-cases (e.g. as tar-balls and repo links) on
> 
>    https://github.com/agda/agda/issues/1692
> 
> This let's me evaluate whether this commit can go into the maintenance 
> version or not (in case the breakage is too big).
> 
> Response time: 5 work days.
> 
> Cheers,
> Andreas
>