Idris2
Idris2 copied to clipboard
idris-lang
Access modifiers of definitions overwrite forward definitions
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.
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.
Right now, https://github.com/idris-lang/Idris2/commit/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:
- 👀 Leave situation as-is
- 🚀 Change max-merge to equals check without
Visibilitychange - 🎉 Change max-merge to equals check with the
Visibilitychange
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. :thinking:
http://gallais.github.io/blog/ceci-pas-default
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?
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.
