[ upstream ] Adapt IData & examples to the presence of WithDefault

[Adowrath]

C.f. https://github.com/idris-lang/Idris2/pull/3063

I've done the change non-invasively here, only adapting the implementation of idata instead of modifying each occurrence of Visbility, because explicitly specifying the default doesn't make sense (we don't use MkLater after all).

[buzden]

Looks like this is the most reasonable change to make the original PR work. But I checked that after applying your changes on the state of the compiler's PR, docs do not typecheck pack build elab-util-docs fail, mostly with ambiguity errors:

16:22 buzden@saoirse ~/.../idris2/theirs/elab-util^incompatible-visibilities-upstream $ pack build elab-util-docs
[ info ] Found local config at /home/buzden/devel/idris2/theirs/elab-util/pack.toml
[ info ] Using package collection nightly-230828
[ build ]  1/33: Building Language.Reflection.Syntax (src/Language/Reflection/Syntax.idr)
[ build ]  2/33: Building Language.Reflection.Types (src/Language/Reflection/Types.idr)
[ build ]  3/33: Building Language.Reflection.Derive (src/Language/Reflection/Derive.idr)
[ build ]  4/33: Building Language.Reflection.Util (src/Language/Reflection/Util.idr)
[ build ]  5/33: Building Doc.Primitives (src/Doc/Primitives.md)
[ build ] Error: While processing right hand side of ==. Ambiguous elaboration. Possible results:
[ build ]     Doc.Primitives.AtomicNr.value
[ build ]     Language.Reflection.TTImp.value
[ build ] 
[ build ] Doc.Primitives:73:20--73:25
[ build ]  69 | Some standard interface implementations come almost for free:
[ build ]  70 | 
[ build ]  71 | ```idris
[ build ]  72 | Eq AtomicNr where
[ build ]  73 |   (==) = (==) `on` value
[ build ]                          ^^^^^
[ build ] 
[ build ] Error: While processing right hand side of compare. Ambiguous elaboration. Possible results:
[ build ]     Doc.Primitives.AtomicNr.value
[ build ]     Language.Reflection.TTImp.value
[ build ] 
[ build ] Doc.Primitives:76:26--76:31
[ build ]  72 | Eq AtomicNr where
[ build ]  73 |   (==) = (==) `on` value
[ build ]  74 | 
[ build ]  75 | Ord AtomicNr where
[ build ]  76 |   compare = compare `on` value
[ build ]                                ^^^^^
[ build ] 
...

[Adowrath]

Ah, my bad, I ran make test to check but didn't see that the docs were included as literal files in a different package. I'll look into it.

[buzden]

Okay, I've checked the update, all works. I'm ready to merge this PR as soon as we are in sync with an upsteam's maintainer, so that we merge both PRs in a single day.

BTW, @Adowrath, are you aware that your original change also breaks LSP? It is not in the Idris2'es CI yet, but this will immediately touch the pack collection the next night.

The last thing I want to ask is -- isn't there any better name rather than value for this function, that is not meant to be used very widely. I mean, this rather rare function would very likely cause ambiguity error with some user functions. I mean, it's okay even now, since only those importing Language.Reflection are affected by this, but now more and more people do have this imported (even without knowing it) because of wider spread of elaboration scripts, say, for derivation. Maybe, there was some alternative you were thinking about during implementation of the original PR?

[Adowrath]

BTW, @Adowrath, are you aware that your original change also breaks LSP? It is not in the Idris2'es CI yet, but this will immediately touch the pack collection the next night.

I was not, that's good to know. I actually haven't even used pack and such, and am rather busy with a uni project for this week, so I think I'll put this on hold until next week and then look into it. 👍

The last thing I want to ask is -- isn't there any better name rather than value for this function, that is not meant to be used very widely. I mean, this rather rare function would very likely cause ambiguity error with some user functions. I mean, it's okay even now, since only those importing Language.Reflection are affected by this, but now more and more people do have this imported (even without knowing it) because of wider spread of elaboration scripts, say, for derivation. Maybe, there was some alternative you were thinking about during implementation of the original PR?

I will also look into changing it to a more descriptive name (cc to future me: nonDefaultValue sounds reasonable). Thanks for bringing it up.

[buzden]

Sorry, I force-pushed this branch by mistake, but I returned it to the original state

[buzden]

@Adowrath when you have time, could you please rebase both this and the upstream PRs to corresponding mains. Now we've automated testing of such pairs of PRs

[Adowrath]

@Adowrath when you have time, could you please rebase both this and the upstream PRs to corresponding mains. Now we've automated testing of such pairs of PRs

Should be done?