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

[Sean-Watters]

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

[gallais]

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.

[nad]

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

agda/src/full/Agda/Interaction/BasicOps.hs

Lines 365 to 374 in a43f45c

	-- | Modifier for the interactive computation command,
	-- specifying the mode of computation and result display.
	--
	computeIgnoreAbstract :: ComputeMode -> Bool
	computeIgnoreAbstract DefaultCompute = False
	computeIgnoreAbstract HeadCompute = False
	computeIgnoreAbstract IgnoreAbstract = True
	computeIgnoreAbstract UseShowInstance = True
	-- UseShowInstance requires the result to be a string literal so respecting
	-- abstract can only ever break things.

[UlfNorell]

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