Internal error in Agda.Interaction.InteractionTop

[UlfNorell]

From jesper.c...@gmail.com on November 28, 2013 15:33:45

I admit this error is somewhat obscure, but it still cost me quite some time trying to find out what's wrong. How to reproduce on latest darcs version of agda:

1. Create the following 3 files in an empty directory:

=== Test1.agda ===

{-# OPTIONS --without-K #-}

module Test1 where

data ≡ {A : Set} (x : A) : A → Set where refl : x ≡ x

K : {A : Set} {x : A} (p : x ≡ x) → p ≡ refl K refl = refl

=== Test2.agda ===

module Test2 where

open import Test1

K' = K

=== Test3.agda ===

module Test3 where

open import Test2

1. Open Test3.agda in emacs and load it. You get an error in Test1.agda (this is still as expected).
2. Comment out the definition of K and reload Test1.agda. The error should now be gone.
3. Return to Test3.agda and try to load it again.

What I expect that would happen: An error telling me K is no longer in scope in Test2.agda

What I get instead: An internal error has occurred. Please report this as a bug. Location of the error: src/full/Agda/Interaction/InteractionTop.hs:852

Original issue: http://code.google.com/p/agda/issues/detail?id=983

[UlfNorell]

From ulf.nor...@gmail.com on November 29, 2013 02:14:35

Status: Accepted
Owner: ulf.nor...@gmail.com
Labels: Type-Defect Priority-High Milestone-2.3.4

[UlfNorell]

From ulf.nor...@gmail.com on November 29, 2013 04:32:19

Status: Fixed