Detect import paths that only differ in capitalization

CHANGELOG.md

@@ -12,6 +12,9 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 ### Deprecated
 ### Removed
 ### Fixed
+
+- Detect import paths that only differ in capitalization (#1295)
+
 ### Security
 
 ## v0.17.1 -- 2023-12-05

quint/cli-tests.md

@@ -381,3 +381,9 @@ Regression test for [#1108](https://github.com/informalsystems/quint/issues/1108
 
 <!-- !test check 1108 -->
     quint parse testFixture/_1052one.qnt
+
+### FAIL on run river::noSolution
+
+<!-- !test exit 1 -->
+<!-- !test check parse testFixture/_1060case.qnt - parse case sensitive filenames -->
+    quint parse testFixture/_1060case.qnt

quint/src/parsing/quintParserFrontend.ts

@@ -159,29 +159,58 @@ export function parsePhase2sourceResolution(
   mainPath: SourceLookupPath,
   mainPhase1Result: ParserPhase1
 ): ParseResult<ParserPhase2> {
-  // we accumulate the source map over all files here
+  // We accumulate the source map over all files here.
   let sourceMap = new Map(mainPhase1Result.sourceMap)
-  // The list of modules that have not been been processed yet.
-  // Each element of the list carries the module to be processed and the trail
-  // of sources that led to this module.
-  // The construction is similar to the worklist algorithm:
+
+  // The list of modules that have not been been processed yet.  Each element of
+  // the list carries the module to be processed and the trail of sources that
+  // led to this module.  The construction is similar to the worklist algorithm:
   // https://en.wikipedia.org/wiki/Reaching_definition#Worklist_algorithm
   const worklist: [QuintModule, SourceLookupPath[]][] = mainPhase1Result.modules.map(m => [m, [mainPath]])
   // Collect modules produced by every source.
   const sourceToModules = new Map<string, QuintModule[]>()
+  // Collect visited paths, so we don't have to load the same file twice.
+  // Some filesystems are case-insensitive, whereas some are case sensitive.
+  // To prevent errors like #1194 from happening, we store both the
+  // original filename and its lower case version. If the user uses the same
+  // filename in different registers, we report an error. Otherwise, it would be
+  // quite hard to figure out tricky naming errors in the case-sensitive
+  // filesystems.  We could also collect hashes of the files instead of
+  // lowercase filenames, but this looks a bit like overkill at the moment.
+  const visitedPaths = new Map<string, string>()
   // Assign a rank to every module. The higher the rank,
   // the earlier the module should appear in the list of modules.
   sourceToModules.set(mainPath.normalizedPath, mainPhase1Result.modules)
+  visitedPaths.set(mainPath.normalizedPath.toLocaleLowerCase(), mainPath.normalizedPath)
   while (worklist.length > 0) {
     const [importer, pathTrail] = worklist.splice(0, 1)[0]
     for (const decl of importer.declarations) {
       if ((decl.kind === 'import' || decl.kind === 'instance') && decl.fromSource) {
         const importerPath = pathTrail[pathTrail.length - 1]
         const stemPath = sourceResolver.stempath(importerPath)
         const importeePath = sourceResolver.lookupPath(stemPath, decl.fromSource + '.qnt')
-        if (sourceToModules.has(importeePath.normalizedPath)) {
-          // The source has been parsed already.
-          continue
+        const importeeNormalized = importeePath.normalizedPath
+        const importeeLowerCase = importeeNormalized.toLowerCase()
+        if (visitedPaths.has(importeeLowerCase)) {
+          if (visitedPaths.get(importeeLowerCase) === importeeNormalized) {
+            // simply skip this import without parsing the same file twice
+            continue
+          } else {
+            // The source has been parsed already, but:
+            //  - Either the same file is imported via paths in different cases, or
+            //  - Two different files are imported via case-sensitive paths.
+            // Ask the user to disambiguate.
+            const original =
+              [...visitedPaths.values()].find(
+                name => name.toLowerCase() === importeeLowerCase && name !== importeeLowerCase
+              ) ?? importeeLowerCase
+            const err: QuintError = {
+              code: 'QNT408',
+              message: `Importing two files that only differ in case: ${original} vs. ${importeeNormalized}. Choose one.`,
+              reference: decl.id,
+            }
+            return { ...mainPhase1Result, errors: mainPhase1Result.errors.concat([err]), sourceMap }
+          }
         }
         // try to load the source code
         const errorOrText = sourceResolver.load(importeePath)
@@ -202,6 +231,7 @@ export function parsePhase2sourceResolution(
           worklist.push([m, pathTrail.concat([importeePath])])
         })
         sourceToModules.set(importeePath.normalizedPath, newModules)
+        visitedPaths.set(importeePath.normalizedPath.toLocaleLowerCase(), importeePath.normalizedPath)
         sourceMap = new Map([...sourceMap, ...parseResult.sourceMap])
       }
     }

quint/src/quintError.ts

@@ -73,7 +73,9 @@ export type ErrorCode =
   | 'QNT406'
   /* QNT407: Cannot import self */
   | 'QNT407'
-  /* QNT500: Unitialized constant */
+  /* QNT408: Case-sensitive filenames */
+  | 'QNT408'
+  /* QNT500: Uninitialized constant */
   | 'QNT500'
   /* QNT501: Internal compiler error */
   | 'QNT501'

quint/testFixture/_1060case.qnt

@@ -0,0 +1,4 @@
+module caseSensitive {
+  import importee2 as i from "_1022importee2"
+  import importee2 as I from "_1022IMPORTEE2"
+}