[ fix ] Fix ability to declare fixities in `do`

[buzden]

Fixity declarations are instructions to parsers, thus they can appear in a lot of places in code, e.g. in lets, wheres, etc., and they work till the end of the module or hiding/redefinition, like pragmas. This indeed may be useful, say, we are definiting local function which uses some context in its closure, and we want to declare it as an infix operator: it's logical that you can declare a fixity of this function near the definition of a function, and it indeed works:

f : Nat
f =
  let (%^%) : Nat -> Nat -> Nat
      (%^%) = (+)
      private infixl 1 %^%
  in 1 %^% 2

But as soon as you try this in do-notation, it suddenly does not work:

g : Nat
g = do
  let (%^%%) : Nat -> Nat -> Nat
      (%^%%) = (+)
      private infixl 1 %^%%
  1 %^%% 2

Error: Unknown operator '%^%%'

tests.idris2.operators.operators012.Y:13:3--13:11
 09 | g = do
 10 |   let (%^%%) : Nat -> Nat -> Nat
 11 |       (%^%%) = (+)
 12 |       private infixl 1 %^%%
 13 |   1 %^%% 2
        ^^^^^^^^

More strangely, you may find that after this function definition, this infix operator is fully usable. Looks like it should work in do-notation too and was meant to work.

I realised that management of fixities is implemented in an imperative way, and just the body after let was desuraged before the let itself, which leads to this error. I propose to change the order of management in order for lets with fixity declarations to work in the same way outside and inside do-notation.

I also found a little bit more obscure, but still seemingly viable cases of such management order, you can see them at the added test case.

Thanks to @GlebChili for discovering this issue.

[dunhamsteve]

I would have guessed it was an accident that infix and other top level declarations worked in let because topDecl is being used. This also happens, but might not be desirable, in interface, implementation, and where. I think it's appropriate inside using, parameters, namespace, failing, and mutual.

So currently we can do:

interface Foo a where
    namespace What
        interface Bar b where
            export infix 8 +
            data Bool = One | Two

[andrevidela]

I think it makes sense to have fixity declaration work in local definitions. This fix should definitley be accepted.

Whether nesting any other top-level declaration should be allowed should be the topic of another issue.

I think the above fix is still suseptible to the very brittle way module visibility is implemented and so I think if the above work the fixity would still be available to the file, rather than just the body of the let. TBD if that's the case, if it is, we should open an issue for it. regardless of this problem, this diff looks good and should be merged

[buzden]

I would have guessed it was an accident that infix and other top level declarations worked in let because topDecl is being used

I'd rather agree, I also had the same feeling. The main concern of this PR is consistency between usual lets and lets in do-notation.

Regarding to the ability to declare fixities in strange places, at least for non-export ones we found it to be useful -- sometimes we need an infix function which captures the context into a closure, thus cannot be moved out to where block or to the top level. So, an ability to declare a fixity in a place where we can define a function (e.g. in let) feels desirable. Not an intuitive thing is that being declared inside some deep lexical scope, unlike other topDecls, fixities do not disappear in the end of the scope. I think this is done because of two things: imperative style of implementation of the compiler and the fact that unlike other topDecls fixities are instructions to the parser, and effect in fixity declaration must be applied as early as possible.