[Agda-dev] [ANNOUNCE] Agda 2.5.3 release candidate 1

[David Darais]

Hi,

I just tried out the RC and got the following error when typechecking a file which succeeds using Agda 2.5.2.

> An internal error has occurred. Please report this as a bug.
> Location of the error: src/full/Agda/TypeChecking/Datatypes.hs:76

The file is a dependent De Bruijn encoding of System F which uses a small standard library I wrote. The piece of code that fails is:

> reduc[s][cut][⊢ᵗ][_] : ∀ {Δ₁ Δ₂ κ₁ κ₂} Δ′ (τ′ : Δ₁ ⊢ᵗ κ₁) (ρ : Δ₁ ◁ Δ₂) (τ : Δ′ ⧺ κ₁ ∷ Δ₁ ⊢ᵗ κ₂)
>   → s[⊢ᵗ] (⇈ˢ< Δ′ > (cut (r[⊢ᵗ] ρ τ′))) (r[⊢ᵗ] (⇈ʳ< Δ′ > (↑ʳ< κ₁ > ρ)) τ)
>   ≡ r[⊢ᵗ] (⇈ʳ< Δ′ > ρ) (s[⊢ᵗ] (⇈ˢ< Δ′ > (cut τ′)) τ)
> reduc[s][cut][⊢ᵗ][ Δ′ ] τ′ ρ (τ₁ ⟨→⟩ τ₂) rewrite reduc[s][cut][⊢ᵗ][ Δ′ ] τ′ ρ τ₁ | reduc[s][cut][⊢ᵗ][ Δ′ ] τ′ ρ τ₂ = ↯
> reduc[s][cut][⊢ᵗ][ Δ′ ] τ′ ρ (Var x) rewrite reduc[s][cut][∈][ Δ′ ] τ′ ρ x = ↯
> reduc[s][cut][⊢ᵗ][ Δ′ ] τ′ ρ (⟨∀⟩ {κ₁ = κ₁} τ) rewrite reduc[s][cut][⊢ᵗ][ κ₁ ∷ Δ′ ] τ′ ρ τ = ↯
> reduc[s][cut][⊢ᵗ][ Δ′ ] τ′ ρ (τ₁ ⟨⋅⟩ τ₂) rewrite reduc[s][cut][⊢ᵗ][ Δ′ ] τ′ ρ τ₁ | reduc[s][cut][⊢ᵗ][ Δ′ ] τ′ ρ τ₂ = ↯

If I comment out the right-hand-sides of each definition, the error goes away. If I comment out all but one of any of the definitions, the error remains.

If you would like to build and interact with the file, let me know and I’ll put together a self-contained directory of files which reaches the error.

Best,
David

> Date: Thu, 17 Aug 2017 03:04:13 -0500
> From: Andr?s Sicard-Ram?rez <asr at eafit.edu.co>
> To: Agda users <agda at lists.chalmers.se>, Agda dev
> 	<agda-dev at lists.chalmers.se>
> Subject: [Agda-dev] [ANNOUNCE] Agda 2.5.3 release candidate 1
> Message-ID:
> 	<CAOUWSGC-DhTskKVgLbjm+sOt9hH4iA7qP7ntsO=U30LsXoK=2Q at mail.gmail.com>
> Content-Type: text/plain; charset="UTF-8"
> 
> Dear all,
> 
> The Agda Team is very pleased to announce the first release candidate of Agda
> 2.5.3. We plan to release 2.5.3 in one week.
> 
> 
> Installation
> =======
> 
> This RC can be installed using the following instruction:
> 
>  $ cabal install
> http://hackage.haskell.org/package/Agda-2.5.2.20170816/candidate/Agda-2.5.2.20170816.tar.gz
> 
> 
> GHC supported versions
> ===============
> 
> This RC has been tested with:
> 
> * GHC 7.8.4, 7.10.3 and 8.0.2 on Linux, Mac OS and Windows
> 
> * GHC 8.2.1 on Linux and Mac OS
> 
> 
> Standard library
> ==========
> 
> For the time being, you can use the master branch of the standard
> library which is compatible with
> this RC. This master branch is available at
> 
>  https://github.com/agda/agda-stdlib/
> 
> 
> What is new, fixed issues and incompatibilities
> ============================
> 
>  http://hackage.haskell.org/package/Agda-2.5.2.20170816/candidate/changelog
> 
> 
> Enjoy the RC and please test as much as possible.
> 
> --
> Andr?s, on behalf of the Agda Team
> La informaci?n contenida en este correo electr?nico est? dirigida ?nicamente a su destinatario y puede contener informaci?n confidencial, material privilegiado o informaci?n protegida por derecho de autor. Est? prohibida cualquier copia, utilizaci?n, indebida retenci?n, modificaci?n, difusi?n, distribuci?n o reproducci?n total o parcial. Si usted recibe este mensaje por error, por favor contacte al remitente y elim?nelo. La informaci?n aqu? contenida es responsabilidad exclusiva de su remitente por lo tanto la Universidad EAFIT no se hace responsable de lo que el mensaje contenga. The information contained in this email is addressed to its recipient only and may contain confidential information, privileged material or information protected by copyright. Its prohibited any copy, use, improper retention, modification, dissemination, distribution or total or partial reproduction. If you receive this message by error, please contact the sender and delete it. The information conta
> ined herein is the sole responsibility of the sender therefore Universidad EAFIT is not responsible for what the message contains.