Add a warning for incompatible visibilities on forward decls and definitions.

[Adowrath]

Description

This addresses #1236 by introducing a warning when a forward declaration and actual definition of a data or record type have differing visibility modifiers, unless the definition has none at all - thus it allows code like the following:

public export
data Foo : Type

data Foo : Type where
  MkFoo : Foo

This makes Foo be publicly exported, yet either export or private would be a warning as suggested by @andrevidela so it can be turned into an error after an upcoming release.

Current behaviour is to take the maximum of the two visibility modifiers, so this is technically a breaking change (though taking the max felt like a buggy behaviour).

The special-casing of an absent visibility modifier required the addition of Libraries.Data.WithDefault, adapted from @gallais's post on explicit defaults. I had to therefore add to the TTC format since this field is stored in the IData and IRecord constructors, and also modiy the TTImp datatypes used in Reflection, making this truly a breaking change.

Should this change go in the CHANGELOG?

• If this is a fix, user-facing change, a compiler change, or a new paper
  implementation, I have updated CHANGELOG.md (and potentially also
  CONTRIBUTORS.md).

[gallais]

Nice. I think we're close!

[Adowrath]

@gallais Encapsulated WithDefault with the two smart constructors, as well as adding a maybe-like catamorphism in onWithDefault for when you still want to reduce the two cases differently - mainly used in the TTC and Reflect implementations because otherwise it'd look e.g. like this

{def : a} -> TTC a => TTC (WithDefault a def) where
  toBuf b def = if isDefault def
                then tag 0
                else do tag 1
                        toBuf b $ collapseDefault def

onWithDefault makes sure you don't mix up the two cases but also in this case allows removing the implicit {def : a} from the constraints. If we passed along the default value to the defaultHandler ((tag 0) in the above example) it could still lead to ambiguity for a user, which is why I chose not to do that.

[Adowrath]

Regarding the failing CI test, it appears to be ubuntu-test-elab, which pulls in Z-snail's prettier and tries to build it, failing because it needs to be updated with regards to the WithDefault change. What should I do about this? I can't exactly introduce such a change in their repository yet I think, no?

[gallais]

You can open PRs to these repos to get the fixes merged upstream.
We can then restart the failing tests to check everything is now alright
and then go ahead and merge this PR once it's all green on our side.
Cf. what I did for #3062

[Adowrath]

Some more changes to accomodate the LSP package on pack and such are required, and I will be busy for this week, so I'm going to mark this as a draft for now.
@gallais Also a general question, would it be okay to rebase this later into more coherent commits or should I leave the history intact, which would fit the commit history after merge better?

[gallais]

By default we squash on merge so there is no need to clean up the history.

[andrevidela]

Is this just stuck ebcause of elab-utils?

[buzden]

Is this just stuck ebcause of elab-utils?

No, not really, elab-util's PR is ready to go in a sync with this PR. But there was decided that a small change to this PR should be done + LSP breakage fix should be suggested.

[andrevidela]

I'm confused as to where this is blocking now, is it because of LSP?

[Adowrath]

I'm confused as to where this is blocking now, is it because of LSP?

I'm sorry, I lost track of this. Currently blocked because of the LSP, but potentially other stuff in pack too, plus the names are a little too general/may cause confusion or other conflicts so I'll change those into more explicit ones too. I'll look into seeing what it does with the libraries in pack by the end of this week and finish up.

[gallais]

I think we should move ahead with this PR.
It's good work and it'd be a shame to see it disappear because
it'll force downstream projects to make some minor updates.

[Adowrath]

I think we should move ahead with this PR. It's good work and it'd be a shame to see it disappear because it'll force downstream projects to make some minor updates.

Hey Guillaume, thanks for the kind words. I actually renamed a couple of functions & the data constructors due to feedback (value was very generic, it changed to specified and defaulted respectively) and will push that change in a bit. I'm also trying to test pack's db build at the same time to verify/at least find the bugs, and will push the rename fix to elab-util as well, but that will be a bit later. Just look at the minor changes in the commit that comes in a few minutes please, that will be the final in Idris' codebase itself. 👍

Edit: Pushed too eagerly, ah. Will update with the new, fixed tests again.

[buzden]

elab-util has been checked upon this PR and appropriate PR to elab-util is ready to be merged as soon as this PR is decided to be merged.

[Adowrath]

Idris2-lsp also received a pending PR. Some other libraries in pack currently don't compile, but I'll work on PRs for those after this.

[Adowrath]

Actually needed one small change to let pretty-show derive its PrettyVal instance (stefan-hoeck/idris2-pretty-show#30), WithDefault needs to be public in the user-facing version (even though the helper constructors are to be preferred).

[gallais]

I'm happy to merge this today.

[Adowrath]

I'm happy to merge this today.

Should be good, PRs to libraries in Pack have been submitted and I can check the collection in a docker container with those modified dependencies, and all compile (some tests are failing but that's neither a blocker nor caused by this change, necessarily).

[buzden]

I'm happy to merge this today.

As far as I understand, LSP's PR won't be merged until this PR is merged because they use this repo as a submodule. I'm ready to merge the accodring update to elab-util now. Are we good to go with red CI because of LSP?

[gallais]

Sure, let's go.

[buzden]

Sure, let's go.

elab-util is ready

[Adowrath]

LSP has been updated with the commit of the new main. 👍

[Adowrath]

With v0.7.0 out, should I already create a patch changing this into a hard error that we can merge later, or can that wait?