search

agda / agda

Agda is a dependently typed programming language / interactive theorem prover.
https://wiki.portal.chalmers.se/agda/pmwiki.php
Other
2.41k stars 339 forks source link

`show` does not respect `abstract`/`opaque` when normalising a term in a hole #7191

Closed Sean-Watters closed 1 month ago

Sean-Watters commented 3 months ago 
open import Agda.Builtin.Nat
open import Agda.Builtin.Equality
open import Agda.Builtin.String

abstract
  foo : Nat → Nat
  foo n = n + 5

show : Nat → String
show n = primShowNat (foo n)

test : show 0 ≡ "5"
test = {!refl!}  -- As expected, the abstract def prevents this from going through

_ = {!0!} -- Bad: normalises to 5, seeing through the abstract block

When I define show for a type using a function that was defined inside an abstract block, as above, I would expect it to get stuck on the abstract function foo. And indeed, that happens in most cases, eg in test. But when show is called by Agda when I normalise the goal at the end of the above example, Agda sees through the abstract block and prints 5. The same behaviour occurs when replacing abstract by opaque.

Tested on Agda 2.6.4.

nad commented 3 months ago

I assume that you (indirectly) used Cmd_compute UseShowInstance, in which case this seems to be the intended behaviour:

https://github.com/agda/agda/blob/a43f45ca661a5017c83754070394b2a755bb53dd/src/full/Agda/Interaction/BasicOps.hs#L365-L374

UlfNorell commented 3 months ago

It is indeed the intended behaviour. Can you elaborate on why this is undesirable, and what is the behaviour you suggest instead?

gallais commented 3 months ago

In a homework we used a REWRITE pragma to add a typechecking-time computational behaviour to an (abstract) function defined in terms of low-level primitives.

Unfolding the abstract definition means the REWRITE equation does not get the opportunity to fire and students using normalise & show end up with a stuck computation rather than a graphical representation of whatever complex state we are trying to show.