[Agda] failure of reduction inside an abstract block

[Andreas Abel]

Well, in your example, f does not reduce in the type of g, because the 
type of g is not abstract, only the definition of g.  (Keyword abstract 
only applies to definitions, not to type signatures.)  Abstract 
definitions only reduce in other abstract things.

If f is not the identity, then the type of g is ill-formed.  So, if f 
would reduce in the type of g, then the type of g would be ill-formed 
outside of the abstract block.  This is not desired.

Cheers,
Andreas

On 26.02.13 5:01 PM, Paolo Capriotti wrote:
> 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.

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/