[Agda] The joys and sorrows of abstraction

[Martin Escardo]

On 16/05/18 20:37, Philip Wadler wrote:
> Thanks for following up. It is the latter case. But I don't understand 
> why it should be ok for that to fail. Removing abstract should just 
> replace some abstract terms by their concretions, which have already 
> been type checked. Everything that was provably equal before should 
> still be equal, so why is it ok for the proof of equality to now fail? 
> Doesn't this violate stability under substitution? Cheers, -- P

It is because of things such as this that I prefer to restrict my usage 
of Agda to a fragment corresponding to a well-understood type theory.

This may be limiting in terms of expressivity, conciseness, and 
efficiency, but at least one can tell whether something is a bug or not, 
rather than a bug or a feature.

:-)
Martin