Internal error typechecking non-terminating function on case-insensitive filesystem

[james-smith-69781]

Working through the tutorial at http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf , I wanted to see the error given by 'fold'. Here is the somewhat-minimized code:

module Universesbug where

data Functor : Set₁ where

[_] : Functor → (Set → Set)

map : (F : Functor){X Y : Set} → (X → Y) → [ F ] X → [ F ] Y

data μ_ (F : Functor) : Set where
  <_> : [ F ] (μ F) → μ F

fold : (F : Functor){A : Set} → ([ F ] A → A) → μ F → A
fold F φ < x > = φ (map F (fold F φ) x)

An internal error has occurred. Please report this as a bug. Location of the error: __IMPOSSIBLE__, called at src/full/Agda/TypeChecking/Errors.hs:296:\ 18 in Agd-2.6.2-d8dfa68e:Agda.TypeChecking.Errors

Agda installed from Homebrew:

% agda --version
Agda version 2.6.2

[gallais]

Strange, I can't reproduce this in either 2.6.1.3 or 2.6.2

in Agd-2.6.2-d8dfa68e

I can't find this Agda commit in the git history. 🤨

Edit: I have just compiled & installed HEAD and I'm not able to reproduce the internal error either.

[james-smith-69781]

Is there additional info I could share that would be useful?

I updated to Homebrew's HEAD version of Agda and it still reproes for me:

An internal error has occurred. Please report this as a bug.
Location of the error: __IMPOSSIBLE__, called at src/full/Agda/TypeChecking/Errors.hs:296:18 in Agd-2.6.3-1fd9406f:Agda.TypeChecking.Errors

[andreasabel]

I cannot reproduce this with any of 2.6.1, 2.6.2, or 2.6.3 (dev version).

[andreasabel]

Actually, looking at the error location, this could be a problem with case-insensitive/ignoring file systems (wild guess).

agda/src/full/Agda/TypeChecking/Errors.hs

Line 296 in 8aec1e6

m <- fromMaybe __IMPOSSIBLE__ <$> lookupModuleFromSource f

Is the filename exactly Universesbug.agda or is it a case-variant of it?

[james-smith-69781]

@andreasabel

The file name is universesbug.agda not Universesbug.agda. My filesystem is APFS (encrypted), which is case insensitive.

agda universesbug.agda reproduces the bug, while agda Universesbug.agda results in correct behavior.

New shrunk repro is any non-termination error in a module where the case of the module name does not match the case in the invocation of agda.

casebug.agda or Casebug.agda (irrelevant):

module Casebug where

nt : ∀ {A : Set} → A → A
nt i = nt i

% agda casebug.agda

...and...

module casebug where

nt : ∀ {A : Set} → A → A
nt i = nt i

% agda Casebug.agda

[andreasabel]

This bug is likely caused by my work on #4828 (commit be5cafa, amended by 0eaf439, see also the repercussions it had on #4671).

[andreasabel]

I can reproduce this on a FAT32-formatted USB stick, when I call agda with the case-variant of the file. (Everything works if I use the case-variant of the module.)

UPDATE (5 hrs later): Actually, this bug also exists on macOS, I could have saved myself many hours trying to get a dev env on Windows running...

[andreasabel]

The moduleToSource map contains apparently the wrong AbsolutePath: rather than the original file name, one that has been constructed from the module name:

( TopLevelModuleName 
  { moduleNameRange = Range (Just (AbsolutePath {textPath = "/Volumes/FAT32/iSSue5508.agda"})) (...)
  , moduleNameParts = "Issue5508" :| []
  }
, AbsolutePath {textPath = "/Volumes/FAT32/Issue5508.agda"}
)

[andreasabel]

Fixed by proactively putting the correct entry into the ModuleToSource map. Thanks for reporting, @james-smith-69781 !

[andreasabel]

The test fails in the cabal-test CI under Windows, see https://github.com/agda/agda/runs/3888327883?check_suite_focus=true.

--- "a/C:\\Users\\runneradmin\\AppData\\Local\\Temp\\iSS3936.golden"
+++ "b/C:\\Users\\runneradmin\\AppData\\Local\\Temp\\iSS3947.actual"
@@ -1,9 +1,7 @@
-customised/iSSue5508.agda:10,1-11,6
-Termination checking failed for the following functions:
-  A
-Problematic calls:
-  A (at customised/iSSue5508.agda:11,5-6)
-customised/iSSue5508.agda:29,6-8
-Cannot eliminate type  R  with projection  S.g
-when checking the clause left hand side
-test .g
+customised/iSSue5508.agda:6,8-17
+The name of the top level module does not match the file name. The
+module Issue5508 should be defined in one of the following files:
+  customised/Issue5508.agda
+  customised/Issue5508.lagda
+  agda-default-include-path/Issue5508.agda
+  agda-default-include-path/Issue5508.lagda

The golden value is the one for a case-insensitive file system, but Agda produces the error for a case-sensitive file system.

The module name is Issue5508

agda/test/Fail/customised/iSSue5508.agda

Line 6 in 070d0c8

module Issue5508 where -- case variant intended!

but Agda is called with file name iSSue5508.agda. The error isn't surprising even for a case-insensitive FS, the question is more why it is not triggered on macOS, but only on Windows.

UPDATE: Ah, the explanation is that Agda does something OS-specific for Windows rather than doing something filesystem-specific. Hence the difference to macOS:

agda/src/full/Agda/Utils/FileName.hs

Lines 106 to 114 in 070d0c8

	doesFileExistCaseSensitive :: FilePath -> IO Bool
	#ifdef mingw32_HOST_OS
	doesFileExistCaseSensitive f = do
	doesFileExist f `and2M` do
	bracket (findFirstFile f) (findClose . fst) $
	fmap (takeFileName f ==) . getFindDataFileName . snd
	#else
	doesFileExistCaseSensitive = doesFileExist
	#endif

This twist was added by Makoto (we miss you in the team!) in e46f6bf.

[andreasabel]

Cherry-picked onto maint-2.6.2, scheduled for 2.6.2.1.

[andreasabel]

(Had to reopen the issue just to link it to #5510.)