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

[David Darais]

Hi Andrés,

I’ve filed the issue and uploaded a self contained project which triggers the error.

https://github.com/agda/agda/issues/2703

Best,
David Darais

> On Aug 17, 2017, at 12:47 PM, Andrés Sicard-Ramírez <asr at eafit.edu.co> wrote:
> 
> Hi,
> 
> Thanks for reporting the error.
> 
> On 17 August 2017 at 11:29, David Darais <david.darais at gmail.com> wrote:
>> 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.
> 
> I think we need the self-contained directory.
> 
> Can you file an issue in
> 
>  https://github.com/agda/agda/issues
> 
> ?
> 
> If this is not possible, I'll file the issue for you.
> 
> 
> Best,
> 
> --
> Andrés
> 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 contained herein is the sole responsibility of the sender therefore Universidad EAFIT is not responsible for what the message contains.