[ Proposal ] Search only appropriate operator

[buzden]

I think the current determination of appropriate operators during desugaring is inconsistent. This PR tries to fix it. I'll try to explain my point.

Basically, we can look at four syntactically different groups of operators:

• prefix (*** expr),
• typebind infixr 0 ((name : expr) *** expr),
• autobind infix(/l/r) ((name <- expr) *** expr),
• regular infix(/l/r) (expr *** expr).

At each use site compiler knows which particular syntactic group is actually used. This currently determines which particular fixity definitions are used in the following way:

• if usage is prefix, then only prefix operators are searched for;
• if usage is any of typebind, autobind or regular infix, then all typebind, autobind and regular are searched for.

I think, this is very inconsistent, since we disambiguate one syntactic group from the other three, but they are all in the same level in means of syntax.

Additionally, currently, if usage is prefix and prefix one is unambiguosly chosen, but there also some other infix operators with the same name, a warning of ambuguity is shown, despite actually there is no ambiguity.

So, what I propose is to show ambiguity warnings only when there is an ambiguity inside the same syntactic groups, i.e. to preserve the current behaviour only in the case of real syntactic ambiguity. Also, I propose to look only for operators in detected syntactic group, which allows us to have, e.g. both typebinding and regular operators with different fixities with no problems (which was originally discussed as a desired thing when typebind operators were proposed). You can look for examples in the added test.

Pinging @andrevidela as the original author of typebind/autobind operators code. I've split this PR to several commits, since some of them include refactorings, just to not to disctract from the meaningful changes.

[andrevidela]

I just had a look and I'm not sure I see what the problem is and how this is addressing it. From a cursory look, this seems to only remove usability guardrails. For example, in one case we remove an ambiguity warning between prefix operator and operator sections, in the other we allow code that is syntactically ambiguous. Would you mind expanding on why this is necessary and what are the benefits for newcomers?

This also seems like a huge usability change that should probably have it's own proposal in the issue tracker to give visibility to less technical members, wouldn't you agree?

[buzden]

I'm not sure I see what the problem is and how this is addressing it

Problem 1.
With the current design of operators search we cannot use the same operator both for binding type constructor and for corresponding data constructor. E.g., now we cannot declare our own operator for dependent pairs (like, for DPair, Subset, etc) to be usable like this:

val : (x : Nat) *** x `GT` 5
val = 6 *** %search

The proposed change allows this without any warnings or errors, as one can see in the newly added tests.

Problem 2 (interconnected with the problem 1).
Current operators search algorithm, plus its warnings and errors sometimes do not make much sense. E.g. if I tried to declare typebind infix fixity for an existing operator with regular infix fixity, and then use it immediately after fixity declaration as a typebind operator, I'll get an error that I'm trying to use regular operator as a typebind operator, despite I just declared it a typebind one, e.g.

(*) : (a : Type) -> (a -> Type) -> Type
(*) = DPair

export typebind infixr 0 *

aPair : (n : Nat) * Vect n Nat -- error occurs here
aPair = (_ ** [1, 2, 3, 4, 5])

leads to

Operator * is a regular operator, but is used as a type-binding (typebind) operator.
   Explanation: regular, typebind and autobind operators all use a slightly different syntax, typebind looks like this: '(name : type) * expr', autobind looks like this: '(name <- expr) * expr'.
   
   Possible solutions:
    - Write the expression using regular syntax: 'Nat * Vect n Nat'.
    - Change the fixity defined at Prelude.Ops:6:8--6:21 to 'export typebind infixl 9 *'.
    - Hide or remove the fixity at Prelude.Ops:6:8--6:21 and import a module that exports a compatible fixity.

and the error's text does not help, actually, because it presumes a syntactic error at the use site, which, I think, is really hard to make (I'm taking not only from a personal view, but I have several employees working with Idris never doing such mistakes and I teach a course to students, so they're new to the language, and they also never do such mistakes).

Problem 2.5.
Moreover, the order of fixity declarations influence on where these error occur and which operator is considered here. So, now, compiler decides which operator fixity is right based on the order of fixities definitions, not on the syntax of usage, despite it mentions this syntax difference, and moreover, it can write syntax that it expects exactly where I wrote as it expects (like in the example above). I think, this does not bring anything good neither to newcomers, nor to experienced users.

Problem 3.
When I have declared different fixities for the same operator where fixities are prefix and infix (regular/typebind/autobind), despite giving some warnings, everything always typechecks properly despite the order or whatever, e.g.:

import Data.Maybe
import Data.String

namespace A
  export
  (***) : String -> Nat
  (***) s = fromMaybe 0 $ parsePositive s

namespace B
  export
  (***) : Nat -> Nat -> Nat
  (***) a b = a + b

export prefix 10 ***
export infix 9 ***

f : Nat -> Nat
f n = ***"12" *** n

Compiler makes a choice based on syntax at the use site, not on the order of fixity declarations. But if I do this with any different type of regular, typebind or autobind infixes, I'll get an error (plus, different errors depending on the order of fixities declarations):

namespace A
  export
  (***) : Nat -> (Nat -> Nat) -> Nat
  (***) a f = a + f a

