You cannot SPECIALISE ‘HMap.insert’

[jespercockx]

You cannot SPECIALISE ‘HMap.insert’

[AndrasKovacs]

Sure, that's what I intend to do.

[andreasabel]

@jespercockx : I cannot reproduce this (TC.Monad.Base compiles without error with make install-bin).
Do you have some non-standard local settings, e.g. in .cabal/config?

Note to myself: Our CI would not catch such problems, as we do not do a -f optimise-heavily build with GHC 8.10.7.

[jespercockx]

@jespercockx : I cannot reproduce this (TC.Monad.Base compiles without error with make install-bin).
Do you have some non-standard local settings, e.g. in .cabal/config?

I don't have anything special there, no.

Note to myself: Our CI would not catch such problems, as we do not do a -f optimise-heavily build with GHC 8.10.7.

The problem also occurs with v1-install (but not with quicker-install-bin), so in this case it would not have mattered.

[AndrasKovacs]

I reproduced this issue with ghc 8.10.7. I did add this specialization in 87ef6e4. I don't understand the problem right now, because the unordered-containers-0.2.19.1 that's being used does have INLINABLE and I don't believe -O0 is used for dependencies.

[andreasabel]

With the current master and GHC 8.10.7,

NB: @jespercockx, I recommend using a more recent GHC for development, since some warnings are off for older GHCs:

agda/Agda.cabal

Lines 276 to 298 in 1688c26

	if impl(ghc >= 9.0)
	ghc-options:
	-Werror=invalid-haddock
	-- #6137: coverage checker works only sufficiently well from GHC 9.0
	-Werror=incomplete-patterns
	-Werror=incomplete-record-updates
	-Werror=overlapping-patterns
	-- ASR (2022-04-27). This warning was added in GHC 9.0.2, removed
	-- from 9.2.1 and added back in 9.2.2.
	if impl(ghc == 9.0.2 || >= 9.2.2)
	ghc-options:
	-Werror=unicode-bidirectional-format-characters
	if impl(ghc >= 9.2)
	ghc-options:
	-- -Werror=operator-whitespace
	-Werror=redundant-bang-patterns
	if impl(ghc >= 9.4)
	ghc-options:
	-Werror=forall-identifier
	-Werror=type-equality-out-of-scope

In my recent PR I also activate the operator-whitespace warning (from GHC 9.2):

• #6929

[jespercockx]

NB: @jespercockx, I recommend using a more recent GHC for development, since some warnings are off for older GHCs:

I switched to GHC 9.2.5 for now (which is the version recommended by ghcup at the moment).

[andreasabel]

I switched to GHC 9.2.5 for now (which is the version recommended by ghcup at the moment).

Your GHCup seems also outdated 🤣 , mine says:

✗  ghc   9.4.7          recommended,base-4.17.2.0      

[jespercockx]

Ah yes, indeed. However, it is still not hls-powered which is annoying. The latest hls-powered release is 9.4.4.

[MatthewDaggitt]

This is also failing on the standard library: https://github.com/agda/agda-stdlib/actions/runs/6688745401/job/18171228466#step:8:1780

[andreasabel]

@jespercockx wrote:

Ah yes, indeed. However, it is still not hls-powered which is annoying. The latest hls-powered release is 9.4.4.

I fear the hls-powered tags are outdated in ghcup list. The table at their homepage lists 9.4.7 as "fully supported" (and 9.4.4 as deprecated): https://haskell-language-server.readthedocs.io/en/latest/support/ghc-version-support.html

• haskell/ghcup-metadata#143

[andreasabel]

@AndrasKovacs : Did you find time to investigate this further? How should we proceed?

A radical step would be to drop GHC 8. But this would require us dropping our Ubuntu LTS support policy (GHC 9 is only shipped with 23.04 or higher). We would then have to require users to install GHC (e.g. via ghcup) first if they want to install from source (and updated the docs accordingly), or bring our binary dists up to speed.

[AndrasKovacs]

I can just remove the offending SPECIALIZE-s. For that I guess I'd need to check builds with all supported GHC versions. What's the official way to get the list of GHC versions? Is it good to get the GHC-s corresponding to each stack.yaml file?

EDIT: sorry, I see the tested-with list in the cabal file already. I'll go through the builds if there's no better idea.

[gallais]

I can just remove the offending SPECIALIZE-s.

Can we ifdef them so that we do benefit from them whenever it is possible?

[AndrasKovacs]

After building everything, there's just a single offending pragma that fails to build below ghc-9.x. I added CPP for it in #6949. I think this is safe to close now.

[andreasabel]

I suppose reporting this to the GHC team makes little sense as they won't fix the GHC 8.x series anymore.

[MatthewDaggitt]

Hmm, the standard library is building Agda 2.6.4 release so this bug appears to have made it into the 2.6.4 release? Concretely, as a consequence of this bug, which versions of GHC can Agda 2.6.4 not be built with? Do we need to update the documentation anywhere?

[andreasabel]

@MatthewDaggitt wrote:

Hmm, the standard library is building Agda 2.6.4 release so this bug appears to have made it into the 2.6.4 release? Concretely, as a consequence of this bug, which versions of GHC can Agda 2.6.4 not be built with? Do we need to update the documentation anywhere?

You seem to be using Agda master in the quoted workflow:

  git clone https://github.com/agda/agda
  cd agda
  git checkout 
  mkdir -p doc
  touch doc/user-manual.pdf
  cabal v1-install --ghc-options='-O1 +RTS -M6G -RTS'
  cd ..
  shell: /usr/bin/bash -e {0}
  env:
    GHC_VERSION: 8.10.7
    CABAL_VERSION: 3.6.2.0
    CABAL_INSTALL: cabal v1-install --ghc-options='-O1 +RTS -M6G -RTS'
    AGDA: agda -Werror +RTS -M3.5G -H3.5G -A128M -RTS -i. -i src/
Cloning into 'agda'...
Your branch is up to date with 'origin/master'.

https://github.com/agda/agda-stdlib/actions/runs/6688745401/job/18171228466#step:8:4
There is a suspicious step

  git checkout

which looks like it wanted to checkout a specific branch/tag, but the respective variable was empty.

Appearances can be deceiving. (Agent Smith)

I upstreamed this here:

• agda/agda-stdlib#2188