20070627-2

The last where clause seems to be abstract, as seen from the point of bar:

 module Bug where

 data _≡_ {a : Set} (x : a) : a -> Set where
   ≡-refl : x ≡ x

 foo : Set1
 foo = Set
   where
   abstract
     bar : forall {a} (x : a) -> x ≡ x
     bar x = ≡-refl {x = y}
       where y = x

 Bug.agda:11,13-26
 y != x of type .a
 when checking that the expression ≡-refl {x = y} has type x ≡ x

The following code works, though:

 module Bug where

 data _≡_ {a : Set} (x : a) : a -> Set where
   ≡-refl : x ≡ x

 abstract
   bar : forall {a} (x : a) -> x ≡ x
   bar x = ≡-refl {x = y}
     where y = x

This does not work either, by the way:

 module Bug where

 data _≡_ {a : Set} (x : a) : a -> Set where
   ≡-refl : x ≡ x

 foo : {a : Set} (x : a) -> Set1
 foo x = Set
   where
   abstract
     y = x

     bar : x ≡ x
     bar = ≡-refl {x = y}

Fixed.