namespace B
  export
  (***) : String -> Nat -> Nat
  (***) s n = fromMaybe n $ parsePositive s

export infix 9 ***
export autobind infixr 0 ***

f : Nat -> Nat
f n = (a <- "12" *** 5) *** S a

I called this difference between prefix-infix and infixes of different types an inconsistence in the original text of this PR.

Problem 3.5.

When I did the same operator with different fixities for purpose (e.g., for a nice DSL), like currently with prefix&infix declarations, I don't want to see loads of warnings, which I even can't turn off. The same appears if we allow different infix fixities to live together.

I understand such warnings in the case when there are some fixities declared and they are used in undeclared meaning (e.g. , there are prefix and regular infix, but I'm using it as typebind infix), or when there are several declarations within the same class (like, several regular infix declarations with different priorities). But in these cases my proposed change leaves the messages/warnings as they are now.

The only change I propose regarding warnings is when same operator deliberately has different fixities in places where these fixities are indeed used. So, I think your comment that "this seems to only remove usability guardrails" is inappropriate.

---

This also seems like a huge usability change

I don't think this change is huge at all. All previously working code should still work as it did before. I didn't change semantics of any existing thing.

... that should probably have it's own proposal in the issue tracker to give visibility to less technical members, wouldn't you agree?

I don't agree. I consider this change to be a fix of inconveniences of the original design of typebind operators search mechanism. I think the proposed behaviour raises less questions than the status quo, because now if we define similar typebind and regular operators we would have them working as those who define them would expect.

[andrevidela]

Thanks, that's a lot more clear.

Problem 1

The code written there is explicitly forbidden because it's syntacticaly ambiguous. From a syntactic perspective, *** has now two meanings and without the help of a compiler it's impossible to tell which one it is. If you remember issue #3113 the main goal was to enable feature of arbitrary syntax blocs, without their drawbacks. Syntactic ambiguity is one of them, although it should have been made clear in the original proposal.

I am personally not entirely opposed to this change, but I think it's a big one and requires approval of other members of the community, which is why I suggest turning this into an issue where non-contributors can participate.

Problem 2

I agree that the error is misleading, I think the proper error should be that we are redefining an operator already in scope. I've never written an issue about this, but there is a big hole in how we handle fixity declarations where, within the same module, we can define conflicting fixities. I think the intuition toward the problem you state is correct, that the fixity you've just declared should override the one in scope. But that's now how the system works and and for that, it needs to be redesigned. My proposal to add export declarations to fixities was a step in that direction but we need more so that fixities are scoped more carefully within namespaces. Again, this should be a proposal in and of itself.

Problem 3

This is the same as problem 1, syntactic overloading should be, if not forbidden, at least strongly discouraged.

A sidenote

There is an extra complexity brought by your PR in that it deliberately makes a choice WRT to operator overloading. One of the missing features for binding operator, for example to implement linearity, is that typebind operator do not automatically overload the non-indexed case

(-@) : (a : Type) -> (b : a -> Type) -> Type
(-@) a b = (1 x : a) -> b x

typebind infixr 0 -@

test : Nat -@ Nat -- nope
test n = n

test2 : (n : LNat) -@ LVect n String -- ok
...

Your proposal fixes that by allowing to overload two functions (-@)

(-@) : (a : Type) -> (b : a -> Type) -> Type
(-@) a b = (1 x : a) -> b x

namespace NonDep
  (-@) : (a : Type) -> (b :  Type) -> Type
  (-@) a b = (1 x : a) -> b 

typebind infixr 0 -@

test : Nat -@ Nat -- ok
test n = n

test2 : (n : LNat) -@ LVect n String -- ok
...

Again, I'm not opposed to this in principle but we should at least get the feedback of the community for which one of the two feature to implement. Personally, I'd be inclined to prefer the first (overload typebind to allow non-dependent calls) because it avoids duplicating a function, and also because it avoids the opportunity to write a bug where the non-dependent and the dependent version do different things

Conclusion

I think we're making progress, but the solution proposed seems, to me, that it pushes users too readily toward misuse, rather than fix the shortcomings of the fixity implementation. To recap here are the problems I'm seeing:

• Fixity declarations can't shadow each other within modules
• Compatible fixity declarations can't be used side by side

The first one is a design issue related to how fixities were implemented in the first place and definitely needs to be fixed sooner rather than later. This PR isn't a solution for that.

The second one is a deliberate design choice and I don't think either of us are enough to make the call to change it. I came up with those restrictions in the context of a new features with lots of opportunities for misuse, the original proposal was extremely conservative for this reason. Nowadays it might be possible to ease some of those restrictions but I'm not ready to make that call myself, and I don't think you should either. We need to ask for feedback from more users. Just to be clear, "i have students and they never make that mistake" is not feedback I can do anything about. Your population sample is not representative, the methods and results aren't public, and Idris the programming language isn't aimed at your students specifically, but at everyone in the world. So we're going to need a bit more than vibes for that

[andrevidela]

I changed the title because this is not a bug fix, there is no bug, the current behaviour is as intended. This is a proposal to change the behaviour of two features: fixity shadowing and binding operator overloading