[Agda] The joys and sorrows of abstraction

[Nils Anders Danielsson]

On 2018-05-16 18:28, Philip Wadler wrote:
> So, I have an equality that is proved under abstraction, that fails
> when the abstraction is removed. Isn't that also a failure of subject
> reduction, or stability under substitution, or some other important
> property that we care about?

Do you really have code of the form

   abstract

     <code>

that fails (ignoring resources) if abstract is removed?

I would not be surprised to see code of the following form fail when
abstract is removed:

   abstract

     <code>

   <code>

However, this seems less problematic to me. Type-checking involves
computation, and when you remove abstract you change the computational
behaviour of the code.

-- 
/NAD