[Extraction] [Haskell] Add support for GHC >= 9

[JasonGross]

Kind: bug fix

Fixes #14256

• Added / updated test-suite (Is there a way to do this?)
• Corresponding documentation was added / updated (including any warning and error messages added / removed / modified). (is there any documentation to update?)
• Entry added in the changelog (see https://github.com/coq/coq/tree/master/doc/changelog#unreleased-changelog for details).
• Overlay pull requests (if this breaks 3rd party developments in CI, see
  https://github.com/coq/coq/blob/master/dev/ci/user-overlays/README.md for details)

[pi8027]

Added / updated test-suite (Is there a way to do this?)

No.

Corresponding documentation was added / updated (including any warning and error messages added / removed / modified). (is there any documentation to update?)

I don't think so.

If you have some time, please check my recent comment: #14256 (comment).

[silene]

The tests in test-suite/output using Extraction Language Haskell need to be updated. As for unsafeCoerce vs unsafeCoerce#, the current pull request is conservative, so the change can be delayed to another pull request.

[pi8027]

Sure. I will test this fix with GHC 8.01, 8.02, and 8.10.4 (but unfortunately Stack does not seem to support GHC 9 yet). If I don't see any issue, I will push a fix for the test-suite and merge.

[JasonGross]

@pi8027 Thanks for the update! I've updated this PR a bit further, since as I discovered in #14256 (comment) the change to Any is not needed, and in fact we only need to update unsafeCoerce. Hence I've reverted the change to Any, which was already addressed in #6023

[JasonGross]

(Sorry for being so belated in updating this)

[pi8027]

I confirm it works at least with GHC 7.10.3, 8.0.1, 8.0.2, and 8.10.4.

[pi8027]

@JasonGross Thanks. Just to be sure, did you test the output with GHC 9? If so, I think this is ready to merge as soon as CI passes.

[JasonGross]

I did not, as I don't have easy access to it. I am basing the change on the tags of ghc/ghc@74ad75e, which indicate that it first showed up in 9.0

[JasonGross]

But I have tested effectively the same change with GHC 9 on Fiat-Crypto CI using https://github.com/mit-plv/fiat-crypto/blob/master/src/haskell.sed, so unless I've made a typo, it works

[pi8027]

OK, that seems fine with me. Let's merge.

[pi8027]

@coqbot: merge now