The paragraph you are quoting starts with:
Informally stated,
and it is indeed just a quick overview of what is happening, meant to give you some intuition. The formal rules are in section 10.3 Layout.
What happens in your case is that your code gets changed into:
y :: [Int]
y = do
{ c <- [4, 4, 4]
; return c
; ... {- we are here -}
the last rule applied being, indeed:
L (<n> : ts) (m : ms) = ; : (L ts (m : ms)) if m = n
However note that emitting ++ now would cause a parse error, and thus this rule kicks in:
L (t : ts) (m : ms) = } : (L (t : ts) ms) if m∕ = 0 and parse-error(t)
(Note 5)
So a closing brace is emitted instead and after that the lexer proceeds normally.
In the end, your code is parsed as:
```haskell
y :: [Int]
y = do
{ c <- [4, 4, 4]
; return c
; } ++ [1]
Actually, the overview section mentions this behaviour too (although, admittedly, it is not particularly easy to understand what it says):
A close brace is also inserted whenever the syntactic category containing the layout list ends; that is, if an illegal lexeme is encountered at a point where a close brace would be legal, a close brace is inserted.