Revert cyclic computation of ranges (and ban `mdo` from this code base)

[andreasabel]

https://github.com/agda/agda/blob/ee1b7beb3d45d507ff0ec60c5f1f7a18d6772063/src/full/Agda/Interaction/Imports.hs#L133-L146 This change in 2.6.3 caused the SrcFile component of ranges to be black holes during parsing, making stuff not Showable and causing regression #7301.

• 7301

This regression shows that playing with exotic language features like mdo can lead to obscure termination bugs that are very hard to discover (the code that loops is fine, but the data it processes goes to Nirwana when you try to look at it).

I think we should find another solution to the mapping of ranges to files/modules, one that is robust and does not make debugging a mine field. And then ban mdo. ATTN: @nad

Keywords: TopLevelModuleName, MonadFix

[UlfNorell]

Here's the only other use:

https://github.com/agda/agda/blob/c563c5e7fef788ae00471210d6409e5540427dd7/src/full/Agda/TypeChecking/RecordPatterns.hs#L687-L693

[andreasabel]

Here's the only other use:

Indeed, and this is dead code since we replaced the record pattern translation by some other implementation.

[andreasabel]

I am experiencing a looping Agda when I prefix the following call to warning with a setCurrentRange: https://github.com/agda/agda/blob/df44b12dd50aa897bf52508335c884bb18a3be15/src/full/Agda/TypeChecking/Warnings.hs#L217-L220 I suspect this is again to the cycles in Range generation.

ATTN: @nad

[andreasabel]

Currently our ranges are a coinductive type: Agda.Syntax.Position:

type Range = Range' SrcFile

data Range' a
  = NoRange
  | Range !a (Seq IntervalWithoutFile)

type SrcFile = Strict.Maybe RangeFile

data RangeFile = RangeFile
  { rangeFilePath :: !AbsolutePath
    -- ^ The file's path.
  , rangeFileName :: !(Maybe (TopLevelModuleName' Range))
    -- ^ The file's top-level module name (if applicable).
    --
    -- This field is optional, but some things may break if the field
    -- is not instantiated with an actual top-level module name. For
    -- instance, the 'Eq' and 'Ord' instances only make use of this
    -- field.
    --
    -- The field uses 'Maybe' rather than 'Strict.Maybe' because it
    -- should be possible to instantiate it with something that is not
    -- yet defined (see 'Agda.Interaction.Imports.parseSource').
    --
    -- This '(TopLevelModuleName' Range)' should not contain a range.
  }

Agda.Syntax.TopLevelModuleName:

type TopLevelModuleName = TopLevelModuleName' Range

Agda.Syntax.TopLevelModuleName.Boot:

data TopLevelModuleName' range = TopLevelModuleName
  { moduleNameRange :: range
  , moduleNameId    :: {-# UNPACK #-} !ModuleNameHash
  , moduleNameParts :: TopLevelModuleNameParts
  }

The natural solution would be to have an ID for top-level-module names in scope. A position would be a pair of such an ID and an offset into the file.

Also, before scope checking (i.e. during parsing and nicifying) all ranges just refer to the one file we are processing, so they would not even need a file ID then. It could be added by the scope checker.