Access modifiers of definitions overwrite forward definitions

[ohad]

Steps to Reproduce

$ cat Mutual.idr
module Mutual
private
data Foo : Type 

public export
data Foo : Type where
------------------------------
$ cat Import.idr
import Mutual

x : Foo

Expected Behavior

Type-checking Mutual.idr should report an error because the access modifiers are incompatible.

Observed Behavior

The latest definition overwrites the access modifier, and Import.idr type-checks fine.

[gallais]

I'm going to go ahead and tag this as good first issue because I assume it's something silly
like overwriting the existing value with a record update instead of making sure it's not set yet.

[Adowrath]

Right now, f76c4c4307 "fixes" this by forcing the maximum visibility to apply. This makes any combination of the three modifiers on either of the forward or actual declaration result in the higher of the two, e.g.

module Mutual

private
data Foo : Type

export
data Foo : Type where

module Mutual

export
data Foo : Type

private
data Foo : Type where

both work as if a single declaration with export was defined.

We can either leave it like this and close the issue (unsatisfying) or modify the max-merge to instead check whether they're the same and throw an error if not - this however makes the following not work anymore:

module Mutual

export
data Foo : Type

-- no visibility
data Foo : Type where

Which, while technically consistent (no visibility == private, and private != export), means you would need to repeat the same visibility in both places. This breaks code in an unsatisfying way, while the general idea of removing the max-check itself breaks code that relied on what seemed like buggy behaviour?

Making the above export+<nothing> declaration possible would require modifying either Visibility - add Unspecified which means "Can be overriden, otherwise means private" or change most occurrences of Visibility to Maybe Visibility, but could be done.

I'll put this up here before I tackle solving it, so please add your input which solution would be the best!

Might even be a good idea to add votes, so:

1. 👀 Leave situation as-is
2. 🚀 Change max-merge to equals check without Visibility change
3. 🎉 Change max-merge to equals check with the Visibility change

[gallais]

If only we had a gadget that allowed us to express that something is the default
without conflating it with the default value it takes. 🤔

http://gallais.github.io/blog/ceci-pas-default

[Adowrath]

If only we had a gadget that allowed us to express that something is the default without conflating it with the default value it takes. 🤔

http://gallais.github.io/blog/ceci-pas-default

Are you suggesting I use this to implement Nr. 3? Or just a general comment?
Where would I place it? src/Libraries/Data/WithDefault.idr or would it warrant a placement in base?

[gallais]

Yeah I think it'd be nice to complain if there are conflicting declarations which means changing
the merge strategy to take into account lack of value vs. value that happens to equal the default.

[emdash]

Is this still an issue? It seems like we get correctly warned now...