Layout processing - same column ; Haskell vs Idris

[MilanKral]

Steps to Reproduce

The following code is accepted in Idris2

t : Int
t = let 
      z = 
      1000
    in 1

but the following code is not accepted in GHC:

ttt :: Int
ttt = let 
        z = 
        1000
      in 1

Expected Behavior

Because 1000 starts on the same column as z = there should be an error message. Idris 2 should only accept the following code as correct.

t : Int
t = let 
      z = 
       1000
    in 1

Observed Behavior

[gallais]

AFAICT it's unambiguous so I'm not too fussed about it.

If someone wants to look into having stricter rules for indentation levels in Idris.Parser's letBinder I won't oppose it.

[dunhamsteve]

The token following the = is not checked at all. The token after that one is checked. I initially fixed this when I did #3350, but I found that there are a dozen places in the Idris compiler and library code that rely on the faulty parsing. Those are easy to fix, but I was afraid that a lot of code in the wild would rely on that too.

For example, in Data.Seq.Internal:

viewRTree (Deep s pr m (One z)) =
  let tr =
    case viewRTree m of

The fix is:

diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr
index fd941c347..d833017b5 100644
--- a/src/Idris/Parser.idr
+++ b/src/Idris/Parser.idr
@@ -831,6 +831,7 @@ mutual
                    ty <- option (PImplicit (virtualiseFC $ boundToFC fname s))
                                 (decoratedSymbol fname ":" *> typeExpr (pnoeq pdef) fname indents)
                    (decoratedSymbol fname "=" <|> decoratedSymbol fname ":=")
+                   continue indents
                    val <- typeExpr pnowith fname indents
                    alts <- block (patAlt fname)
                    pure (MkLetBinder rig pat ty val alts)