Use GHC.Base.Any for compatibility with GHC 8.2

[tchajed]

Fixes #6022.

Thanks @bmsherman for identifying the issue!

[tchajed]

The GHC issue (Trac 10886) doesn't really resolve the backwards compatibility issue. It looks like GHC.Base re-exports GHC.Types and GHC.Prim, which means this solution works in both 8.0.1 and 8.2.1.

I'd like to check that this works in GHC 7 and then I'm happy with this solution, even though it's somewhat unclear to me what GHC wants users to do. The alternative is to use GHC.Prim.Any in older GHC versions and GHC.Types.Any in GHC >= 8.2.

[tchajed]

Also here's a test case that triggers a use of Any.

Require Import Extraction.

Inductive expr : Type -> Type :=
| bind : forall T T', expr T -> expr T'.

Extraction Language Haskell.

Extraction "expr.hs" expr.

[maximedenes]

@letouzey Could you review this PR? Thanks!

[maximedenes]

@letouzey ping

[maximedenes]

@letouzey Would you have some time to look at this PR?

[tchajed]

I actually want this patch at least in Coq master, since Arch uses GHC 8.2. Is there anybody else with some basic knowledge of Haskell to review this?

I've now tested this example on GHC 7.10.3, 8.0.2, and 8.2.1. If somebody wants to reproduce (which I imagine is the only blocker to merging), use Stack resolvers lts-6.27, lts-9.13, and nightly-2017-11-15 respectively.

[Zimmi48]

Maxime has asked a review from @letouzey because he is kind of "the guardian of the temple" when it comes to Extraction. However, given the triviality of this patch, given that it has been pending for more than 20 days, and given that it was extensively tested by @tchajed, I say this should get merged without waiting more.

[Zimmi48]

@tchajed: BTW, @letouzey said we can't test the result of extraction to Haskell in the test-suite but we could on Travis. If you want to contribute such tests, a PR would be welcome, I guess.

[maximedenes]

Sounds good, will merge then, thanks!

[maximedenes]

Thanks for your contribution and your patience, @tchajed !