First docstring in a file can never belong to a top level declaration

[blackberryshortcake]

trafficstars

Steps to Reproduce

||| This should document f.
f : Nat -> Nat

Save this file, load it in the REPL and run :doc f. It doesn't matter that f is a function, it just needs to be a top level declaration.

Expected Behavior

We should see

Main> :doc f
Main.f : Nat -> Nat
  This should document f.

Observed Behavior

The top level declaration f is missing its docstring.

     ____    __     _         ___
    /  _/___/ /____(_)____   |__ \
    / // __  / ___/ / ___/   __/ /     Version 0.6.0-870bc8243
  _/ // /_/ / /  / (__  )   / __/      https://www.idris-lang.org
 /___/\__,_/_/  /_/____/   /____/      Type :? for help

Welcome to Idris 2.  Enjoy yourself!
Main>       :l "FirstDocstringAlwaysBelongsToFile.idr"
1/1: Building FirstDocstringAlwaysBelongsToFile (FirstDocstringAlwaysBelongsToFile.idr)
Loaded file FirstDocstringAlwaysBelongsToFile.idr
Main>       :doc f
Main.f : Nat -> Nat

I think (but haven't verified) that the issue comes down to https://github.com/idris-lang/Idris2/blob/870bc824371d504a03af937f326216302210a875/src/Idris/Parser.idr#L1902 because doc <- optDocumentation fname will always run before documentation of top level declarations such as f is parsed.

[gallais]

Nameless modules indeed have this intrinsic ambiguity.

But tbh if you're going to document a module, you should probably start by naming it.

[blackberryshortcake]

It was never supposed to be module documentation though...

edit: Oh, you probably mean documenting anything within a module should start with naming the module?

[gallais]

Yeah I mean if you're adding documentation to the definitions in a module then it should probably be named. Anonymous ones are only really useful as throwaways to test some code quickly.

So it is true that the grammar is ambiguous but I don't think it's worth fixing (not even sure how we would go about doing that).

[dunhamsteve]

The issue could be handled by moving the optDocumentation into the option for the module (both prog and progHdr need to match though). The problem with that is that it then fails to parse files with no module declaration, and a docstring before an import statement. This happens in a half dozen tests, and I'm afraid it might affect other code (although most code should have a module declaration).

So we can either make it an error if there is a docstring before import or paste together the docstrings before module and between module and import.

I've done the latter. I don't know if it's worth the added complexity for an edge case like this, but we might want to factor out the common code between prog and progHdr anyway. It could be a problem if a change is made to one of them and a file is parsed differently in header only mode.

Do we want this change? (TBH, I don't see people wanting to use doc strings without module declarations.) https://github.com/idris-lang/Idris2/compare/main...dunhamsteve:Idris2:issue-3068

[buzden]

Do we want this change?

I like in your change that it removes code duplication between prog and progHdr. I think it may be valuable to do this even without changing the behaviour of docstrings.