Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix build with GHC 8.0.2 #2310

Merged
merged 1 commit into from Nov 22, 2016
Merged

Fix build with GHC 8.0.2 #2310

merged 1 commit into from Nov 22, 2016

Conversation

RyanGlScott
Copy link
Contributor

Agda has symptoms of code that was pointed out in GHC Trac #12784, and as a result, Agda fails to build with GHC 8.0.2. This PR fixes the situation by reworking some default type signatures so that they are more correct w.r.t. their type variables.

@@ -1,4 +1,6 @@
{-# LANGUAGE CPP #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE NoMonoLocalBinds #-}
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

So you might be wondering why enabling NoMonoLocalBinds is necessary here. The confusing reality is that enabling GADTs implies also enabling MonoLocalBinds, which causes dozens of functions below to have monomorphic inferred type signatures (even in the presence of NoMonomorphismRestriction!) Thus we need to have NoMonoLocalBinds appear after GADTs to counter this behavior.

@ilovezfs
Copy link

ilovezfs commented Nov 22, 2016

Unfortunately this doesn't apply cleanly to the current release tag.

@mietek @asr any idea when the next tag is due? Right now this bug currently means that agda cannot be built with brew's GHC on Sierra.

@UlfNorell UlfNorell merged commit 5e778c9 into agda:stable-2.5 Nov 22, 2016
@UlfNorell
Copy link
Member

We should get 2.5.1.2 (which would just be 2.5.1.1 + this commit) out asap. I filed #2311.

@ilovezfs
Copy link

Yes, also because of alex. If necessary, I can apply a minimal patch on Homebrew until the release is out.

==> Summary
🍺  /usr/local/Cellar/agda/2.5.1.1: 1,003 files, 118M, built in 36 minutes 27 seconds

@ilovezfs
Copy link

Yeah, the alex issue alone causes CI to fail on all nodes: https://bot.brew.sh/job/Homebrew%20Testing/1168/

@asr asr added this to the 2.5.1.2 milestone Nov 22, 2016
UlfNorell referenced this pull request Nov 23, 2016
ghc-8.0.2-rc1 compiles the modules in a different order from
previous versions of ghc leading to the test failing. Since we
only care that the compilation was successful we can ignore
the ghc output completely.
@asr asr removed this from the 2.5.1.2 milestone Nov 24, 2016
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

4 participants