Agda-style Lexing

I have been mulling this for a while, but the difficulties in fixing #197 made it feel more urgent.

As a (rare) user of Adga, I have been very fond of it's lexing, which seems very simple, and more concerned with the *boundaries between* tokens rather than the *contents of* tokens themselves. (You can seem me singing its praises in, e.g. https://github.com/ghc-proposals/ghc-proposals/discussions/444#discussioncomment-1509256).

I have a few questions on this.

1. Do the people *implementing* Agda agree with this premise, that lexing in Agda is significantly different and/or simpler than that in other languages? Or am I reading to much into it as a user guessing how it works?

2. If the premise is valid (per question 1), is there anything Alex might do to make this easier / a more obvious way to do things? I suppose I should study https://github.com/agda/agda/blob/master/src/full/Agda/Syntax/Parser/Lexer.x

3. Should we transition Alex itself to lex more in this style, basically requiring more things to be space-separated?

CC @andreasabel who conveniently works on both Alex and Agda, and @int-index who spearheaded the similar left right lexing context rules for Haskell.

Start by reading Agda's src/full/Agda/Syntax/Parser/Lexer.x and the discussion linked in the issue to compare its lexing approach with Alex. Review issue #197 and the referenced left-right lexing context rules. The issue does not define a concrete change or acceptance criteria; it first needs agreement on whether Alex should support or adopt this style.

Written by the indexing model from the issue text.