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

[Andrés Sicard-Ramírez]

On 22 November 2015 at 09:53, Sergei Meshveliani <mechvel at botik.ru> wrote:
> ...
>   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

Thanks for testing!

For the record, the issue was generated when type-cheking
docon/source/Structures0.agda (this information was missing from the
above report).

Since I could reproduce the issue using both the maint-2.4.2 branch
and the agda-issue-1692 branch, the issue is not related to the
implementation of a more aggressive `with`.

Please report the issue in the bug tracker.

As usual, a *minimal working example* will be appreciated.

-- 
Andrés