-
Notifications
You must be signed in to change notification settings - Fork 13.3k
Prohibit in-scope consts from use as variable names in binders, like nullary tags #1193
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Comments
const
|
but it works with literals and this makes it confusing, will this change? |
We could make |
While, for reference, this is okay in Erlang. -module(t).
-export([f/1]).
f(V) ->
X = 1,
case V of
X -> true;
0 -> false;
Z -> new_binding
end. and, Haskell (and OCaml) generates a warning: f d =
let x = 0
in let y = 1
in case d of
x -> True
y -> False
main = putStrLn $ show (f 3)
|
I like the idea of using In general, I wonder if allowing variable names that are identical to consts in scope has any sensible use and wether consts should not simply take precedence instead. I haven't checked but I guess this issue extends to pattern matches in let as well and maybe alternatively some syntax for explicitly splicing in expression values at match time needs to be introduced, e.g. |
We decided against this, mostly for the reason that making the meaning of a piece of code depend on which identifiers are in scope seems dangerous -- you move it, or you add some unrelated definition somewhere, and suddenly it means something else. |
What we could do is have the dot (or some other symbol) mean 'look this up in the outer namespace', rather than binding something new. That way, it'd allow one to match against consts, locals, nullary tags, and anything else that's comparable. This makes exhaustiveness and overlap checking a bit less precise, but that seems an acceptable trade-off. |
I've been trying to figure out a good "look this up in the outer namespace" disambiguator syntax for such cases for a while. About the best I can come up with is |
Eh, on further thought, I think we should just extend the analysis that prohibits colliding variable names and nullary tags to cover consts as well. A nullary tag is very similar in spirit to a const. |
The fix for this also has the effect that you can no longer name-shadow a constant (for example, if a const |
* Ensure cargo-kani setup is idempotent * add test, flip print order for better errors
The following minimal example fails with "unreachable pattern"
The text was updated successfully, but these errors were encountered: