[Agda] failure of reduction inside an abstract block

[Paolo Capriotti]

Hi all,

I've stumbled upon a problem with types defined within an abstract
block. Sometimes, they don't get normalised as I would expect. Here is a minimal
test case:

    module test where

    open import Data.Nat
    open import Relation.Binary.PropositionalEquality

    abstract
      f : (A : Set) → Set
      f A = A

      g : subst f refl 0 ≡ subst f refl 0
      g = refl

If I take f out of the abstract block, then it works normally. I tried both Agda
2.3.2 and the development version.

BR,
Paolo