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

Add trustworthiness pragma #1829

Merged
merged 1 commit into from
Mar 30, 2021
Merged

Conversation

oquechy
Copy link
Contributor

@oquechy oquechy commented Feb 27, 2021

Mark Prelude, Data.Bits, Data.Word, Data.Typable, Data.ByteString, and Data.ByteString.Char8 as Trustworthy to match modules from base and bytestring packages. Without the pragma it's impossible to safe import Prelude and other modules, see #1827

@ranjitjhala
Copy link
Member

Thanks @oquechy !

I think the cabal-810 test is failing for some random reason; restarting and hopefully will pass and we can merge. (May do so otherwise too...)

@adinapoli
Copy link
Collaborator

I think the cabal-810 test is failing for some random reason; restarting and hopefully will pass and we can merge. (May do so otherwise too...)

Yes, I agree the test failure for cabal-810 is unrelated to this PR -- it seems like #1828 also failed due to the same issue. In particular, it seems like the failing test is the golden one, which checks that the --json output we get from liquidhaskell is the same as the one we have stored in a file.

I don't think the failure should hold this PR, but I guess we should investigate why the test is failing? Do we have an issue for that?

@@ -1,3 +1,4 @@
{-# LANGUAGE Trustworthy #-}
Copy link
Collaborator

Choose a reason for hiding this comment

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

I am surprised we need to add the pragma for anything except Prelude. For this and the other modules GHC should just transitively infer. But it looks like that wasn't the case?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

First, I tried to insert pragma only in Prelude but GHC still complained about safe import Data.Bits and safe import Data.Word in the project I was building. It didn't compile until I inserted pragmas in all liquid modules that the project uses.

Should I also file an issue to GHC about not inferring safety?

Copy link
Collaborator

Choose a reason for hiding this comment

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

Uhm, maybe this is actually expected after all? I was just reading the Safe Haskell Inference section in GHC's documentation, and it says:

"[..]In the case where a module is compiled without one of -XSafe, -XTrustworthy or -XUnsafe being used, GHC will try to figure out itself if the module can be considered safe. This safety inference will never mark a module as trustworthy, only as either unsafe or as safe. GHC uses a simple method to determine this for a module M: If M would compile without error under the -XSafe flag, then M is marked as safe. If M would fail to compile under the -XSafe flag, then it is marked as unsafe.[...]"

So perhaps the extra pragmas were necessary, although it's a bit unsatisfactory. I am also noticing that the original base modules have different inferred degree of safety: Data.Bits and Prelude for example are marked Trustworthy, but Data.Word is marked as Safe, so perhaps this has something to do with the chain of pragmas you had to add. Perhaps @kosmikus can shed some extra light here?

@nikivazou
Copy link
Member

The golden error seems very minor (to me). The json fields have the same information but different orders. I edited the field order in my PR and waiting to see what happens.

@nikivazou nikivazou merged commit 7e37ca2 into ucsd-progsys:develop Mar 30, 2021
@nikivazou nikivazou deleted the trustworthiness branch March 30, 2021 13:36
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.

4 participants