Counterintuitive behaviour of `%unbound_implicits off` in a `where` block

[buzden]

Steps to Reproduce

Consider a code where you turned off unbound implicits in a where-block of a function. As soon as we are allowed to use %unbound_implicits in where-blocks, I would expect that the status of unbound implicits turning off resets after the where-block, thus allowing to use unbound implicits later in the code.

import Data.Vect

g : Vect n a -> Nat
g xs = x $ lengthCorrect xs where

  %unbound_implicits off

  x : length xs = n -> Nat
  x _ = 5

f : List a -> Nat

Expected Behavior

Typecheks

Observed Behavior

Error: While processing type of f. Undefined name a.

UnboundImplsWhere:19:10--19:11
 15 |
 16 |   x : length xs = n -> Nat
 17 |   x _ = 5
 18 |
 19 | f : List a -> Nat
               ^

[gallais]

It's counter intuitive if you assume pragmas are scoped directives but they're toggles for a stateful config. Making them scoped could have drawbacks (e.g. %logging off in a nested block would require more %logging offs at lesser indentations to guarantee logging is really off).

[buzden]

The drawback of toggling a stateful config is that when I paste or even just work on a piece of code with scoped stuff like %unbound_implicits or even %logging, I have no option to restore the setting that was before my code. That is, I have no instruments to say "this is a piece of code with alternative config".