20070614-1

The following program yields the message Panic: panic: Not in scope Bug.tt:

 module Bug where

 abstract

   data ⊤ : Set where
     tt : ⊤

 abstract

   view : ⊤ -> Set1
   view tt = Set

That particular program works for me. I get a panic in this case though:

 module Bug where

 abstract
   data ⊤ : Set where
     tt : ⊤

 t : ⊤
 t = tt

Here it's a case of the scope checker not handling the scoping rules for constructors of abstract datatypes properly. The bug is that the error message isn't better. / Ulf

The first program above panics in the Emacs interface, but not in the CLI. /N­AD

Fixed. The second program still panics though. / Ulf

Fixed error message for second program. / Ulf