[Agda] Circular proof causes stack overflow

[Dan Piponi]

This short piece of code causes a stack overflow in 2.3.2.1 (sometimes
after a long wait):

{-# OPTIONS --without-K --type-in-type #-}

module bug where

 open import Data.Nat

 infix 3 _≡_

 data _≡_ {A : Set} : A → A → Set where
   refl : {a : A} → a ≡ a

 infixr 14 _■_
 _■_ : {A : Set} {x y z : A} → (x ≡ y) → (y ≡ z) → (x ≡ z)
 refl ■ refl = refl

 f : ℕ → ℕ ≡ ℕ
 f zero = refl
 f (suc n) = f (suc n) ■ refl
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130904/a271f547/attachment.html