Andreas Abel

> A random guess: since you are on a case-insensitive system, does your module name agree exactly with your file name (including case)? See #5508 Yes, @andrejbauer : - What...

The is likely no MWE coming. Closing.

> Sorry for the delay. Using Agda 2.6.2 on MacOS, I can confirm that the problem is caused by case-insensitive file names. When I make sure that the file name...

> Looks like `Agda.Interaction.FindFile` already has the right logic. Should this ifdef: > > https://github.com/agda/agda/blob/798be60d51a56a8c74cfd309c1498b070240e686/src/full/Agda/Utils/FileName.hs#L107-L114 > > also be activated for mac? Trying to remember my thought process here. OK:...

> In that case we should perhaps refuse having (say) both `A.agda` and `a.agda` on a case-sensitive file system. Yes! I definitely support this. > However, should we then also...

This suggests that `text-icu` provides the standard. I can change my mind, knowing a standard exists...

Ping @andrejbauer for a self-contained reproducer.

Ping @andrejbauer for a self-contained reproducer.

Bringing back the unreachable clause error in - https://github.com/agda/agda/pull/6131

> ``` > src/full/Agda/Syntax/Concrete/Pattern.hs:104:22-58: Non-exhaustive patterns in record update > ``` We should rule out such error statically with `-Werror=incomplete-record-updates`. However, a first experiment suggests that e.g. all uses of...