Skip to content

Instantly share code, notes, and snippets.

@atacratic
Created December 5, 2016 21:27
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save atacratic/bd9e08b43717dc50d31bcc2f27842a03 to your computer and use it in GitHub Desktop.
Save atacratic/bd9e08b43717dc50d31bcc2f27842a03 to your computer and use it in GitHub Desktop.
Idris namespaces are not privileged for disambiguation within their own scope
-- I would like to try two options for a bit of code, within the same file...
namespace Option1
foo : Nat
bar : Nat -> Nat
bar n = n + foo
namespace Option2
foo : Nat
bar : Nat -> Nat
bar n = n + foo - 1
-- ... but I can't. I get:
-- Can't disambiguate name: Main.Option1.foo, Main.Option2.foo
-- Obviously, I could use two files. Or I could disambiguate the calls to foo with Option1.foo and
-- Option2.foo - but then I'd have to undo that edit when I commit to one of the options and get rid
-- of the namespace.
-- "using namespace" doesn't seem to exist, and "with <NAMESPACE> <EXPR>" is only for expressions.
-- Could disambiguation privilege the current namespace?
@atacratic
Copy link
Author

atacratic commented Dec 5, 2016

Reply from Edwin:

[21:30] edwinb: I don't think we should ever have a situation where there are potentially two valid interpretations of some code and Idris just picks one
[21:30] edwinb: if there's ambiguity, I would rather it be resolved explicitly
[21:31] edwinb: (exception: auto implicits, because part of the point of them is that it really doesn't matter what value is filled in)
[21:32] atacratic: Okey doke, good reason :-) thanks
[21:34] edwinb: I know it's irritating, because I've also wanted that myself, but that is the reason I've resisted

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment