Consider where we can use `opaque` mechanism to provide abstraction

[MatthewDaggitt]

Maybe now that opaque is implemented in Agda 2.6.4 we should revisit our solution to #1753.

This is exactly the situation that the new opaque mechanism was designed for. What are people's thoughts? Too risky to adopt a cutting edge feature? In v3.0 I would imagine we will be making a lot of definitions opaque in the library?

[Taneb]

I'd love this to be done! Maybe for 2.1 rather than 2.0 though?

[MatthewDaggitt]

We can't do it for v2.1 as it'll be a breaking change 😢

[jamesmckinna]

piano, piano

FWIW, I think there are a few (!?) too many moving targets at the moment for the v2.0 release to incorporate such a new feature, especially as we have delayed and delayed and delayed the release for all kinds of reasons already.

Regarding v3.0, maybe we should be planning for this now, and not anticipating too many v2.x bumps?

[jamesmckinna]

Eg, I've been working on a revised version of #2055 which

• (BREAKING) makes Relation.Nullary.Decidable.Core.{yes|no} lazier still (and streamlining invert via its dependently-typed version)
• (DEPRECATION) lifts Relation.Nullary.Decidable.Core.recompute to Relation.Nullary.Reflects, with knock-on import simplifications
• (DEPRECATION) but with widespread knock-on consequences throughout to respond to the first change

plus misc. other overhauls. I don't want to hold anything up trying to argue for this now just because v2.0 will be the titanic breaking release... I think there will be more of those to come in future, and we should plan for that.

Mind you, if @MatthewDaggitt has self-assigned the current issue, we might have a PR for it before the meeting today ;-)

[MatthewDaggitt]

Hmm I was trying, but it turns out there's some subtlety to opaque that I hadn't quite understood. In particular you can only unfold a definition in another opaque block... which means that we'd have to have opaque blocks in the Properties files too...

Maybe I'll leave this one lie for v3.0 as @jamesmckinna suggests.