Importing module with wrong namespace causes internal error instead of user-friendly error.

[m0rphism]

Importing module with wrong namespace causes internal error instead of user-friendly error.

[andreasabel]

Ouch! The internal error is here:

agda/src/full/Agda/Syntax/Abstract/Name.hs

Lines 149 to 154 in 403ee42

	withRangesOf :: ModuleName -> List1 C.Name -> ModuleName
	MName ms `withRangesOf` ns = if m < n then __IMPOSSIBLE__ else MName $
	zipWith setRange (replicate (m - n) noRange ++ map getRange (List1.toList ns)) ms
	where
	m = length ms
	n = length ns

However, the cause is probably in our dreaded imports logic.

[andreasabel]

Agda 2.6.1 still says:

The file /Users/abel/play/agda/bugs/Issue7208/A.agda can be
accessed via several project roots. Both A and Issue7208.A point to
this file.
when scope checking the declaration
  import Issue7208.A

[andreasabel]

Bisection says:
6c29efd is the first bad commit @rwe
Date: Tue Nov 24 15:26:01 2020 -0800

imports/refact: Move ifile module name validation into getStoredInterface

Interfaces made with `createInterface` will already have been checked by
the scope checker, and cached interfaces will already have been either
there or here.

src/full/Agda/Interaction/Imports.hs | 14 +++++++-------

[andreasabel]

This commit does not cleanly revert, so one has to understand what is going on to restore the proper error. But blaming this commit might help understanding.