[Agda] [ANNOUNCE] Agda 2.6.1 release candidate 1

[mechvel at scico.botik.ru]

On 2019-12-22 14:41, Andres Sicard Ramirez wrote:
> [..]
> The Agda Team is very pleased to announce the first release candidate
> of Agda 2.6.1.
> [..]
> The RC has been tested with GHC 8.8.1, 8.6.5, 8.4.4, 8.2.2 and 8.0.2.
> [..]
> Standard library
> ==========
> 
> For the time being, you can use the *experimental* branch of the
> standard library which is compatible with the RC. This branch is
> available at
> 
>     https://github.com/agda/agda-stdlib/
> [..]


I tried it on  ghc-8.6.3 under Ubuntu Linux 18.04 on a certain small 
application
List0.agda:

   > agda $agdaLibOpt List0.agda

As I guess, it first starts type-checking the needed part of the 
"installed"
master library of December 29. And it reports

Checking List0 (/home/mechvel/inAgda/bfLib/0.3/List0.agda).
  Checking Data.List.Relation.Unary.All.Properties 
(/home/mechvel/agda/stLib/master-dec29/src/Data/List/Relation/Unary/All/Properties.agda).
   Checking Data.List.Membership.Propositional.Properties 
(/home/mechvel/agda/stLib/master-dec29/src/Data/List/Membership/Propositional/Properties.agda).
    Checking Data.List.Relation.Unary.Any.Properties 
(/home/mechvel/agda/stLib/master-dec29/src/Data/List/Relation/Unary/Any/Properties.agda).
/home/mechvel/agda/stLib/master-dec29/src/Data/List/Relation/Unary/Any/Properties.agda:251,16-27
B.b != q₁ of type Level
when checking that the inferred type of an application
   Any.map _f_1489 y∈ys ≡ pq′
matches the expected type
   Any.map (λ q₂ → p , q₂) (Any.map (λ x₁ → P.subst Q x₁ _1452) y∈ys)
   ≡ pq′

--
SM